Constant propagation over Props

CHANGELOG.md

@@ -16,6 +16,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   and continue running, whenever possible
 - STATICCALL abstraction is now performed in case of symbolic arguments
 - Better error messages for JSON parsing
+- Constant propagation for symbolic values
 
 ## Fixed
 - We now try to simplify expressions fully before trying to cast them to a concrete value

src/EVM/Expr.hs

@@ -1219,8 +1219,11 @@ simplify e = if (mapExpr go e == e)
 simplifyProps :: [Prop] -> [Prop]
 simplifyProps ps = if cannotBeSat then [PBool False] else simplified
   where
-    simplified = remRedundantProps . map simplifyProp . flattenProps $ ps
-    cannotBeSat = isUnsat simplified
+    simplified = if (goOne ps == ps) then ps else simplifyProps (goOne ps)
+    cannotBeSat = PBool False `elem` simplified
+    goOne :: [Prop] -> [Prop]
+    goOne = remRedundantProps . map simplifyProp . constPropagate . flattenProps
+
 
 -- | Evaluate the provided proposition down to its most concrete result
 -- Also simplifies the inner Expr, if it exists
@@ -1567,38 +1570,54 @@ data ConstState = ConstState
   }
   deriving (Show)
 
--- | Checks if a conjunction of propositions is definitely unsatisfiable
-isUnsat :: [Prop] -> Bool
-isUnsat ps = Prelude.not $ oneRun ps (ConstState mempty True)
+-- | Performs constant propagation
+constPropagate :: [Prop] -> [Prop]
+constPropagate ps =
+ let consts = collectConsts ps (ConstState mempty True)
+ in if consts.canBeSat then substitute consts ps ++ fixVals consts
+    else [PBool False]
   where
-    oneRun ps2 startState = (execState (mapM (go . simplifyProp) ps2) startState).canBeSat
+    -- Fixes the values of the constants
+    fixVals :: ConstState -> [Prop]
+    fixVals cs = Map.foldrWithKey (\k v acc -> peq (Lit v) k : acc) [] cs.values
+
+    -- Substitutes the constants in the props.
+    -- NOTE: will create PEq (Lit x) (Lit x) if x is a constant
+    --       hence we need the fixVals function to add them back in
+    substitute :: ConstState -> [Prop] -> [Prop]
+    substitute cs ps2 = map (mapProp (subsGo cs)) ps2
+    subsGo :: ConstState -> Expr a-> Expr a
+    subsGo cs (Var v) = case Map.lookup (Var v) cs.values of
+      Just x -> Lit x
+      Nothing -> Var v
+    subsGo _ x = x
+
+    -- Collects all the constants in the given props, and sets canBeSat to False if UNSAT
+    collectConsts ps2 startState = execState (mapM go ps2) startState
     go :: Prop -> State ConstState ()
     go = \case
-        -- PEq
         PEq (Lit l) a -> do
           s <- get
           case Map.lookup a s.values of
             Just l2 -> unless (l==l2) $ put ConstState {canBeSat=False, values=mempty}
             Nothing -> modify (\s' -> s'{values=Map.insert a l s'.values})
         PEq a b@(Lit _) -> go (PEq b a)
-        -- PNeg
         PNeg (PEq (Lit l) a) -> do
           s <- get
           case Map.lookup a s.values of
             Just l2 -> when (l==l2) $ put ConstState {canBeSat=False, values=mempty}
             Nothing -> pure ()
         PNeg (PEq a b@(Lit _)) -> go $ PNeg (PEq b a)
-        -- Others
         PAnd a b -> do
           go a
           go b
         POr a b -> do
           s <- get
           let
-            v1 = oneRun [a] s
-            v2 = oneRun [b] s
-          unless v1 $ go b
-          unless v2 $ go a
+            v1 = collectConsts [a] s
+            v2 = collectConsts [b] s
+          unless v1.canBeSat $ go b
+          unless v2.canBeSat $ go a
         PBool False -> put $ ConstState {canBeSat=False, values=mempty}
         _ -> pure ()
 

test/test.hs

@@ -777,28 +777,28 @@ tests = testGroup "hevm"
       test "disjunction-left-false" $ do
         let
           t = [PEq (Var "x") (Lit 1), POr (PEq (Var "x") (Lit 0)) (PEq (Var "y") (Lit 1)), PEq (Var "y") (Lit 2)]
-          cannotBeSat = Expr.isUnsat t
-        assertEqualM "Must be equal" cannotBeSat True
+          propagated = Expr.constPropagate t
+        assertEqualM "Must contain PBool False" True ((PBool False) `elem` propagated)
     , test "disjunction-right-false" $ do
         let
           t = [PEq (Var "x") (Lit 1), POr (PEq (Var "y") (Lit 1)) (PEq (Var "x") (Lit 0)), PEq (Var "y") (Lit 2)]
-          cannotBeSat = Expr.isUnsat t
-        assertEqualM "Must be equal" cannotBeSat True
+          propagated = Expr.constPropagate t
+        assertEqualM "Must contain PBool False" True ((PBool False) `elem` propagated)
     , test "disjunction-both-false" $ do
         let
           t = [PEq (Var "x") (Lit 1), POr (PEq (Var "x") (Lit 2)) (PEq (Var "x") (Lit 0)), PEq (Var "y") (Lit 2)]
-          cannotBeSat = Expr.isUnsat t
-        assertEqualM "Must be equal" cannotBeSat True
+          propagated = Expr.constPropagate t
+        assertEqualM "Must contain PBool False" True ((PBool False) `elem` propagated)
     , ignoreTest $ test "disequality-and-equality" $ do
         let
           t = [PNeg (PEq (Lit 1) (Var "arg1")), PEq (Lit 1) (Var "arg1")]
-          cannotBeSat = Expr.isUnsat t
-        assertEqualM "Must be equal" cannotBeSat True
+          propagated = Expr.constPropagate t
+        assertEqualM "Must contain PBool False" True ((PBool False) `elem` propagated)
     , test "equality-and-disequality" $ do
         let
           t = [PEq (Lit 1) (Var "arg1"), PNeg (PEq (Lit 1) (Var "arg1"))]
-          cannotBeSat = Expr.isUnsat t
-        assertEqualM "Must be equal" cannotBeSat True
+          propagated = Expr.constPropagate t
+        assertEqualM "Must contain PBool False" True ((PBool False) `elem` propagated)
   ]
   , testGroup "simpProp-concrete-tests" [
       test "simpProp-concrete-trues" $ do
@@ -866,6 +866,26 @@ tests = testGroup "hevm"
           t = [PEq (Or (Lit 2) (Lit 4)) (Lit 6)]
           simplified = Expr.simplifyProps t
         assertEqualM "Must be equal" [] simplified
+    , test "simpProp-constpropagate-1" $ do
+        let
+          -- 5+1 = 6
+          t = [PEq (Add (Lit 5) (Lit 1)) (Var "a"), PEq (Var "b") (Var "a")]
+          simplified = Expr.simplifyProps t
+        assertEqualM "Must be equal" [PEq (Lit 6) (Var "a"), PEq (Lit 6) (Var "b")] simplified
+    , test "simpProp-constpropagate-2" $ do
+        let
+          -- 5+1 = 6
+          t = [PEq (Add (Lit 5) (Lit 1)) (Var "a"), PEq (Var "b") (Var "a"), PEq (Var "c") (Sub (Var "b") (Lit 1))]
+          simplified = Expr.simplifyProps t
+        assertEqualM "Must be equal" [PEq (Lit 6) (Var "a"), PEq (Lit 6) (Var "b"), PEq (Lit 5) (Var "c")] simplified
+    , test "simpProp-constpropagate-3" $ do
+        let
+          t = [ PEq (Add (Lit 5) (Lit 1)) (Var "a") -- a = 6
+              , PEq (Var "b") (Var "a")             -- b = 6
+              , PEq (Var "c") (Sub (Var "b") (Lit 1)) -- c = 5
+              , PEq (Var "d") (Sub (Var "b") (Var "c"))] -- d = 1
+          simplified = Expr.simplifyProps t
+        assertEqualM "Must  know d == 1" ((PEq (Lit 1) (Var "d")) `elem` simplified) True
   ]
   , testGroup "MemoryTests"
     [ test "read-write-same-byte"  $ assertEqualM ""