Merge pull request #1544 from GaloisInc/heapster/unsafeAssert-in-tran…

…slation

Heapster: use unsafeAssert for translating BVProps known to hold

heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs

@@ -3654,17 +3654,23 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
       (:>: PTrans_Conj [APTrans_BVProp (BVPropTrans prop unitOpenTerm)]) $
       trans k]
 
-  {-
+  -- If we know e1 < e2 statically, translate to unsafeAssert
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULt e1 e2) _ |],
-   [nuMP| MbPermImpls_Cons _ mb_impl' |])
+   [nuMP| MbPermImpls_Cons _ _ mb_impl' |])
     | mbLift (fmap bvPropHolds prop) ->
-      withPermStackM (:>: translateVar x)
-      (:>: bvPropPerm (BVPropTrans prop
-                       (ctorOpenTerm "Prelude.Refl" [globalOpenTerm "Prelude.Bool",
-                                                     globalOpenTerm "Prelude.True"])))
-      (translate $ mbCombine mb_impl')
-  -}
+      translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans ->
+      return $ \k ->
+      do let w = natVal4 e1
+         t1 <- translate1 e1
+         t2 <- translate1 e2
+         let pf_tm =
+               applyOpenTermMulti (globalOpenTerm "Prelude.unsafeAssertBVULt")
+               [natOpenTerm w, t1, t2]
+         withPermStackM (:>: translateVar x)
+           (:>: bvPropPerm (BVPropTrans prop pf_tm))
+           (trans k)
 
+  -- If we don't know e1 < e2 statically, translate to bvultWithProof
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULt e1 e2) prop_str |],
    [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) ->
     translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans ->
@@ -3681,17 +3687,23 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
            [ return (natOpenTerm $ natVal2 prop), translate1 e1, translate1 e2]
          ]
 
-  {-
+  -- If we know e1 <= e2 statically, translate to unsafeAssert
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULeq e1 e2) _ |],
-   [nuMP| MbPermImpls_Cons _ mb_impl' |])
+   [nuMP| MbPermImpls_Cons _ _ mb_impl' |])
     | mbLift (fmap bvPropHolds prop) ->
-      withPermStackM (:>: translateVar x)
-      (:>: bvPropPerm (BVPropTrans prop
-                       (ctorOpenTerm "Prelude.Refl" [globalOpenTerm "Prelude.Bool",
-                                                     globalOpenTerm "Prelude.True"])))
-      (translate $ mbCombine mb_impl')
-  -}
+      translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans ->
+      return $ \k ->
+      do let w = natVal4 e1
+         t1 <- translate1 e1
+         t2 <- translate1 e2
+         let pf_tm =
+               applyOpenTermMulti (globalOpenTerm "Prelude.unsafeAssertBVULe")
+               [natOpenTerm w, t1, t2]
+         withPermStackM (:>: translateVar x)
+           (:>: bvPropPerm (BVPropTrans prop pf_tm))
+           (trans k)
 
+  -- If we don't know e1 <= e2 statically, translate to bvuleWithProof
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULeq e1 e2) prop_str |],
    [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) ->
     translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans ->
@@ -3708,7 +3720,26 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl
            [ return (natOpenTerm $ natVal2 prop), translate1 e1, translate1 e2]
          ]
 
+  -- If we know e1 <= e2-e3 statically, translate to unsafeAssert
+  ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULeq_Diff e1 e2 e3) _ |],
+   [nuMP| MbPermImpls_Cons _ _ mb_impl' |])
+    | mbLift (fmap bvPropHolds prop) ->
+      translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans ->
+      return $ \k ->
+      do let w = natVal4 e1
+         t1 <- translate1 e1
+         t2 <- translate1 e2
+         t3 <- translate1 e3
+         let pf_tm =
+               applyOpenTermMulti (globalOpenTerm "Prelude.unsafeAssertBVULe")
+               [natOpenTerm w, t1,
+                applyOpenTermMulti (globalOpenTerm
+                                    "Prelude.bvSub") [natOpenTerm w, t2, t3]]
+         withPermStackM (:>: translateVar x)
+           (:>: bvPropPerm (BVPropTrans prop pf_tm))
+           (trans k)
 
+  -- If we don't know e1 <= e2-e3 statically, translate to bvuleWithProof
   ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULeq_Diff e1 e2 e3) prop_str |],
    [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) ->
     translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans ->

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v

@@ -782,3 +782,19 @@ Hint Extern 3 (IntroArg _ (@eq bool ?x ?y) _) =>
     | msb _ _ => simple apply IntroArg_msb_false_iff_bvsle
     end
   end : refinesFun.
+
+
+(* Tactics for solving bitvector inequalities *)
+
+(* FIXME: these axioms should be easy to prove... *)
+
+(* 0 <= x for any x *)
+Axiom bvule_zero_any : forall n x, bvule n (intToBv n 0) x = true.
+
+(* x = y implies x <= y *)
+Axiom eq_implies_bvule : forall n x y, x = y -> bvule n x y = true.
+
+Ltac solveUnsafeAssertBVULt := reflexivity.
+Ltac solveUnsafeAssertBVULe :=
+  try reflexivity; try (apply bvule_zero_any);
+  try (apply eq_implies_bvule; reflexivity).

saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

@@ -212,6 +212,8 @@ sawCorePreludeSpecialTreatmentMap configuration =
   [ ("error",             mapsTo sawDefinitionsModule "error")
   , ("fix",               skip)
   , ("unsafeAssert",      replaceDropArgs 3 $ Coq.Ltac "solveUnsafeAssert")
+  , ("unsafeAssertBVULt", replaceDropArgs 3 $ Coq.Ltac "solveUnsafeAssertBVULt")
+  , ("unsafeAssertBVULe", replaceDropArgs 3 $ Coq.Ltac "solveUnsafeAssertBVULe")
   , ("unsafeCoerce",      skip)
   , ("unsafeCoerce_same", skip)
   ]

saw-core/prelude/Prelude.sawcore

@@ -1538,6 +1538,12 @@ foldW64List =
 --------------------------------------------------------------------------------
 -- Vector operations with built-in casts of their resulting lengths
 
+-- Specialized version of unsafeAssert for bitvector inequalities
+axiom unsafeAssertBVULt : (n : Nat) -> (x : Vec n Bool) -> (y : Vec n Bool) ->
+                          Eq Bool (bvult n x y) True;
+axiom unsafeAssertBVULe : (n : Nat) -> (x : Vec n Bool) -> (y : Vec n Bool) ->
+                          Eq Bool (bvule n x y) True;
+
 -- Decide equality on two bitvectors, returning a proof if they are equal
 primitive bvEqWithProof : (n : Nat) -> (v1 v2 : Vec n Bool) ->
                           Maybe (Eq (Vec n Bool) v1 v2);

src/SAWScript/HeapsterBuiltins.hs

@@ -1204,7 +1204,9 @@ heapster_export_coq _bic _opts henv filename =
      saw_mod <- liftIO $ scFindModule sc $ heapsterEnvSAWModule henv
      let coq_doc =
            vcat [preamble coq_trans_conf {
-                   postPreamble = "From CryptolToCoq Require Import SAWCorePrelude."},
+                   postPreamble =
+                       "From CryptolToCoq Require Import SAWCorePrelude.\n" ++
+                       "From CryptolToCoq Require Import SAWCoreBitvectors." },
                  translateSAWModule coq_trans_conf saw_mod]
      liftIO $ writeFile filename (show coq_doc)