Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Heapster: use unsafeAssert for translating BVProps known to hold #1544

Merged
merged 3 commits into from
Dec 20, 2021
Merged

Heapster: use unsafeAssert for translating BVProps known to hold #1544

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
eccfa7e
added special cases in the translation of BVProps that are statically…
Dec 19, 2021
f0aef5f
changed the translation of true BVProps to now use special-purpose as…
Dec 19, 2021
908f76f
Merge branch 'master' into heapster/unsafeAssert-in-translation
Dec 20, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 47 additions & 16 deletions heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand All @@ -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 ->
Expand All @@ -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 ->
Expand Down
16 changes: 16 additions & 0 deletions saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
2 changes: 2 additions & 0 deletions saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
]
Expand Down
6 changes: 6 additions & 0 deletions saw-core/prelude/Prelude.sawcore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
4 changes: 3 additions & 1 deletion src/SAWScript/HeapsterBuiltins.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down