From 80096d90684e650f54486fb537ffa76acb35f874 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 3 Aug 2026 15:54:21 +0000 Subject: [PATCH 1/2] Add end-to-end .solc regression test for asm constant substitution MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Complements the substYulBlock unit tests with an executable contract that runs through the full pipeline (sol-core → yule → solc → testrunner) and asserts real EVM return values, so the miscompilation is caught end to end: * asmFlow() — `x := 5; y := add(x, 1)` returns 6 (buggy: 1). * asmLoopFlow() — a loop body accumulating an outer `s` returns 3 (buggy: the pre-loop literal `s == 0` is inlined into the body, so `s` is reset to 1 each iteration and the function returns 1). Registered in run_contests.sh (executes and checks return data) and in the tasty `dispatches` group in Cases.hs (compile coverage under `cabal test`). Co-Authored-By: Alex Beregszaszi --- run_contests.sh | 1 + test/Cases.hs | 1 + test/examples/dispatch/asm_subst.json | 40 +++++++++++++++++++++++++++ test/examples/dispatch/asm_subst.solc | 40 +++++++++++++++++++++++++++ 4 files changed, 82 insertions(+) create mode 100644 test/examples/dispatch/asm_subst.json create mode 100644 test/examples/dispatch/asm_subst.solc diff --git a/run_contests.sh b/run_contests.sh index e36c8dddf..e51aef378 100755 --- a/run_contests.sh +++ b/run_contests.sh @@ -8,6 +8,7 @@ cd "$root_dir" bash ./contest.sh test/examples/dispatch/basic.json bash ./contest.sh test/examples/dispatch/assembly.json bash ./contest.sh test/examples/dispatch/asm_break_continue_leave.json +bash ./contest.sh test/examples/dispatch/asm_subst.json bash ./contest.sh test/examples/dispatch/neg.json bash ./contest.sh test/examples/dispatch/miniERC20.json bash ./contest.sh test/examples/dispatch/Revert.json diff --git a/test/Cases.hs b/test/Cases.hs index dc6aa69de..6318c3c56 100644 --- a/test/Cases.hs +++ b/test/Cases.hs @@ -128,6 +128,7 @@ dispatches = "Files for dispatch cases" [ runDispatchTest "basic.solc", runDispatchTest "assembly.solc", + runDispatchTest "asm_subst.solc", runDispatchTest "stringid.solc", runDispatchTest "storage.solc", runDispatchTest "miniERC20.solc", diff --git a/test/examples/dispatch/asm_subst.json b/test/examples/dispatch/asm_subst.json new file mode 100644 index 000000000..4fc296308 --- /dev/null +++ b/test/examples/dispatch/asm_subst.json @@ -0,0 +1,40 @@ +{ + "asm_subst": { + "bytecode": "_CODE", + "contract": "C", + "tests": [ + { + "input": { + "comment": "constructor()", + "calldata": "", + "value": "0" + }, + "kind": "constructor" + }, + { + "input": { + "comment": "asmFlow()(uint256) -> 6 (x := 5; y := add(x, 1))", + "calldata": "8decb8c5", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000006", + "status": "success" + } + }, + { + "input": { + "comment": "asmLoopFlow()(uint256) -> 3 (accumulate s across 3 iterations)", + "calldata": "2b591092", + "value": "0" + }, + "kind": "call", + "output": { + "returndata": "0000000000000000000000000000000000000000000000000000000000000003", + "status": "success" + } + } + ] + } +} diff --git a/test/examples/dispatch/asm_subst.solc b/test/examples/dispatch/asm_subst.solc new file mode 100644 index 000000000..a9c5c80fc --- /dev/null +++ b/test/examples/dispatch/asm_subst.solc @@ -0,0 +1,40 @@ +import std.{*}; +import std.dispatch.{*}; + +// Regression tests for constant substitution into `assembly` blocks, which the +// partial evaluator must apply in a scope- and flow-aware way. A single, +// uniform substitution map (built from every literal-valued local in scope) +// used to be inlined into the whole block at once, producing wrong code. +contract C { + constructor() {} + + // Flow-sensitivity: after `x := 5` the read of `x` in `add(x, 1)` must see + // the new value 5, not the pre-block literal 0. The buggy substitution + // folded the second statement to `add(0, 1)` and returned 1; the correct + // result is 6. + public function asmFlow() -> uint256 { + let x : word = 0; + let y : word = 0; + assembly { + x := 5 + y := add(x, 1) + } + return uint256(y); + } + + // A variable assigned inside a loop is not loop-invariant: the pre-loop + // literal `s == 0` must not be inlined into `add(s, 1)` in the body. The + // buggy substitution rewrote the body to `s := add(0, 1)`, so `s` was reset + // to 1 on every iteration and the function returned 1; the correct sum over + // three iterations is 3. The asm-local counter `j` (no outer counterpart) + // exercises the loop without any name collision. + public function asmLoopFlow() -> uint256 { + let s : word = 0; + assembly { + for { let j := 0 } lt(j, 3) { j := add(j, 1) } { + s := add(s, 1) + } + } + return uint256(s); + } +} From 229c32ef9ede30fde4c096e68a6d158e41d4914f Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 3 Aug 2026 15:20:24 +0000 Subject: [PATCH 2/2] Make asm constant substitution scope- and flow-aware MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `evalStmt (MastAsm yul)` inlined every literal-valued binding in scope into the asm block with a single, uniform substitution map. That map was neither scope- nor flow-aware, so it produced wrong code in two ways: * Flow: after an in-block `x := 5`, later reads of `x` were still replaced by the stale pre-block literal (`y := add(x, 1)` folded to `add(0, 1)`). * Shadowing: an asm-local `let i` (including a `for`-loop counter, plain `let`, and function parameters/returns) was overwritten by the outer literal, e.g. `for { let i := 0 } lt(i, 3) { ... }` became `lt(0, 3)` — an infinite loop. `substYulBlock` now threads the substitution map through the statement sequence: an assignment drops the reassigned name, a `let`/parameter/return drops the shadowed name for the rest of its scope, and assignments that escape a nested `if`/`for`/`switch`/block invalidate the outer literal afterwards. Yul function bodies have an isolated scope, so they neither leak shadowing outward nor let inner assignments invalidate outer literals. Adds direct unit tests for `substYulBlock` in YulEvalTests covering the flow case, the shadowing cases (plain `let`, `for` counter, loop-assigned variable, function params/returns), let-initialiser scope, and nested-block escape. Co-Authored-By: Alex Beregszaszi --- src/Solcore/Backend/MastEval.hs | 145 +++++++++++++++++++++++++++----- test/YulEvalTests.hs | 95 +++++++++++++++++++++ 2 files changed, 219 insertions(+), 21 deletions(-) diff --git a/src/Solcore/Backend/MastEval.hs b/src/Solcore/Backend/MastEval.hs index 0ad9ed6e0..3bd629787 100644 --- a/src/Solcore/Backend/MastEval.hs +++ b/src/Solcore/Backend/MastEval.hs @@ -16,6 +16,7 @@ module Solcore.Backend.MastEval evalYulOp, evalYulStmt, evalYulBlock, + substYulBlock, asmIsInterpretable, maskWord, mstoreBytes, @@ -707,36 +708,138 @@ venvToSubst env = yulLit (StrLit s) = YLit (YulString s) -- | Substitute known literal values into a Yul block. --- Only replaces YIdent occurrences in expression positions; does not touch --- variable names on the left-hand side of let/assign or function parameter lists. +-- +-- The substitution map is inlined into expression positions only (never into +-- the names on the left of let/assign or into parameter lists), but it is +-- threaded through the statement sequence so it stays both scope- and +-- flow-aware: +-- +-- * An asm-local @let x@ shadows any outer @x@: @x@ is dropped from the map +-- for the rest of that scope, so later reads resolve to the local binding +-- instead of the eliminated comptime value (otherwise a @for@ loop that +-- rebinds its counter would read the stale outer literal forever). +-- * An assignment @x := …@ makes the pre-block literal of @x@ stale: @x@ is +-- dropped from the map so subsequent statements read the new runtime value +-- (otherwise @x := 5; y := add(x, 1)@ would inline the pre-block @x@). +-- * @let@/parameter/return names introduced by a nested @if@/@for@/@switch@/ +-- function shadow within their own scope only; assignments to outer +-- variables inside them escape and invalidate the outer literal afterwards. substYulBlock :: Map.Map Name YulExp -> [YulStmt] -> [YulStmt] -substYulBlock subst = map (substYulStmt subst) - -substYulStmt :: Map.Map Name YulExp -> YulStmt -> YulStmt -substYulStmt subst (YAssign names e) = YAssign names (substYulExp subst e) -substYulStmt subst (YExp e) = YExp (substYulExp subst e) -substYulStmt subst (YLet names me) = YLet names (fmap (substYulExp subst) me) -substYulStmt subst (YIf e block) = YIf (substYulExp subst e) (substYulBlock subst block) -substYulStmt subst (YBlock stmts) = YBlock (substYulBlock subst stmts) -substYulStmt subst (YFun n as rs body) = YFun n as rs (substYulBlock subst body) +substYulBlock _ [] = [] +substYulBlock subst (s : ss) = + let (s', subst') = substYulStmt subst s + in s' : substYulBlock subst' ss + +-- | Substitute into one statement and return the map to use for the statements +-- that follow it in the same block (with shadowed/reassigned names removed). +substYulStmt :: Map.Map Name YulExp -> YulStmt -> (YulStmt, Map.Map Name YulExp) +substYulStmt subst (YAssign names e) = + (YAssign names (substYulExp subst e), dropNames names subst) +substYulStmt subst (YExp e) = (YExp (substYulExp subst e), subst) +substYulStmt subst (YLet names me) = + (YLet names (fmap (substYulExp subst) me), dropNames names subst) +substYulStmt subst (YIf e block) = + ( YIf (substYulExp subst e) (substYulBlock subst block), + dropSet (escapingAssignsYulBlock block) subst + ) +substYulStmt subst (YBlock stmts) = + ( YBlock (substYulBlock subst stmts), + dropSet (escapingAssignsYulBlock stmts) subst + ) +substYulStmt subst (YFun n as rs body) = + -- Parameters and return variables are local to the body; the definition + -- itself does not change any binding in the enclosing scope. + let inner = dropNames (as ++ concat rs) subst + in (YFun n as rs (substYulBlock inner body), subst) substYulStmt subst (YFor pre c post b) = - YFor - (substYulBlock subst pre) - (substYulExp subst c) - (substYulBlock subst post) - (substYulBlock subst b) + -- Top-level @pre@ lets scope over the whole loop and shadow outer bindings; + -- any variable assigned inside the loop is not loop-invariant, so its + -- pre-loop literal must not be inlined into the condition/post/body either. + let shadowed = letBoundYulBlock pre + escaping = + escapingAssignsYulBlock pre + `Set.union` escapingAssignsYulBlock post + `Set.union` escapingAssignsYulBlock b + inner = dropSet (shadowed `Set.union` escaping) subst + in ( YFor + (substYulBlock inner pre) + (substYulExp inner c) + (substYulBlock inner post) + (substYulBlock inner b), + dropSet escaping subst + ) substYulStmt subst (YSwitch e cases def) = - YSwitch - (substYulExp subst e) - (map (\(lit, block) -> (lit, substYulBlock subst block)) cases) - (fmap (substYulBlock subst) def) -substYulStmt _ stmt = stmt -- YBreak, YContinue, YLeave, YComment unchanged + let cases' = map (\(lit, block) -> (lit, substYulBlock subst block)) cases + def' = fmap (substYulBlock subst) def + escaping = + foldMap (escapingAssignsYulBlock . snd) cases + `Set.union` maybe Set.empty escapingAssignsYulBlock def + in ( YSwitch (substYulExp subst e) cases' def', + dropSet escaping subst + ) +substYulStmt subst stmt = (stmt, subst) -- YBreak, YContinue, YLeave, YComment + +dropNames :: [Name] -> Map.Map Name YulExp -> Map.Map Name YulExp +dropNames names m = foldr Map.delete m names + +dropSet :: Set.Set Name -> Map.Map Name YulExp -> Map.Map Name YulExp +dropSet names m = Set.foldr Map.delete m names substYulExp :: Map.Map Name YulExp -> YulExp -> YulExp substYulExp subst (YIdent n) = Map.findWithDefault (YIdent n) n subst substYulExp subst (YCall op args) = YCall op (map (substYulExp subst) args) substYulExp _ e = e -- YLit, YMeta unchanged +-- | Names @let@-bound at the top level of a block; these are the only ones a +-- @for@ pre-block puts in scope for the rest of the loop. +letBoundYulBlock :: [YulStmt] -> Set.Set Name +letBoundYulBlock = foldMap letBound + where + letBound (YLet names _) = Set.fromList names + letBound _ = Set.empty + +-- | Names assigned inside a block that refer to a variable declared outside it, +-- i.e. assignments whose effect escapes the block's own scope. A name that is +-- @let@-bound anywhere within the block is local, so it is excluded — dropping +-- an outer literal for a purely local reassignment would be both unnecessary +-- and unsafe (the outer name may be an eliminated comptime value still read +-- after the block). Yul functions have an isolated scope, so their bodies are +-- not traversed. +escapingAssignsYulBlock :: [YulStmt] -> Set.Set Name +escapingAssignsYulBlock block = + assignedYulBlock block `Set.difference` letBoundDeepYulBlock block + +assignedYulBlock :: [YulStmt] -> Set.Set Name +assignedYulBlock = foldMap assignedYulStmt + +assignedYulStmt :: YulStmt -> Set.Set Name +assignedYulStmt (YAssign names _) = Set.fromList names +assignedYulStmt (YIf _ block) = assignedYulBlock block +assignedYulStmt (YBlock stmts) = assignedYulBlock stmts +assignedYulStmt (YFor pre _ post b) = + assignedYulBlock pre `Set.union` assignedYulBlock post `Set.union` assignedYulBlock b +assignedYulStmt (YSwitch _ cases def) = + foldMap (assignedYulBlock . snd) cases + `Set.union` maybe Set.empty assignedYulBlock def +assignedYulStmt (YFun {}) = Set.empty -- isolated scope +assignedYulStmt _ = Set.empty + +letBoundDeepYulBlock :: [YulStmt] -> Set.Set Name +letBoundDeepYulBlock = foldMap go + where + go (YLet names _) = Set.fromList names + go (YIf _ block) = letBoundDeepYulBlock block + go (YBlock stmts) = letBoundDeepYulBlock stmts + go (YFor pre _ post b) = + letBoundDeepYulBlock pre + `Set.union` letBoundDeepYulBlock post + `Set.union` letBoundDeepYulBlock b + go (YSwitch _ cases def) = + foldMap (letBoundDeepYulBlock . snd) cases + `Set.union` maybe Set.empty letBoundDeepYulBlock def + go (YFun {}) = Set.empty -- isolated scope + go _ = Set.empty + -- | Merge a YulState back into VEnv, using TypeReg to find the right MastIds. -- Only names present in TypeReg are merged; others are silently ignored. mergeYulStateToVEnv :: TypeReg -> YulState -> VEnv -> VEnv diff --git a/test/YulEvalTests.hs b/test/YulEvalTests.hs index a4f28f4cb..1b9f1f8d5 100644 --- a/test/YulEvalTests.hs +++ b/test/YulEvalTests.hs @@ -30,6 +30,13 @@ yExp op args = YExp (YCall (Name op) args) st :: [(String, Integer)] -> YulState st = Map.fromList . map (\(n, v) -> (Name n, v)) +-- A name→literal substitution map, as built from a VEnv before an asm block. +mkSubst :: [(String, Integer)] -> Map.Map Name YulExp +mkSubst = Map.fromList . map (\(n, v) -> (Name n, YLit (YulNumber v))) + +yLet :: String -> YulExp -> YulStmt +yLet n e = YLet [Name n] (Just e) + -- Run an EvalM action in non-comptime mode (memory ops inactive). runPure :: EvalM a -> a runPure m = fst $ runEvalM (EvalEnv Map.empty Set.empty False) defaultFuel m @@ -56,6 +63,7 @@ yulEvalTests = evalYulOpTests, evalYulExpTests, evalYulBlockTests, + substYulBlockTests, memoryHelperTests, memoryEvalTests, asmIsInterpretableTests @@ -270,6 +278,93 @@ evalYulBlockTests = @?= Nothing ] +----------------------------------------------------------------------- +-- substYulBlock: scope- and flow-aware inlining of comptime literals +----------------------------------------------------------------------- + +substYulBlockTests :: TestTree +substYulBlockTests = + testGroup + "substYulBlock (scope/flow-aware substitution)" + [ testCase "an unassigned variable is still inlined" $ + substYulBlock + (mkSubst [("x", 0)]) + [yAssign "z" (yCall "add" [yIdent "x", yNum 1])] + @?= [yAssign "z" (yCall "add" [yNum 0, yNum 1])], + -- Flow: after `x := 5`, `x` holds a new runtime value, so the pre-block + -- literal must not be inlined into the following `add(x, 1)`. + testCase "a reassigned variable is not inlined downstream" $ + let block = + [ yAssign "x" (yNum 5), + yAssign "y" (yCall "add" [yIdent "x", yNum 1]) + ] + in substYulBlock (mkSubst [("x", 0), ("y", 0)]) block @?= block, + -- Shadowing: the asm-local `let i` owns the name for the rest of the + -- block, so `add(i, 1)` must read the local, not the outer literal. + testCase "a plain asm-local let shadows the outer literal" $ + let block = + [ yLet "i" (yNum 7), + yAssign "r" (yCall "add" [yIdent "i", yNum 1]) + ] + in substYulBlock (mkSubst [("i", 0)]) block @?= block, + -- ...but the let's initialiser is still evaluated in the outer scope. + testCase "a let initialiser is inlined from the outer scope" $ + substYulBlock + (mkSubst [("x", 9)]) + [yLet "i" (yIdent "x"), yAssign "r" (yIdent "i")] + @?= [yLet "i" (yNum 9), yAssign "r" (yIdent "i")], + -- The reported infinite-loop case: the for-counter is `let`-bound in the + -- pre-block, so neither the condition nor the body may inline the outer 0. + testCase "a for-loop counter shadowed by its pre-let is not inlined" $ + let block = + [ YFor + [yLet "i" (yNum 0)] + (yCall "lt" [yIdent "i", yNum 3]) + [yAssign "i" (yCall "add" [yIdent "i", yNum 1])] + [yAssign "r" (yIdent "i")] + ] + in substYulBlock (mkSubst [("i", 0)]) block @?= block, + -- A variable assigned inside the loop is not loop-invariant either. + testCase "a variable assigned in a for-body is not inlined into it" $ + let block = + [ YFor + [] + (yCall "lt" [yIdent "n", yNum 3]) + [] + [yAssign "s" (yCall "add" [yIdent "s", yNum 1])] + ] + in substYulBlock (mkSubst [("s", 0)]) block @?= block, + -- Function parameters and returns shadow within the body. + testCase "function parameters and returns shadow within the body" $ + let block = + [ YFun + (Name "f") + [Name "a"] + (Just [Name "r"]) + [yAssign "r" (yCall "add" [yIdent "a", yNum 1])] + ] + in substYulBlock (mkSubst [("a", 0), ("r", 0)]) block @?= block, + -- ...but a function definition does not disturb the enclosing scope: a + -- statement after it still sees the outer binding. + testCase "a function definition does not leak its shadowing outward" $ + substYulBlock + (mkSubst [("a", 0)]) + [ YFun (Name "f") [Name "a"] (Just [Name "r"]) [yAssign "r" (yIdent "a")], + yAssign "z" (yIdent "a") + ] + @?= [ YFun (Name "f") [Name "a"] (Just [Name "r"]) [yAssign "r" (yIdent "a")], + yAssign "z" (yNum 0) + ], + -- An assignment to an outer variable inside a nested block escapes and + -- invalidates the literal for statements after the block. + testCase "an assignment inside an if escapes the block" $ + let block = + [ YIf (yIdent "flag") [yAssign "x" (yNum 5)], + yAssign "y" (yIdent "x") + ] + in substYulBlock (mkSubst [("x", 0)]) block @?= block + ] + ----------------------------------------------------------------------- -- Memory helpers (pure functions: mstoreBytes, mloadWord) -----------------------------------------------------------------------