Skip to content

Commit 27aefc5

Browse files
msoosethmsooseth
authored
Merge pull request #673 from ethereum/more-symbolic
More symbolic overapproximation when the remote contract cannot be fetched, adding CodeHash SMT representation
2 parents 2716b1b + 51e4c85 commit 27aefc5

File tree

5 files changed

+153
-5
lines changed

5 files changed

+153
-5
lines changed

‎CHANGELOG.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
3737
but allows much more thorough exploration of the contract
3838
- Allow controlling the max buffer sizes via --max-buf-size to something smaller than 2**64
3939
so we don't get too large buffers as counterexamples
40+
- More symbolic overapproximation for Balance and ExtCodeHash opcodes, fixing
41+
CodeHash SMT representation
4042

4143

4244
## Fixed

‎src/EVM.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -450,7 +450,7 @@ exec1 conf = do
450450
case stk of
451451
x:xs -> forceAddr x (freshVarFallback xs) $ \a ->
452452
accessAndBurn a $
453-
fetchAccount a $ \c -> do
453+
fetchAccountWithFallback a (freshVarFallback xs) $ \c -> do
454454
next
455455
assign (#state % #stack) xs
456456
pushSym c.balance
@@ -568,9 +568,9 @@ exec1 conf = do
568568
case stk of
569569
x':xs -> forceAddr x' (freshVarFallback xs) $ \x ->
570570
accessAndBurn x $ do
571-
next
572-
assign (#state % #stack) xs
573-
fetchAccount x $ \c ->
571+
fetchAccountWithFallback x (freshVarFallback xs) $ \c -> do
572+
next
573+
assign (#state % #stack) xs
574574
if accountEmpty c
575575
then push (W256 0)
576576
else case view bytecode c of

‎src/EVM/Fetch.hs‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ import Numeric.Natural (Natural)
2727
import System.Environment (lookupEnv, getEnvironment)
2828
import System.Process
2929
import Control.Monad.IO.Class
30+
import Control.Monad (when)
3031
import EVM.Effects
3132
import qualified EVM.Expr as Expr
3233

@@ -214,6 +215,8 @@ oracle solvers info q = do
214215
continue <$> getSolutions solvers symExpr numBytes pathconds
215216

216217
PleaseFetchContract addr base continue -> do
218+
conf <- readConfig
219+
when (conf.debug) $ liftIO $ putStrLn $ "Fetching contract at " ++ show addr
217220
contract <- case info of
218221
Nothing -> let
219222
c = case base of
@@ -225,7 +228,9 @@ oracle solvers info q = do
225228
Just x -> pure $ continue x
226229
Nothing -> internalError $ "oracle error: " ++ show q
227230

228-
PleaseFetchSlot addr slot continue ->
231+
PleaseFetchSlot addr slot continue -> do
232+
conf <- readConfig
233+
when (conf.debug) $ liftIO $ putStrLn $ "Fetching slot " <> (show slot) <> " at " <> (show addr)
229234
case info of
230235
Nothing -> pure (continue 0)
231236
Just (n, url) ->

‎src/EVM/SMT.hs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -325,6 +325,7 @@ referencedFrameContext expr = nubOrd $ foldTerm go [] expr
325325
TxValue -> [(fromString "txvalue", [])]
326326
v@(Balance a) -> [(fromString "balance_" <> formatEAddr a, [PLT v (Lit $ 2 ^ (96 :: Int))])]
327327
Gas freshVar -> [(fromString ("gas_" <> show freshVar), [])]
328+
CodeHash a@(LitAddr _) -> [(fromString "codehash_" <> formatEAddr a, [])]
328329
_ -> []
329330

330331
referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]
@@ -872,6 +873,7 @@ exprToSMT = \case
872873
SLoad idx store -> op2 "select" store idx
873874
LitAddr n -> pure $ fromLazyText $ "(_ bv" <> T.pack (show (into n :: Integer)) <> " 160)"
874875
Gas freshVar -> pure $ fromLazyText $ "gas_" <> (T.pack $ show freshVar)
876+
CodeHash a@(LitAddr _) -> pure $ fromLazyText "codehash_" <> formatEAddr a
875877

876878
a -> internalError $ "TODO: implement: " <> show a
877879
where
@@ -1066,6 +1068,7 @@ parseTxCtx name
10661068
| name == "txvalue" = TxValue
10671069
| Just a <- TS.stripPrefix "balance_" name = Balance (parseEAddr a)
10681070
| Just a <- TS.stripPrefix "gas_" name = Gas (textToInt a)
1071+
| Just a <- TS.stripPrefix "codehash_" name = CodeHash (parseEAddr a)
10691072
| otherwise = internalError $ "cannot parse " <> (TS.unpack name) <> " into an Expr"
10701073

10711074
getAddrs :: (TS.Text -> Expr EAddr) -> (Text -> IO Text) -> [TS.Text] -> IO (Map (Expr EAddr) Addr)

‎test/test.hs‎

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2614,6 +2614,144 @@ tests = testGroup "hevm"
26142614
assertEqualM "number of errors" 0 numErrs
26152615
assertEqualM "number of counterexamples" 1 numCexes
26162616
assertEqualM "number of qed-s" 0 numQeds
2617+
, test "call-balance-symb" $ do
2618+
Just c <- solcRuntime "C"
2619+
[i|
2620+
contract C {
2621+
function checkval(address inputAddr) public {
2622+
uint256 balance = inputAddr.balance;
2623+
assert(balance < 10);
2624+
}
2625+
}
2626+
|]
2627+
let sig = Just (Sig "checkval(address)" [AbiAddressType])
2628+
(expr, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
2629+
let numCexes = sum $ map (fromEnum . isCex) ret
2630+
let numErrs = sum $ map (fromEnum . isError) ret
2631+
assertBoolM "The expression MUST NOT be partial" $ Prelude.not (Expr.containsNode isPartial expr)
2632+
assertEqualM "number of errors" 0 numErrs
2633+
assertEqualM "number of counterexamples" 1 numCexes
2634+
, test "call-balance-symb2" $ do
2635+
Just c <- solcRuntime "C"
2636+
[i|
2637+
contract C {
2638+
function checkval() public {
2639+
uint256 balance = address(0xacab).balance;
2640+
assert(balance < 10);
2641+
}
2642+
}
2643+
|]
2644+
let sig = Just (Sig "checkval()" [])
2645+
(expr, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
2646+
let numCexes = sum $ map (fromEnum . isCex) ret
2647+
let numErrs = sum $ map (fromEnum . isError) ret
2648+
assertBoolM "The expression MUST NOT be partial" $ Prelude.not (Expr.containsNode isPartial expr)
2649+
assertEqualM "number of errors" 0 numErrs
2650+
assertEqualM "number of counterexamples" 1 numCexes
2651+
, test "call-balance-concrete-pass" $ do
2652+
Just c <- solcRuntime "C"
2653+
[i|
2654+
interface Vm {
2655+
function deal(address,uint256) external;
2656+
}
2657+
contract Target {
2658+
}
2659+
contract C {
2660+
function checkval() public {
2661+
Target t = new Target();
2662+
Vm vm = Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
2663+
vm.deal(address(t), 5);
2664+
uint256 balance = address(t).balance;
2665+
assert(balance < 10);
2666+
}
2667+
}
2668+
|]
2669+
let sig = Just (Sig "checkval()" [])
2670+
(expr, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
2671+
let numErrs = sum $ map (fromEnum . isError) ret
2672+
let numQeds = sum $ map (fromEnum . isQed) ret
2673+
assertBoolM "The expression MUST NOT be partial" $ Prelude.not (Expr.containsNode isPartial expr)
2674+
assertEqualM "number of errors" 0 numErrs
2675+
assertEqualM "number of qed-s" 1 numQeds
2676+
, test "call-balance-concrete-fail" $ do
2677+
Just c <- solcRuntime "C"
2678+
[i|
2679+
interface Vm {
2680+
function deal(address,uint256) external;
2681+
}
2682+
contract Target {
2683+
}
2684+
contract C {
2685+
function checkval() public {
2686+
Target t = new Target();
2687+
Vm vm = Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D);
2688+
vm.deal(address(t), 5);
2689+
uint256 balance = address(t).balance;
2690+
assert(balance < 5);
2691+
}
2692+
}
2693+
|]
2694+
let sig = Just (Sig "checkval()" [])
2695+
(expr, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
2696+
let numErrs = sum $ map (fromEnum . isError) ret
2697+
let numCexes = sum $ map (fromEnum . isCex) ret
2698+
assertBoolM "The expression MUST NOT be partial" $ Prelude.not (Expr.containsNode isPartial expr)
2699+
assertEqualM "number of errors" 0 numErrs
2700+
assertEqualM "number of counterexamples" 1 numCexes
2701+
, test "call-extcodehash-symb1" $ do
2702+
Just c <- solcRuntime "C"
2703+
[i|
2704+
contract C {
2705+
function checkval(address inputAddr) public {
2706+
bytes32 hash = inputAddr.codehash;
2707+
assert(uint(hash) < 10);
2708+
}
2709+
}
2710+
|]
2711+
let sig = Just (Sig "checkval(address)" [AbiAddressType])
2712+
(expr, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
2713+
let numCexes = sum $ map (fromEnum . isCex) ret
2714+
let numErrs = sum $ map (fromEnum . isError) ret
2715+
assertBoolM "The expression MUST NOT be partial" $ Prelude.not (Expr.containsNode isPartial expr)
2716+
assertEqualM "number of errors" 0 numErrs
2717+
assertEqualM "number of counterexamples" 1 numCexes
2718+
, test "call-extcodehash-symb2" $ do
2719+
Just c <- solcRuntime "C"
2720+
[i|
2721+
contract C {
2722+
function checkval() public {
2723+
bytes32 hash = address(0xacab).codehash;
2724+
assert(uint(hash) < 10);
2725+
}
2726+
}
2727+
|]
2728+
let sig = Just (Sig "checkval()" [])
2729+
(expr, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
2730+
let numCexes = sum $ map (fromEnum . isCex) ret
2731+
let numErrs = sum $ map (fromEnum . isError) ret
2732+
assertBoolM "The expression MUST NOT be partial" $ Prelude.not (Expr.containsNode isPartial expr)
2733+
assertEqualM "number of errors" 0 numErrs
2734+
assertEqualM "number of counterexamples" 1 numCexes
2735+
, test "call-extcodehash-concrete-fail" $ do
2736+
Just c <- solcRuntime "C"
2737+
[i|
2738+
contract Target {
2739+
}
2740+
contract C {
2741+
function checkval() public {
2742+
Target t = new Target();
2743+
bytes32 hash = address(t).codehash;
2744+
assert(uint(hash) == 8);
2745+
}
2746+
}
2747+
|]
2748+
let sig = Just (Sig "checkval()" [])
2749+
(expr, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
2750+
let numErrs = sum $ map (fromEnum . isError) ret
2751+
let numCexes = sum $ map (fromEnum . isCex) ret
2752+
assertBoolM "The expression MUST NOT be partial" $ Prelude.not (Expr.containsNode isPartial expr)
2753+
assertEqualM "number of errors" 0 numErrs
2754+
assertEqualM "number of counterexamples" 1 numCexes
26172755
, test "jump-symbolic" $ do
26182756
Just c <- solcRuntime "C"
26192757
[i|

0 commit comments

Comments
 (0)