Augmenting Smart Contract Decompiler Output through Fine-grained Dependency Analysis and LLM-facilitated Semantic Recovery

Prior work

• Earlier recovery tools have limited scope or rely on fixed heuristics, while learning-based methods can degrade on newly emerging or rare contracts.Prior methods target selected information, such as attributes or parameter types, and some rely on EVM-instruction heuristics.Source: §I · pp. 1–2

Our work

• SmartHalo combines static analysis and LLMs to recover function boundaries, variable types, and contract attributes in existing decompiler output.Static analysis extracts state, control-flow, and type dependencies for prompts that guide LLM optimization.Source: §I · p. 2

Key insight

• Program context offers complementary recovery signals: static analysis handles constrained targets, while LLMs can predict types for rare local variables.The paper attributes this division to static analysis soundness and LLM flexibility in few-shot in-context learning.Source: §I · p. 2

Correctness verification

• SmartHalo checks optimized code against the original using symbolic execution and formal verification, and rejects errors that violate static rules.The checks target program-behavior equivalence and static rules such as type rules.Source: §I · p. 2

Evaluation

• Against Gigahorse, SmartHalo improves function-boundary precision by 20.30% and recall by 30.03%; against VarLifter, type precision by 13.51% and recall by 77.08%.Against SmartDagger, contract-attribute precision improves by 44.69% and recall by 80.86%.Source: §I · p. 2
• SmartHalo enables 60.22% of optimized code to be recompiled, while its output also improves vulnerability-detection precision and recall for integer overflow.The reported integer-overflow gains are 21.96% precision and 38.00% recall; contract-attack identification precision improves by 16.67%.Source: §I · p. 2

A. Smart Contract Decompiler

• More than 99% of smart contracts do not publicly disclose source code, making decompilation important when only bytecode is accessible.Decompilation recovers program abstractions and synthesizes them into a high-level code representation.Source: A. Smart Contract Decompiler · pp. 2–3
• Compiler information loss and low-coverage heuristics make it difficult to restore bytecode to its original source code.The lost information can include variable types, names, annotations, and function boundaries.Source: A. Smart Contract Decompiler · p. 3

B. Deficiencies in Decompiler Output

• Type-recovery errors can assign the wrong mapping key type or parameter type, and can complicate identification of vulnerabilities such as overflows.Existing tools may cover only selected variable types or rely heavily on predefined EVM-instruction heuristics.Source: B. Deficiencies in Decompiler Output · p. 3
• Contract attributes such as assets can disappear at bytecode level, making it harder to identify vulnerabilities such as reentrancy.In the Bank example, recognizing Acc.balance as an asset attribute is critical to the vulnerability analysis.Source: B. Deficiencies in Decompiler Output · p. 3
• Low-coverage heuristics can miss inherited functions because inheritance embeds base-contract code without explicit call information in bytecode.Gigahorse may integrate an inherited validate function into handle, hindering cross-contract call-flow and component analysis.Source: B. Deficiencies in Decompiler Output · p. 4

C. Our solution

• Static analysis links type dependencies, control flow, and state-variable usage to recover types, function boundaries, and contract attributes.For example, a bytes32 return type can propagate through dependent variables to correct a mapping key type.Source: C. Our solution · p. 4
• LLMs can predict optimization targets that are rare or lack useful constraints from other program elements, complementing static analysis.The paper illustrates this with an LLM assigning a string-memory type to an input variable.Source: C. Our solution · p. 4

III. DESIGN OF SMARTHALO

• SmartHalo takes decompiler output and builds a Dependency Graph from state, type, and control-flow dependencies to represent critical program semantics.The design extends prior work by adding state and type dependencies.Source: §III · pp. 4–5
• The graph guides prompts that provide target context, static-analysis inference steps, and candidate types or attributes for LLM optimization.SmartHalo uses the prompts to guide recovery of variable types, contract attributes, and function boundaries.Source: §III · p. 5
• Symbolic execution and formal verification check behavioral equivalence, while static type rules identify and reject rule-violating inferences.The rule check does not cover function boundaries or contract attributes because the paper identifies no explicit static rules for them.Source: §III · p. 5

A. Dependency-based Semantic Extraction

• The DG represents variables and expressions as nodes, and control-flow, state, and type dependencies as labeled edges.Source: A. Dependency-based Semantic Extraction · p. 6
• SmartHalo constructs the DG by adding state- and type-dependency edges to a control-flow graph and connecting related variables and expressions.Source: A. Dependency-based Semantic Extraction · p. 6

B. LLM-driven Semantic Enrichment

• SmartHalo builds prompts from code contexts, inference candidates, and chain-of-thought steps derived from static-analysis dependencies.Source: B. LLM-driven Semantic Enrichment · pp. 6–7
• For variables, SmartHalo uses DG-based code slicing to select dependent expressions; for functions, it extracts functions along their call chains as context.The selected code snippets narrow the original decompiled code to content related to the target variable or function.Source: B. LLM-driven Semantic Enrichment · p. 6
• SmartHalo supplies candidate types and contract attributes to the LLM to narrow its selection range.Type candidates are collected from Solidity's built-in types, while contract-attribute candidates are summarized from representative smart-contract data.Source: B. LLM-driven Semantic Enrichment · p. 6
• Chain-of-thought templates use type and control-flow dependencies for variable-type optimization, and control-flow dependencies for function-boundary optimization.Source: B. LLM-driven Semantic Enrichment · p. 7

C. Correctness Verification

• Symbolic execution generates summaries for the original and optimized functions, and formal verification checks an assertion of their program-behavior equivalence.Source: C. Correctness Verification · p. 8
• Non-linear constraints in symbolic summaries can make Z3 solving difficult, and SmartHalo uses methods from ARDiff to eliminate most solving failures.Source: C. Correctness Verification · p. 8
• Static violation-rejection rules inspect optimized code to identify and reject incorrect LLM-predicted variable types.The rules are expressed as premises and conclusions, with type judgments assigning types to expressions in context.Source: C. Correctness Verification · p. 8
• Verification suggestions and identified violations are retransmitted to the LLM, with optimization and checking repeated until errors are amended or the iteration limit is reached.Source: C. Correctness Verification · pp. 8–9

• The evaluation asks how effective SmartHalo is at optimizing decompiler output.Source: §V · p. 9
• It compares SmartHalo with state-of-the-art mechanisms and examines how individual components affect optimization precision.Source: §V · p. 9
• The evaluation also asks whether SmartHalo generalizes across complex contracts, decompilers, and LLMs, and examines efficiency and downstream program-analysis utility.Source: §V · p. 9

• From 500 randomly sampled functions, the authors retained 456 source-code/decompiler-output pairs after excluding functions the decompiler could not handle.The source dataset contained 963,151 smart contracts, and function pairs were used because SmartHalo's GPT input requires shorter snippets.Source: A. Implementation and Evaluation Setup · p. 9
• Function-boundary and variable-type ground truth came from direct comparison with source code, while contract-attribute ground truth was manually summarized.Source: A. Implementation and Evaluation Setup · p. 9
• Six researchers formed two annotator pairs and a referee pair; consensus was sought through cross-validation, with referee decisions when needed.Average Cohen’s Kappa was 0.772.Source: A. Implementation and Evaluation Setup · p. 9
• The evaluation measures boundary match, exact type match, exact contract-attribute match, and recompilation failures.Source: A. Implementation and Evaluation Setup · p. 9

B. Overall Effectiveness

• The evaluation compares optimized SmartHalo code with Dedaub output using four key metrics and examines optimization failures.Source: B. Overall Effectiveness · p. 9
• SmartHalo improves all four metrics over Dedaub: boundary precision/recall by 20.30%/30.03% and variable-type precision/recall by 30.02%/42.04%.The comparison evaluates SmartHalo on the evaluation dataset against the original Dedaub output.Source: Table III · p. 10, B. Overall Effectiveness · p. 10
• SmartHalo recovers contract attributes at 68.06% precision and 90.93% recall; 60.22% of its optimized code can be recompiled.The original decompiler output lacks contract attributes and is not suitable for recompilation.Source: B. Overall Effectiveness · p. 10
• Failures occur with low-level or delegated calls, inline assembly, off-chain reliance, inheritance structures, and other cases; many call-related failures stem from incorrect Gigahorse facts.The authors attribute most E1 failures to Gigahorse and most E2 and E5 failures to GPT-3.5 limitations; E3 and E4 pose limits for static analysis.Source: B. Overall Effectiveness · p. 10

C. Comparison to Prior Work

• SigRec, DeepInfer, and Neural-FEBI recover only subsets of types or function boundaries, while SmartHalo optimizes these targets across all variables and functions.The authors could not reproduce SigRec or DeepInfer or conduct a comparative evaluation with Neural-FEBI because of unavailable or incomplete implementation artifacts.Source: C. Comparison to Prior Work · p. 10
• Against SmartDagger, SmartHalo improves contract-attribute precision and recall by 44.69% and 80.86%; against VarLifter, variable-type precision and recall improve by 13.51% and 77.08%.The authors report that SmartDagger’s performance degrades on newly emerging contracts, while VarLifter’s low-coverage heuristic rules recover only a small subset of variable types.Source: Table IV · p. 10, C. Comparison to Prior Work · pp. 10–11
• SmartHalo with GPT-3.5 reaches 68.06% precision and 90.93% recall for contract attributes, and 92.27% precision and 84.26% recall for variable types.With GPT-4o mini, contract-attribute precision is 80.65% and variable-type recall is 88.81%.Source: C. Comparison to Prior Work · p. 11

D. Ablation Study

• LLM alone offers limited boundary gains over Dedaub, raises variable-type precision by 10.01%, but lowers variable-type recall by 18.80%.The authors report incorrect boundary predictions without static-knowledge prompts and state-variable deletions in LLM-optimized code.Source: D. Ablation Study · p. 11
• The passage refers to improvement of decompiler output optimization in SmartHalo.Source: D. Ablation Study · p. 11

E. Generalizability Ability

• On 50 complex contracts covering more than 12 scenarios, SmartHalo improves boundary recall by 20.44%, variable-type precision/recall by 16.89%/16.80%, and recovers contract attributes at 86.95% precision and 48.27% recall.The contracts comprise around 900 functions and include inheritance, modifiers, and complex storage patterns.Source: Table VI · p. 11, E. Generalizability Ability · p. 11
• Across GPT-4o mini, Deepseek-R1, and Qwen-2.5-coder, SmartHalo reports improvements or recovered contract attributes; it also performs well with locally deployed 7B-parameter Llama 3.The authors summarize performance across LLMs as generalizable regardless of model type, open-source status, reasoning capability, or model version.Source: E. Generalizability Ability · p. 12
• With Heimdall and Panoramix, SmartHalo improves precision and recall across the reported metrics and recovers contract attributes, supporting adaptability across decompilers.The reported contract-attribute precision/recall is 46.63%/99.52% for Heimdall and 81.76%/81.86% for Panoramix.Source: E. Generalizability Ability · p. 12

F. Efficiency

• Per-function processing averages 1.94 s for dependency-based semantic extraction, 8.95 s for LLM-driven enrichment, and 13.10 s for correctness verification.Source: F. Efficiency · p. 12, Table X · p. 13
• With GPT-4o mini, SmartHalo averages 8,920 tokens and $0.00136 per function, or an estimated $0.046 and 815.66 s per contract.The contract estimate assumes approximately 34 functions per contract in the evaluation dataset.Source: F. Efficiency · pp. 12–13
• A local 7B-parameter Llama model can reduce SmartHalo’s monetary cost to nearly zero; verification runtime and cost stop increasing at iteration limit n ≥3, where convergence reaches 100%.The evaluation sets the iteration limit to 3.Source: F. Efficiency · p. 13

Contract attributes for Reentrancy vulnerability detection

• 80.41% Reentrancy-detection precision with SliSE+SmartHalo versus 72.16% with SliSE; SmartHalo eliminated 8 of 27 reported false positives.In the example, recovering the state variable's [Flag] attribute distinguishes a non-profitable function from a Reentrancy risk.Source: Table XI · p. 13, §VI · p. 13

Function identification for attack identification

• 16.67% higher attack-identification recall with BlockWatchdog+SmartHalo than with BlockWatchdog alone.The example attributes a missed attack path to an unavailable function boundary in decompiled code; SmartHalo identifies the function.Source: Table XII · p. 13, §VI · pp. 13–14

Variable types for Integer-overflow vulnerability detection

• 21.96% higher precision and 38.00% higher recall for Mythril+SmartHalo than Mythril alone on integer-overflow detection.SmartHalo recovers a variable's uint256 type, supplying the bit width Mythril needs to check for overflow; Mythril alone misses it without that type information.Source: Table XIII · p. 13, §VI · p. 14

VII. DISCUSSION AND LIMITATION

• SmartHalo combines static analysis and LLMs for joint decompiler-output optimization and applies correctness verification to optimization outputs.The authors describe its evaluation as showing effectiveness for function boundaries, variable types, and contract attributes compared with prior approaches.Source: §VII · p. 14
• Generic dependency extraction and few-shot in-context learning are presented as reasons SmartHalo can adapt to newly deployed contracts.The authors define few-shot in-context learning as addressing new cases during inference based on a small number of known examples.Source: §VII · p. 14
• Although evaluation focuses on functions, prompts capture contract-wide context, and the authors report scalability for contract-level decompilation optimization.Examples include modifier context and dependencies between key–value pairs in mappings and structs.Source: §VII · p. 15
• SmartHalo cannot recover inheritance structures because inheritance relationships and class information are absent from bytecode; evaluation covers 456 functions.The authors describe the evaluation sample as relatively small, while noting its random selection from a large real-world repository and diversity of application scenarios.Source: §VII · p. 15
• Predefined type rules used for correctness verification are identified as an internal threat to validity.The discussion also states that SmartHalo focuses on Solidity and argues that its static rules are generic across Solidity versions.Source: §VII · p. 15

VIII. RELATED WORK

• The conclusion reports improved function-boundary identification, variable-type inference, contract-attribute recovery, and downstream-task effectiveness; related work spans static-analysis and learned approaches.The related-work discussion notes that prior dependency-analysis approaches rely on heuristic rules, while neural approaches predict function names.Source: §IX · p. 15, §VIII · p. 15