Remove SBV from the SMT backend

Makefile

@@ -54,7 +54,8 @@ test-parse: parser compiler $(parser_pass:=.parse.pass) $(parser_fail:=.parse.fa
 test-type: parser compiler $(typing_pass:=.type.pass) $(typing_fail:=.type.fail)
 test-invariant: parser compiler $(invariant_pass:=.invariant.pass) $(invariant_fail:=.invariant.fail)
 test-hevm: parser compiler $(hevm_pass:=.hevm.pass) $(hevm_fail:=.hevm.fail)
-
+test-cabal: src/*.hs
+	cd src && cabal v2-run test
 
 # Just checks parsing
 tests/%.parse.pass:
@@ -91,4 +92,4 @@ tests/hevm/fail/%.act.hevm.fail:
 	./bin/act hevm --spec tests/hevm/fail/$*.act --soljson tests/hevm/fail/$*.sol.json && exit 1 || echo 0
 	rm tests/hevm/fail/$*.sol.json
 
-test: test-parse test-type test-invariant test-coq test-hevm
+test: test-parse test-type test-invariant test-coq test-hevm test-cabal

default.nix

@@ -12,11 +12,11 @@ let
       hevm = dapptools.haskellPackages.hevm;
       sbv = dapptools.haskellPackages.sbv;
       act =
-        hself.callCabal2nixWithOptions
+        pkgs.haskell.lib.dontCheck (hself.callCabal2nixWithOptions
           "act"
           (gitignore ./src)
           "-fci"
-          {};
+          {});
     };
   };
 
@@ -27,6 +27,8 @@ let
     buildInputs = with pkgs.haskellPackages; [
       cabal-install
       pkgs.jq
+      pkgs.z3
+      pkgs.cvc4
       pkgs.coq_8_10
       dapptools.solc
     ];

src/Enrich.hs

@@ -10,7 +10,7 @@ import EVM.ABI (AbiType(..))
 import EVM.Solidity (SlotType(..))
 
 import RefinedAst
-import Type (bound, defaultStore, metaType)
+import Type (bound, defaultStore)
 import Syntax (EthEnv(..), Id, Decl(..), Interface(..))
 import Extract
 
@@ -21,41 +21,42 @@ enrich claims = [S store]
                 <> (C <$> (enrichConstructor store <$> constructors))
                 <> (B <$> (enrichBehaviour store <$> behaviours))
   where
-    store = head $ [s | S s <- claims]
+    store = head [s | S s <- claims]
     behaviours = [b | B b <- claims]
     invariants = [i | I i <- claims]
     constructors = [c | C c <- claims]
-    definition (Invariant c _ _) = head $ filter (\b -> Pass == _cmode b && _cname b == c) [c' | C c' <- claims]
+    definition (Invariant c _ _ _) = head [c' | c' <- constructors, _cmode c' == Pass, _cname c' == c]
 
 -- |Adds type bounds for calldata , environment vars, and external storage vars as preconditions
 enrichConstructor :: Store -> Constructor -> Constructor
 enrichConstructor store ctor@(Constructor _ _ (Interface _ decls) pre _ _ storageUpdates) =
   ctor { _cpreconditions = pre' }
     where
       pre' = pre
-             <> (mkCallDataBounds decls)
-             <> (mkStorageBounds store storageUpdates)
-             <> (mkEthEnvBounds $ ethEnvFromConstructor ctor)
+             <> mkCallDataBounds decls
+             <> mkStorageBounds store storageUpdates
+             <> mkEthEnvBounds (ethEnvFromConstructor ctor)
 
 -- | Adds type bounds for calldata, environment vars, and storage vars as preconditions
 enrichBehaviour :: Store -> Behaviour -> Behaviour
 enrichBehaviour store behv@(Behaviour _ _ _ (Interface _ decls) pre _ stateUpdates _) =
   behv { _preconditions = pre' }
     where
       pre' = pre
-             <> (mkCallDataBounds decls)
-             <> (mkStorageBounds store stateUpdates)
-             <> (mkEthEnvBounds $ ethEnvFromBehaviour behv)
+             <> mkCallDataBounds decls
+             <> mkStorageBounds store stateUpdates
+             <> mkEthEnvBounds (ethEnvFromBehaviour behv)
 
--- | Adds type bounds for calldata, environment vars, and storage vars as preconditions
+-- | Adds type bounds for calldata, environment vars, and storage vars
 enrichInvariant :: Store -> Constructor -> Invariant -> Invariant
-enrichInvariant store (Constructor _ _ (Interface _ decls) _ _ _ _) inv@(Invariant _ conds predicate) =
-  inv { _ipreconditions = conds' }
+enrichInvariant store (Constructor _ _ (Interface _ decls) _ _ _ _) inv@(Invariant _ preconds storagebounds predicate) =
+  inv { _ipreconditions = preconds', _istoragebounds = storagebounds' }
     where
-      conds' = conds
-               <> (mkCallDataBounds decls)
-               <> (mkStorageBounds store (Left <$> locsFromExp predicate))
-               <> (mkEthEnvBounds $ ethEnvFromExp predicate)
+      preconds' = preconds
+                  <> mkCallDataBounds decls
+                  <> mkEthEnvBounds (ethEnvFromExp predicate)
+      storagebounds' = storagebounds
+                       <> mkStorageBounds store (Left <$> locsFromExp predicate)
 
 mkEthEnvBounds :: [EthEnv] -> [Exp Bool]
 mkEthEnvBounds vars = catMaybes $ mkBound <$> nub vars

src/Extract.hs

@@ -6,6 +6,7 @@ import qualified Data.List.NonEmpty as NonEmpty
 
 import RefinedAst
 import Syntax
+import EVM.ABI (AbiType(..))
 
 locsFromReturnExp :: ReturnExp -> [StorageLocation]
 locsFromReturnExp (ExpInt e) = locsFromExp e
@@ -43,10 +44,10 @@ locsFromExp e = case e of
   IntVar _  -> []
   LitBool _ -> []
   BoolVar _ -> []
-  NewAddr _ _ -> error "TODO: handle new addr in SMT expressions"
+  NewAddr a b -> locsFromExp a <> locsFromExp b
   IntEnv _ -> []
   ByEnv _ -> []
-  ITE x y z -> (locsFromExp x) <> (locsFromExp y) <> (locsFromExp z)
+  ITE x y z -> locsFromExp x <> locsFromExp y <> locsFromExp z
   TEntry a -> case a of
     DirectInt contract name -> [IntLoc $ DirectInt contract name]
     DirectBool contract slot -> [BoolLoc $ DirectBool contract slot]
@@ -138,6 +139,19 @@ mkLoc (IntUpdate item _) = IntLoc item
 mkLoc (BoolUpdate item _) = BoolLoc item
 mkLoc (BytesUpdate item _) = BytesLoc item
 
+metaType :: AbiType -> MType
+metaType (AbiUIntType _)     = Integer
+metaType (AbiIntType  _)     = Integer
+metaType AbiAddressType      = Integer
+metaType AbiBoolType         = Boolean
+metaType (AbiBytesType _)    = ByteStr
+metaType AbiBytesDynamicType = ByteStr
+metaType AbiStringType       = ByteStr
+--metaType (AbiArrayDynamicType a) =
+--metaType (AbiArrayType        Int AbiType
+--metaType (AbiTupleType        (Vector AbiType)
+metaType _ = error "Extract.metaType: TODO"
+
 nameFromStorage :: Syntax.Storage -> Id
 nameFromStorage (Rewrite (Entry _ name _) _) = name
 nameFromStorage (Constant (Entry _ name _)) = name

src/HEVM.hs

@@ -1,31 +1,37 @@
 {-# Language RecordWildCards #-}
 {-# Language TypeApplications #-}
 {-# Language OverloadedStrings #-}
+{-# Language ScopedTypeVariables #-}
 {-# Language DataKinds #-}
 {-# Language GADTs #-}
 
 module HEVM where
 
 import Prelude hiding (lookup)
-import Syntax
+import Syntax hiding (Post)
 import RefinedAst hiding (S)
 import Extract
 
+import Data.ByteString (ByteString)
+import Data.ByteString.UTF8 (toString)
 import Data.Text (Text, pack, splitOn)
 import Data.Maybe
 import Data.Either
 import Data.List hiding (lookup)
-import Data.Map hiding (drop, null, findIndex, splitAt, foldl, filter)
+import qualified Data.List.NonEmpty as NonEmpty (toList)
+import Data.Map hiding (drop, null, findIndex, splitAt, foldl, foldr, filter)
 import qualified Data.Map as Map
 import Control.Monad.State.Strict (execState)
 import Data.SBV.Control
 import Data.SBV
-import Control.Lens hiding (pre)
+import Data.SBV.String ((.++), subStr)
+import Control.Lens hiding (pre, (.>))
 import Control.Monad
 import qualified Data.Vector as Vec
+import Data.Type.Equality
+import Data.Typeable
 
-import Prove
-import Type
+import Print
 
 import EVM hiding (Query)
 import EVM.VMTest
@@ -283,3 +289,201 @@ keccak' (SymbolicBuffer bytes) = case maybeLitBytes bytes of
   Nothing -> symkeccak' bytes
   Just bs -> keccak' (ConcreteBuffer bs)
 keccak' (ConcreteBuffer bytes) = literal $ toSizzle $ wordValue $ keccakBlob bytes
+
+--- Symbolic Expression Generation ---
+
+data Ctx = Ctx ContractName Method Args HEVM.Storage HEVM.Env
+  deriving (Show)
+
+data SMType
+  = SymInteger (SBV Integer)
+  | SymBool (SBV Bool)
+  | SymBytes (SBV String)
+  deriving (Show)
+
+type ContractName = Id
+type Method = Id
+type Args = Map Id SMType
+type Storage = Map Id (SMType, SMType)
+type Env = Map Id SMType
+data When = Pre | Post
+
+symExp :: Ctx -> When -> ReturnExp -> SMType
+symExp ctx whn ret = case ret of
+  ExpInt e -> SymInteger $ symExpInt ctx whn e
+  ExpBool e -> SymBool $ symExpBool ctx whn e
+  ExpBytes e -> SymBytes $ symExpBytes ctx whn e
+
+symExpBool :: Ctx -> When -> Exp Bool -> SBV Bool
+symExpBool ctx@(Ctx c m args store _) w e = case e of
+  And a b   -> symExpBool ctx w a .&& symExpBool ctx w b
+  Or a b    -> symExpBool ctx w a .|| symExpBool ctx w b
+  Impl a b  -> symExpBool ctx w a .=> symExpBool ctx w b
+  LE a b    -> symExpInt ctx w a .< symExpInt ctx w b
+  LEQ a b   -> symExpInt ctx w a .<= symExpInt ctx w b
+  GE a b    -> symExpInt ctx w a .> symExpInt ctx w b
+  GEQ a b   -> symExpInt ctx w a .>= symExpInt ctx w b
+  NEq a b   -> sNot (symExpBool ctx w (Eq a b))
+  Neg a     -> sNot (symExpBool ctx w a)
+  LitBool a -> literal a
+  BoolVar a -> get (nameFromArg c m a) (catBools args)
+  TEntry a  -> get (nameFromItem m a) (catBools store')
+  ITE x y z -> ite (symExpBool ctx w x) (symExpBool ctx w y) (symExpBool ctx w z)
+  Eq (a :: Exp t) (b :: Exp t) -> case eqT @t @Integer of
+    Just Refl -> symExpInt ctx w a .== symExpInt ctx w b
+    Nothing -> case eqT @t @Bool of
+      Just Refl -> symExpBool ctx w a .== symExpBool ctx w b
+      Nothing -> case eqT @t @ByteString of
+        Just Refl -> symExpBytes ctx w a .== symExpBytes ctx w b
+        Nothing -> error "Internal Error: invalid expression type"
+ where store' = case w of
+         Pre -> fst <$> store
+         Post -> snd <$> store
+
+symExpInt :: Ctx -> When -> Exp Integer -> SBV Integer
+symExpInt ctx@(Ctx c m args store environment) w e = case e of
+  Add a b   -> symExpInt ctx w a + symExpInt ctx w b
+  Sub a b   -> symExpInt ctx w a - symExpInt ctx w b
+  Mul a b   -> symExpInt ctx w a * symExpInt ctx w b
+  Div a b   -> symExpInt ctx w a `sDiv` symExpInt ctx w b
+  Mod a b   -> symExpInt ctx w a `sMod` symExpInt ctx w b
+  Exp a b   -> symExpInt ctx w a .^ symExpInt ctx w b
+  LitInt a  -> literal a
+  IntMin a  -> literal $ intmin a
+  IntMax a  -> literal $ intmax a
+  UIntMin a -> literal $ uintmin a
+  UIntMax a -> literal $ uintmax a
+  IntVar a  -> get (nameFromArg c m a) (catInts args)
+  TEntry a  -> get (nameFromItem m a) (catInts store')
+  IntEnv a -> get (nameFromEnv c m a) (catInts environment)
+  NewAddr _ _ -> error "TODO: handle new addr in SMT expressions"
+  ITE x y z -> ite (symExpBool ctx w x) (symExpInt ctx w y) (symExpInt ctx w z)
+ where store' = case w of
+         Pre -> fst <$> store
+         Post -> snd <$> store
+
+symExpBytes :: Ctx -> When -> Exp ByteString -> SBV String
+symExpBytes ctx@(Ctx c m args store environment) w e = case e of
+  Cat a b -> symExpBytes ctx w a .++ symExpBytes ctx w b
+  ByVar a  -> get (nameFromArg c m a) (catBytes args)
+  ByStr a -> literal a
+  ByLit a -> literal $ toString a
+  TEntry a  -> get (nameFromItem m a) (catBytes store')
+  Slice a x y -> subStr (symExpBytes ctx w a) (symExpInt ctx w x) (symExpInt ctx w y)
+  ByEnv a -> get (nameFromEnv c m a) (catBytes environment)
+  ITE x y z -> ite (symExpBool ctx w x) (symExpBytes ctx w y) (symExpBytes ctx w z)
+ where store' = case w of
+         Pre -> fst <$> store
+         Post -> snd <$> store
+
+
+-- *** SMT Variable Names *** --
+
+
+nameFromItem :: Method -> TStorageItem a -> Id
+nameFromItem method item = case item of
+  DirectInt c name -> c @@ method @@ name
+  DirectBool c name -> c @@ method @@ name
+  DirectBytes c name -> c @@ method @@ name
+  MappedInt c name ixs -> c @@ method @@ name >< showIxs c ixs
+  MappedBool c name ixs -> c @@ method @@ name >< showIxs c ixs
+  MappedBytes c name ixs -> c @@ method @@ name >< showIxs c ixs
+  where
+    x >< y = x <> "-" <> y
+    showIxs c ixs = intercalate "-" (NonEmpty.toList $ nameFromExp c method <$> ixs)
+
+nameFromExp :: ContractName -> Method -> ReturnExp -> Id
+nameFromExp c method e = case e of
+  ExpInt e' -> nameFromExpInt c method e'
+  ExpBool e' -> nameFromExpBool c method e'
+  ExpBytes e' -> nameFromExpBytes c method e'
+
+nameFromExpInt :: ContractName -> Method -> Exp Integer -> Id
+nameFromExpInt c m e = case e of
+  Add a b   -> nameFromExpInt c m a <> "+" <> nameFromExpInt c m b
+  Sub a b   -> nameFromExpInt c m a <> "-" <> nameFromExpInt c m b
+  Mul a b   -> nameFromExpInt c m a <> "*" <> nameFromExpInt c m b
+  Div a b   -> nameFromExpInt c m a <> "/" <> nameFromExpInt c m b
+  Mod a b   -> nameFromExpInt c m a <> "%" <> nameFromExpInt c m b
+  Exp a b   -> nameFromExpInt c m a <> "^" <> nameFromExpInt c m b
+  LitInt a  -> show a
+  IntMin a  -> show $ intmin a
+  IntMax a  -> show $ intmax a
+  UIntMin a -> show $ uintmin a
+  UIntMax a -> show $ uintmax a
+  IntVar a  -> a
+  TEntry a  -> nameFromItem m a
+  IntEnv a -> nameFromEnv c m a
+  NewAddr _ _ -> error "TODO: handle new addr in SMT expressions"
+  ITE x y z -> "if-" <> nameFromExpBool c m x <> "-then-" <> nameFromExpInt c m y <> "-else-" <> nameFromExpInt c m z
+
+nameFromExpBool :: ContractName -> Method -> Exp Bool -> Id
+nameFromExpBool c m e = case e of
+  And a b   -> nameFromExpBool c m a <> "&&" <> nameFromExpBool c m b
+  Or a b    -> nameFromExpBool c m a <> "|" <> nameFromExpBool c m b
+  Impl a b  -> nameFromExpBool c m a <> "=>" <> nameFromExpBool c m b
+  LE a b    -> nameFromExpInt c m a <> "<" <> nameFromExpInt c m b
+  LEQ a b   -> nameFromExpInt c m a <> "<=" <> nameFromExpInt c m b
+  GE a b    -> nameFromExpInt c m a <> ">" <> nameFromExpInt c m b
+  GEQ a b   -> nameFromExpInt c m a <> ">=" <> nameFromExpInt c m b
+  Neg a     -> "~" <> nameFromExpBool c m a
+  LitBool a -> show a
+  BoolVar a -> nameFromArg c m a
+  TEntry a  -> nameFromItem m a
+  ITE x y z -> "if-" <> nameFromExpBool c m x <> "-then-" <> nameFromExpBool c m y <> "-else-" <> nameFromExpBool c m z
+  Eq (a :: Exp t) (b :: Exp t) -> case eqT @t @Integer of
+    Just Refl -> nameFromExpInt c m a <> "==" <> nameFromExpInt c m b
+    Nothing -> case eqT @t @Bool of
+      Just Refl -> nameFromExpBool c m a <> "==" <> nameFromExpBool c m b
+      Nothing -> case eqT @t @ByteString of
+        Just Refl -> nameFromExpBytes c m a <> "==" <> nameFromExpBytes c m b
+        Nothing -> error "Internal Error: invalid expression type"
+  NEq (a :: Exp t) (b :: Exp t) -> case eqT @t @Integer of
+    Just Refl -> nameFromExpInt c m a <> "=/=" <> nameFromExpInt c m b
+    Nothing -> case eqT @t @Bool of
+      Just Refl -> nameFromExpBool c m a <> "=/=" <> nameFromExpBool c m b
+      Nothing -> case eqT @t @ByteString of
+        Just Refl -> nameFromExpBytes c m a <> "=/=" <> nameFromExpBytes c m b
+        Nothing -> error "Internal Error: invalid expression type"
+
+nameFromExpBytes :: ContractName -> Method -> Exp ByteString -> Id
+nameFromExpBytes c m e = case e of
+  Cat a b -> nameFromExpBytes c m a <> "++" <> nameFromExpBytes c m b
+  ByVar a  -> nameFromArg c m a
+  ByStr a -> show a
+  ByLit a -> show a
+  TEntry a  -> nameFromItem m a
+  Slice a x y -> nameFromExpBytes c m a <> "[" <> show x <> ":" <> show y <> "]"
+  ByEnv a -> nameFromEnv c m a
+  ITE x y z -> "if-" <> nameFromExpBool c m x <> "-then-" <> nameFromExpBytes c m y <> "-else-" <> nameFromExpBytes c m z
+
+nameFromDecl :: ContractName -> Method -> Decl -> Id
+nameFromDecl c m (Decl _ name) = nameFromArg c m name
+
+nameFromArg :: ContractName -> Method -> Id -> Id
+nameFromArg c method name = c @@ method @@ name
+
+nameFromEnv :: ContractName -> Method -> EthEnv -> Id
+nameFromEnv c method e = c @@ method @@ (prettyEnv e)
+
+(@@) :: Id -> Id -> Id
+x @@ y = x <> "_" <> y
+
+
+-- *** Utils *** --
+
+
+get :: (Show a, Ord a, Show b) => a -> Map a b -> b
+get name vars = fromMaybe (error (show name <> " not found in " <> show vars)) $ Map.lookup name vars
+
+catInts :: Map Id SMType -> Map Id (SBV Integer)
+catInts m = Map.fromList [(name, i) | (name, SymInteger i) <- Map.toList m]
+
+catBools :: Map Id SMType -> Map Id (SBV Bool)
+catBools m = Map.fromList [(name, i) | (name, SymBool i) <- Map.toList m]
+
+catBytes :: Map Id SMType -> Map Id (SBV String)
+catBytes m = Map.fromList [(name, i) | (name, SymBytes i) <- Map.toList m]
+
+concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
+concatMapM f xs = liftM concat (mapM f xs)