Simplify exponentiation in SMT backend

src/RefinedAst.hs

@@ -10,15 +10,21 @@
 {-# Language ScopedTypeVariables #-}
 {-# Language TypeFamilies #-}
 {-# Language TypeApplications #-}
+{-# LANGUAGE MonadComprehensions #-}
 
 module RefinedAst where
 
+import Control.Applicative (empty)
+
+import Data.List (genericDrop,genericTake)
 import Data.Text (pack)
 import Data.Type.Equality
 import Data.Typeable
 import Data.Map.Strict (Map)
 import Data.List.NonEmpty hiding (fromList)
 import Data.ByteString (ByteString)
+import qualified Data.ByteString as BS
+import Data.String (fromString)
 
 import EVM.Solidity (SlotType(..))
 
@@ -149,8 +155,8 @@ data Exp t where
   NewAddr :: Exp Integer -> Exp Integer -> Exp Integer
 
   -- polymorphic
-  Eq  :: (Typeable t, ToJSON (Exp t)) => Exp t -> Exp t -> Exp Bool
-  NEq :: (Typeable t, ToJSON (Exp t)) => Exp t -> Exp t -> Exp Bool
+  Eq  :: (Eq t, Typeable t, ToJSON (Exp t)) => Exp t -> Exp t -> Exp Bool
+  NEq :: (Eq t, Typeable t, ToJSON (Exp t)) => Exp t -> Exp t -> Exp Bool
   ITE :: Exp Bool -> Exp t -> Exp t -> Exp t
   TEntry :: (TStorageItem t) -> Exp t
 
@@ -215,6 +221,52 @@ data ReturnExp
   | ExpBytes  (Exp ByteString)
   deriving (Eq, Show)
 
+-- | Simplifies concrete expressions into literals.
+-- Returns `Nothing` if the expression contains symbols.
+eval :: Exp a -> Maybe a
+eval e = case e of
+  And  a b    -> [a' && b' | a' <- eval a, b' <- eval b]
+  Or   a b    -> [a' || b' | a' <- eval a, b' <- eval b]
+  Impl a b    -> [a' <= b' | a' <- eval a, b' <- eval b]
+  Neg  a      -> not <$> eval a
+  LE   a b    -> [a' <  b' | a' <- eval a, b' <- eval b]
+  LEQ  a b    -> [a' <= b' | a' <- eval a, b' <- eval b]
+  GE   a b    -> [a' >  b' | a' <- eval a, b' <- eval b]
+  GEQ  a b    -> [a' >= b' | a' <- eval a, b' <- eval b]
+  LitBool a   -> pure a
+  BoolVar _   -> empty
+
+  Add a b     -> [a' + b'     | a' <- eval a, b' <- eval b]
+  Sub a b     -> [a' - b'     | a' <- eval a, b' <- eval b]
+  Mul a b     -> [a' * b'     | a' <- eval a, b' <- eval b]
+  Div a b     -> [a' `div` b' | a' <- eval a, b' <- eval b]
+  Mod a b     -> [a' `mod` b' | a' <- eval a, b' <- eval b]
+  Exp a b     -> [a' ^ b'     | a' <- eval a, b' <- eval b]
+  LitInt a    -> pure a
+  IntVar _    -> empty
+  IntEnv _    -> empty
+  IntMin  a   -> pure . negate $ 2 ^ (a - 1)
+  IntMax  a   -> pure $ 2 ^ (a - 1) - 1
+  UIntMin _   -> pure 0
+  UIntMax a   -> pure $ 2 ^ a - 1
+
+  Cat s t     -> [s' <> t' | s' <- eval s, t' <- eval t]
+  Slice s a b -> [BS.pack . genericDrop a' . genericTake b' $ s'
+                           | s' <- BS.unpack <$> eval s
+                           , a' <- eval a
+                           , b' <- eval b]
+  ByVar _     -> empty
+  ByStr s     -> pure . fromString $ s
+  ByLit s     -> pure s
+  ByEnv _     -> empty
+
+  NewAddr _ _ -> empty
+
+  Eq a b      -> [a' == b' | a' <- eval a, b' <- eval b]
+  NEq a b     -> [a' /= b' | a' <- eval a, b' <- eval b]
+  ITE a b c   -> eval a >>= \cond -> if cond then eval b else eval c
+  TEntry _    -> empty
+
 -- intermediate json output helpers ---
 instance ToJSON Claim where
   toJSON (S storages) = object [ "kind" .= (String "Storages")

src/SMT.hs

@@ -1,7 +1,10 @@
 {-# LANGUAGE GADTs #-}
+{-# LANGUAGE MonadComprehensions #-}
 
 module SMT (Solver(..), SMTConfig(..), Query(..), SMTResult(..), runSMT, runQuery, mkPostconditionQueries, mkInvariantQueries, getTarget, getSMT) where
 
+import Control.Applicative ((<|>))
+
 import Data.Map (Map)
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Maybe
@@ -406,10 +409,12 @@ expToSMT2 ctx@(Ctx behvName whn) e = case e of
 
 -- | SMT2 has no support for exponentiation, but we can do some preprocessing
 --   if the RHS is concrete to provide some limited support for exponentiation
---   TODO: support any exponentiation expression where the RHS evaluates to a concrete value
 simplifyExponentiation :: Exp Integer -> Exp Integer -> Exp Integer
-simplifyExponentiation (LitInt a) (LitInt b) = LitInt (a ^ b)
-simplifyExponentiation _ _ = error "Internal Error: exponentiation is unsupported in SMT lib"
+simplifyExponentiation a b = fromMaybe (error "Internal Error: no support for symbolic exponents in SMT lib")
+                             $   [LitInt $ a' ^ b'               | a' <- eval a, b' <- evalb]
+                             <|> [foldr Mul (LitInt 1) (genericReplicate b' a) | b' <- evalb]
+  where
+    evalb = eval b
 
 constant :: Id -> MType -> SMT2
 constant name tp = "(declare-const " <> name <> " " <> (sType tp) <> ")"

tests/invariants/fail/concretebase.act

@@ -0,0 +1,10 @@
+constructor of Exponentiation
+interface constructor()
+
+creates
+
+    uint256 thirtytwo := (10 - 2 * 4) ^ (100 - 5 * 19)
+
+invariants
+
+    thirtytwo == 33

tests/invariants/fail/concreteexponent.act

@@ -0,0 +1,10 @@
+constructor of Exponentiation
+interface constructor(uint256 x)
+
+creates
+
+    uint256 xpow5 := x ^ (100 - 5 * 19)
+
+invariants
+
+    xpow5 == x ^ 4

tests/invariants/fail/symbolicexponent.act

@@ -0,0 +1,10 @@
+constructor of Exponentiation
+interface constructor(uint x)
+
+creates
+
+    uint256 exponential := (10 - 2 * 4) ^ (100 - x * 19)
+
+invariants
+
+    exponential == 32

tests/invariants/pass/concretebase.act

@@ -0,0 +1,10 @@
+constructor of Exponentiation
+interface constructor()
+
+creates
+
+    uint256 thirtytwo := (10 - 2 * 4) ^ (100 - 5 * 19)
+
+invariants
+
+    thirtytwo == 32

tests/invariants/pass/concreteexponent.act

@@ -0,0 +1,10 @@
+constructor of Exponentiation
+interface constructor(uint256 x)
+
+creates
+
+    uint256 xpow5 := x ^ (100 - 5 * 19)
+
+invariants
+
+    xpow5 == x ^ 5