Expose the divNat, modNat and divModNat SAWCore operations

via the `SharedTerm` module. Add a new `intAbs` primitive operation for integer absolute value.
GaloisInc · Aug 7, 2018 · eac2b68 · eac2b68
1 parent 33bb7dd
commit eac2b68
Show file tree

Hide file tree

Showing 5 changed files with 24 additions and 3 deletions.
diff --git a/prelude/Prelude.sawcore b/prelude/Prelude.sawcore
@@ -1295,6 +1295,7 @@ primitive intMod :: Integer -> Integer -> Integer;
 primitive intMin :: Integer -> Integer -> Integer;
 primitive intMax :: Integer -> Integer -> Integer;
 primitive intNeg :: Integer -> Integer;
+primitive intAbs :: Integer -> Integer;
 primitive intEq  :: Integer -> Integer -> Bool;
 primitive intLe  :: Integer -> Integer -> Bool;
 primitive intLt  :: Integer -> Integer -> Bool;

diff --git a/src/Verifier/SAW/SharedTerm.hs b/src/Verifier/SAW/SharedTerm.hs
@@ -96,6 +96,9 @@ module Verifier.SAW.SharedTerm
   , scAddNat
   , scSubNat
   , scMulNat
+  , scDivNat
+  , scModNat
+  , scDivModNat
   , scEqualNat
   , scLtNat
   , scMinNat
@@ -166,7 +169,7 @@ module Verifier.SAW.SharedTerm
   , scIntegerConst
   , scIntAdd, scIntSub, scIntMul
   , scIntDiv, scIntMod, scIntNeg
-  , scIntMin, scIntMax
+  , scIntAbs, scIntMin, scIntMax
   , scIntEq, scIntLe, scIntLt
   , scIntToNat, scNatToInt
   , scIntToBv, scBvToInt, scSbvToInt
@@ -1323,6 +1326,18 @@ scSubNat sc x y = scGlobalApply sc "Prelude.subNat" [x,y]
 scMulNat :: SharedContext -> Term -> Term -> IO Term
 scMulNat sc x y = scGlobalApply sc "Prelude.mulNat" [x,y]
 
+-- divNat :: Nat -> Nat -> Nat;
+scDivNat :: SharedContext -> Term -> Term -> IO Term
+scDivNat sc x y = scGlobalApply sc "Prelude.divNat" [x,y]
+
+-- modNat :: Nat -> Nat -> Nat;
+scModNat :: SharedContext -> Term -> Term -> IO Term
+scModNat sc x y = scGlobalApply sc "Prelude.modNat" [x,y]
+
+-- divModNat :: Nat -> Nat -> #(Nat, Nat);
+scDivModNat :: SharedContext -> Term -> Term -> IO Term
+scDivModNat sc x y = scGlobalApply sc "Prelude.divModNat" [x,y]
+
 scEqualNat :: SharedContext -> Term -> Term -> IO Term
 scEqualNat sc x y = scGlobalApply sc "Prelude.equalNat" [x,y]
 
@@ -1356,10 +1371,11 @@ scIntMod sc x y = scGlobalApply sc "Prelude.intMod" [x, y]
 scIntMin sc x y = scGlobalApply sc "Prelude.intMin" [x, y]
 scIntMax sc x y = scGlobalApply sc "Prelude.intMax" [x, y]
 
--- primitive intNeg :: Integer -> Integer;
-scIntNeg
+-- primitive intNeg/intAbs :: Integer -> Integer;
+scIntNeg, scIntAbs
    :: SharedContext -> Term -> IO Term
 scIntNeg sc x = scGlobalApply sc "Prelude.intNeg" [x]
+scIntAbs sc x = scGlobalApply sc "Prelude.intAbs" [x]
 
 -- primitive intEq/intLe/intLt  :: Integer -> Integer -> Bool;
 scIntEq, scIntLe, scIntLt

diff --git a/src/Verifier/SAW/Simulator/Concrete.hs b/src/Verifier/SAW/Simulator/Concrete.hs
@@ -212,6 +212,7 @@ prims =
   , Prims.bpIntDiv = pure2 div
   , Prims.bpIntMod = pure2 mod
   , Prims.bpIntNeg = pure1 negate
+  , Prims.bpIntAbs = pure1 abs
   , Prims.bpIntEq  = pure2 (==)
   , Prims.bpIntLe  = pure2 (<=)
   , Prims.bpIntLt  = pure2 (<)

diff --git a/src/Verifier/SAW/Simulator/Prims.hs b/src/Verifier/SAW/Simulator/Prims.hs
@@ -104,6 +104,7 @@ data BasePrims l =
   , bpIntDiv :: VInt l -> VInt l -> MInt l
   , bpIntMod :: VInt l -> VInt l -> MInt l
   , bpIntNeg :: VInt l -> MInt l
+  , bpIntAbs :: VInt l -> MInt l
   , bpIntEq :: VInt l -> VInt l -> MBool l
   , bpIntLe :: VInt l -> VInt l -> MBool l
   , bpIntLt :: VInt l -> VInt l -> MBool l
@@ -182,6 +183,7 @@ constMap bp = Map.fromList
   , ("Prelude.intDiv", intBinOp "intDiv" (bpIntDiv bp))
   , ("Prelude.intMod", intBinOp "intMod" (bpIntMod bp))
   , ("Prelude.intNeg", intUnOp  "intNeg" (bpIntNeg bp))
+  , ("Prelude.intAbs", intUnOp  "intAbs" (bpIntAbs bp))
   , ("Prelude.intEq" , intBinCmp "intEq" (bpIntEq bp))
   , ("Prelude.intLe" , intBinCmp "intLe" (bpIntLe bp))
   , ("Prelude.intLt" , intBinCmp "intLt" (bpIntLt bp))

diff --git a/src/Verifier/SAW/Simulator/RME.hs b/src/Verifier/SAW/Simulator/RME.hs
@@ -197,6 +197,7 @@ prims =
   , Prims.bpIntDiv = pure2 div
   , Prims.bpIntMod = pure2 mod
   , Prims.bpIntNeg = pure1 negate
+  , Prims.bpIntAbs = pure1 abs
   , Prims.bpIntEq  = pure2 (\x y -> RME.constant (x == y))
   , Prims.bpIntLe  = pure2 (\x y -> RME.constant (x <= y))
   , Prims.bpIntLt  = pure2 (\x y -> RME.constant (x < y))