Merge pull request #1274 from GaloisInc/issue1120

Make `goal_eval_unint` handle `Z n` types.
GaloisInc · May 6, 2021 · 2d92f2a · 2d92f2a
2 parents 1fb5f4e + 4a471b6
commit 2d92f2a
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 0 deletions.
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -1193,6 +1193,9 @@ parseUninterpretedSAW sym st sc ref trm app ty =
     VIntType
       -> VInt  <$> mkUninterpretedSAW sym st ref trm app BaseIntegerRepr
 
+    VIntModType n
+      -> VIntMod n <$> mkUninterpretedSAW sym st ref (ArgTermFromIntMod n trm) app BaseIntegerRepr
+
     -- 0 width bitvector is a constant
     VVecType 0 VBoolType
       -> return $ VWord ZBV
@@ -1247,6 +1250,8 @@ mkUninterpretedSAW sym st ref trm (UnintApp nm args tys) ret =
 data ArgTerm
   = ArgTermVar
   | ArgTermBVZero -- ^ scBvNat 0 0
+  | ArgTermToIntMod Natural ArgTerm -- ^ toIntMod n x
+  | ArgTermFromIntMod Natural ArgTerm -- ^ fromIntMod n x
   | ArgTermVector Term [ArgTerm] -- ^ element type, elements
   | ArgTermUnit
   | ArgTermPair ArgTerm ArgTerm
@@ -1278,6 +1283,16 @@ reconstructArgTerm atrm sc ts =
           do z <- scNat sc 0
              x <- scBvNat sc z z
              return (x, ts0)
+        ArgTermToIntMod n at1 ->
+          do n' <- scNat sc n
+             (x1, ts1) <- parse at1 ts0
+             x <- scToIntMod sc n' x1
+             pure (x, ts1)
+        ArgTermFromIntMod n at1 ->
+          do n' <- scNat sc n
+             (x1, ts1) <- parse at1 ts0
+             x <- scFromIntMod sc n' x1
+             pure (x, ts1)
         ArgTermVector ty ats ->
           do (xs, ts1) <- parseList ats ts0
              x <- scVector sc ty xs
@@ -1336,6 +1351,7 @@ mkArgTerm sc ty val =
     (_, VWord ZBV)       -> return ArgTermBVZero     -- 0-width bitvector is a constant
     (_, VWord (DBV _))   -> return ArgTermVar
     (VUnitType, VUnit)   -> return ArgTermUnit
+    (VIntModType n, VIntMod _ _) -> pure (ArgTermToIntMod n ArgTermVar)
 
     (VVecType _ ety, VVector vv) ->
       do vs <- traverse force (V.toList vv)

diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -185,6 +185,7 @@ module Verifier.SAW.SharedTerm
     -- *** IntMod
   , scIntModType
   , scToIntMod
+  , scFromIntMod
     -- *** Vectors
   , scAppend
   , scJoin
@@ -1829,6 +1830,12 @@ scIntModType sc n = scGlobalApply sc "Prelude.IntMod" [n]
 scToIntMod :: SharedContext -> Term -> Term -> IO Term
 scToIntMod sc n x = scGlobalApply sc "Prelude.toIntMod" [n, x]
 
+-- | Convert an integer mod n to an integer.
+--
+-- > fromIntMod : (n : Nat) -> IntMod n -> Integer;
+scFromIntMod :: SharedContext -> Term -> Term -> IO Term
+scFromIntMod sc n x = scGlobalApply sc "Prelude.fromIntMod" [n, x]
+
 
 -- Primitive operations on bitvectors