From 2e79a1ea3a7c86507c36b3ad4e6e281ed51b6f4c Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 7 Nov 2023 06:24:56 -0800 Subject: [PATCH] Draft: Basic checking for underspecified mutable allocs in overrides --- intTests/test_mir_unsafe_assume_spec/test.saw | 19 +- .../Makefile | 13 + .../test.linked-mir.json | 1 + .../test.rs | 14 + .../test.saw | 56 +++ .../test.sh | 3 + src/SAWScript/Crucible/MIR/MethodSpecIR.hs | 19 +- src/SAWScript/Crucible/MIR/Override.hs | 365 +++++++++++++++++- 8 files changed, 476 insertions(+), 14 deletions(-) create mode 100644 intTests/test_mir_unsafe_assume_spec_statics/Makefile create mode 100644 intTests/test_mir_unsafe_assume_spec_statics/test.linked-mir.json create mode 100644 intTests/test_mir_unsafe_assume_spec_statics/test.rs create mode 100644 intTests/test_mir_unsafe_assume_spec_statics/test.saw create mode 100755 intTests/test_mir_unsafe_assume_spec_statics/test.sh diff --git a/intTests/test_mir_unsafe_assume_spec/test.saw b/intTests/test_mir_unsafe_assume_spec/test.saw index c37e1d645a..ff32e70085 100644 --- a/intTests/test_mir_unsafe_assume_spec/test.saw +++ b/intTests/test_mir_unsafe_assume_spec/test.saw @@ -84,6 +84,8 @@ let side_spec_2 = do { mir_return (mir_term a); }; +// This spec is erroneous—see the comments below in the "Avoid unsoundness" +// part of the test. let foo_spec = do { x <- mir_fresh_var "x" mir_u32; @@ -141,18 +143,17 @@ fails ( // Avoid unsoundness // /////////////////////// -// https://github.com/GaloisInc/saw-script/issues/30 - side_ov_1 <- mir_verify m "test::side_effect" [] false side_spec_1 z3; side_ov_2 <- mir_verify m "test::side_effect" [] false side_spec_2 z3; +// This should not verify, as invoking `side_effect` should cause `foo` to +// always return `0` rather than the argument value. fails ( mir_verify m "test::foo" [side_ov_1] false foo_spec z3 ); -// TODO: This should not verify, as side_spec_2 underspecifies the mutable -// allocation `a_ptr`. We need to implement a check that catches this. -// fails ( -// mir_verify m "test::foo" [side_ov_2] false foo_spec z3 -// ); - -// TODO: Add similar tests for mutable statics. +// This should not verify, as side_spec_2 underspecifies the mutable +// allocation `a_ptr` in its postconditions. SAW will catch this when attempting +// to use side_ov_2 as an override. +fails ( + mir_verify m "test::foo" [side_ov_2] false foo_spec z3 +); diff --git a/intTests/test_mir_unsafe_assume_spec_statics/Makefile b/intTests/test_mir_unsafe_assume_spec_statics/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec_statics/Makefile @@ -0,0 +1,13 @@ +all: test.linked-mir.json + +test.linked-mir.json: test.rs + saw-rustc $< + $(MAKE) remove-unused-build-artifacts + +.PHONY: remove-unused-build-artifacts +remove-unused-build-artifacts: + rm -f test libtest.mir libtest.rlib + +.PHONY: clean +clean: remove-unused-build-artifacts + rm -f test.linked-mir.json diff --git a/intTests/test_mir_unsafe_assume_spec_statics/test.linked-mir.json b/intTests/test_mir_unsafe_assume_spec_statics/test.linked-mir.json new file mode 100644 index 0000000000..1a3481a675 --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec_statics/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:1:21: 1:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:1: 1:24"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/65ce71a4::A","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::5c073f3fd0b9c562"},"kind":"Constant"},"kind":"Call","pos":"test.rs:12:5: 12:18"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb2"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::5c073f3fd0b9c562"},"kind":"Constant"},"kind":"Call","pos":"test.rs:13:5: 13:18"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:14:2: 14:2"}},"blockid":"bb2"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}]},"name":"test/65ce71a4::foo","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:5:22: 5:23","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/65ce71a4::A","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:5:22: 5:23","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:6:9: 6:10","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/65ce71a4::A","kind":"static_ref"},"ty":"ty::RawPtr::63e5937014067f41"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}},"pos":"test.rs:6:9: 6:14","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"0"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:9:2: 9:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::RawPtr::63e5937014067f41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::RawPtr::63e5937014067f41"}]},"name":"test/65ce71a4::side_effect","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[{"kind":"body","mutable":true,"name":"test/65ce71a4::A","ty":"ty::u32"}],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/65ce71a4::foo","kind":"Item","substs":[]},"name":"test/65ce71a4::foo"},{"inst":{"def_id":"test/65ce71a4::side_effect","kind":"Item","substs":[]},"name":"test/65ce71a4::side_effect"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::FnDef::5c073f3fd0b9c562","ty":{"defid":"test/65ce71a4::side_effect","kind":"FnDef"}},{"name":"ty::RawPtr::63e5937014067f41","ty":{"kind":"RawPtr","mutability":{"kind":"Mut"},"ty":"ty::u32"}}],"roots":["test/65ce71a4::side_effect","test/65ce71a4::foo"]} \ No newline at end of file diff --git a/intTests/test_mir_unsafe_assume_spec_statics/test.rs b/intTests/test_mir_unsafe_assume_spec_statics/test.rs new file mode 100644 index 0000000000..ce4f1d0f11 --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec_statics/test.rs @@ -0,0 +1,14 @@ +static mut A: u32 = 42; + +pub fn side_effect() -> u32 { + unsafe { + let v: u32 = A; + A = 0; + v + } +} + +pub fn foo() -> u32 { + side_effect(); + side_effect() +} diff --git a/intTests/test_mir_unsafe_assume_spec_statics/test.saw b/intTests/test_mir_unsafe_assume_spec_statics/test.saw new file mode 100644 index 0000000000..385b32deb3 --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec_statics/test.saw @@ -0,0 +1,56 @@ +enable_experimental; + +m <- mir_load_module "test.linked-mir.json"; + +let side_spec_1 = do { + let a_static = mir_static "test::A"; + a_init <- mir_fresh_var "A" mir_u32; + mir_points_to a_static (mir_term a_init); + + mir_execute_func []; + + mir_points_to a_static (mir_term {{ 0 : [32] }}); + mir_return (mir_term a_init); +}; + +let side_spec_2 = do { + let a_static = mir_static "test::A"; + a_init <- mir_fresh_var "A" mir_u32; + mir_points_to a_static (mir_term a_init); + + mir_execute_func []; + + mir_return (mir_term a_init); +}; + +// This spec is erroneous—see the comments below in the "Avoid unsoundness" +// part of the test. +let foo_spec = do { + let a_static = mir_static "test::A"; + a_init <- mir_fresh_var "A" mir_u32; + mir_points_to a_static (mir_term a_init); + + mir_execute_func []; + + mir_points_to a_static (mir_term {{ 0 : [32] }}); + mir_return (mir_term a_init); +}; + +/////////////////////// +// Avoid unsoundness // +/////////////////////// + +side_ov_1 <- mir_verify m "test::side_effect" [] false side_spec_1 z3; +side_ov_2 <- mir_verify m "test::side_effect" [] false side_spec_2 z3; + +// This should not verify, as invoking `side_effect` should cause `foo` to +// always return `0` rather than the original value of A. +fails ( + mir_verify m "test::foo" [side_ov_1] false foo_spec z3 +); +// This should not verify, as side_spec_2 underspecifies the mutable +// static `a_ptr` in its postconditions. SAW will catch this when attempting +// to use side_ov_2 as an override. +fails ( + mir_verify m "test::foo" [side_ov_2] false foo_spec z3 +); diff --git a/intTests/test_mir_unsafe_assume_spec_statics/test.sh b/intTests/test_mir_unsafe_assume_spec_statics/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_unsafe_assume_spec_statics/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs index d11a8b82b5..b66b3cc02a 100644 --- a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs @@ -1,4 +1,5 @@ {-# Language DataKinds #-} +{-# Language LambdaCase #-} {-# Language OverloadedStrings #-} {-# Language RankNTypes #-} {-# Language TemplateHaskell #-} @@ -33,6 +34,9 @@ module SAWScript.Crucible.MIR.MethodSpecIR , maMirType , maLen + , mutIso + , isMut + -- * @MirPointer@ , MirPointer(..) , mpType @@ -51,7 +55,7 @@ module SAWScript.Crucible.MIR.MethodSpecIR , initialCrucibleSetupState ) where -import Control.Lens (Getter, (^.), to) +import Control.Lens (Getter, Iso', Lens', (^.), iso, to) import qualified Prettyprinter as PP import Lang.Crucible.FunctionHandle (HandleAllocator) @@ -83,6 +87,19 @@ instance PP.Pretty MirPointsTo where pretty (MirPointsTo _md ref sv) = PP.parens $ MS.ppSetupValue ref PP.<+> "->" PP.<+> PP.list (map MS.ppSetupValue sv) +mutIso :: Iso' M.Mutability Bool +mutIso = + iso + (\case + M.Mut -> True + M.Immut -> False) + (\case + True -> M.Mut + False -> M.Immut) + +isMut :: Lens' (MirAllocSpec tp) Bool +isMut = maMutbl . mutIso + type MIRMethodSpec = MS.CrucibleMethodSpecIR MIR initialDefCrucibleMethodSpecIR :: diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index 69bf96e6fa..ef2aab1e08 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -4,8 +4,11 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} -- | Override matching and application for MIR. module SAWScript.Crucible.MIR.Override @@ -36,10 +39,12 @@ import Data.List (tails) import qualified Data.List.NonEmpty as NE import qualified Data.Map as Map import Data.Map (Map) -import Data.Maybe (catMaybes) +import Data.Maybe (catMaybes, isJust) +import qualified Data.Parameterized.Classes as PC import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.Some (Some(..)) import qualified Data.Parameterized.TraversableFC as FC +import Data.Proxy (Proxy(..)) import qualified Data.Set as Set import Data.Set (Set) import qualified Data.Vector as V @@ -52,6 +57,8 @@ import qualified Lang.Crucible.Backend as Crucible import qualified Lang.Crucible.FunctionHandle as Crucible import qualified Lang.Crucible.Simulator as Crucible import qualified Lang.Crucible.Types as Crucible +import qualified Mir.DefId as Mir +import qualified Mir.FancyMuxTree as Mir import qualified Mir.Generator as Mir import qualified Mir.Intrinsics as Mir import Mir.Intrinsics (MIR) @@ -129,6 +136,359 @@ assignTerm sc cc md prepost var val = Just old -> matchTerm sc cc md prepost val old +-- | TODO RGS: Docs +checkMutableAllocPostconds :: + Options -> + SharedContext -> + MIRCrucibleContext -> + CrucibleMethodSpecIR -> + OverrideMatcher MIR md () +checkMutableAllocPostconds opts sc cc cs = do + sub <- use setupValueSub + + postRefs <- Set.fromList <$> + traverse + (\(MirPointsTo _cond ref _val) -> do + MIRVal refShp refVal <- + resolveSetupValueMIR opts cc sc cs ref + case testRefShape refShp of + Just IsRefShape{} -> + pure $ Some $ MirReferenceMuxConcrete refVal + Nothing -> + panic "checkMutableAllocPostconds" + [ "Unexpected non-reference type:" + , show $ PP.pretty $ shapeMirTy refShp + ]) + (cs ^. MS.csPostState ^. MS.csPointsTos) + + let mutAllocSpecs = + Map.filter (\(Some mas) -> view isMut mas) $ + cs ^. MS.csPreState . MS.csAllocs + let mutAllocRefs = + map + (\(Some mp, Some spec) -> + ( Some $ MirReferenceMuxConcrete $ mp ^. mpRef + , spec ^. maConditionMetadata + )) + (Map.elems (Map.intersectionWith (,) sub mutAllocSpecs)) + + F.for_ mutAllocRefs $ \(mutAllocRef, cond) -> + unless (Set.member mutAllocRef postRefs) $ + fail $ underspecified_mut_alloc_err cond + + let mutStatics = + Map.filter (view Mir.sMutable) $ + col ^. Mir.statics + let mutStaticRefs = + map + (\(mutStaticDid, (_, Mir.StaticVar gv)) -> + ( mutStaticDid + , Some $ MirReferenceMuxConcrete $ staticRefMux sym gv + )) + (Map.toList + (Map.intersectionWith + (,) mutStatics (colState ^. Mir.staticMap))) + + F.for_ mutStaticRefs $ \(mutStaticDid, mutStaticRef) -> + unless (Set.member mutStaticRef postRefs) $ + fail $ underspecified_mut_static_err mutStaticDid + where + sym = cc ^. mccSym + colState = cc ^. mccRustModule . Mir.rmCS + col = colState ^. Mir.collection + + underspecified_mut_alloc_err :: + MS.ConditionMetadata -> String + underspecified_mut_alloc_err cond = + concat + [ "State of memory allocated in precondition (at " + , show $ W4.plSourceLoc $ MS.conditionLoc cond + , ") not described in postcondition" + ] + + underspecified_mut_static_err :: + Mir.DefId -> String + underspecified_mut_static_err did = + concat + [ "State of mutable static variable \"" + , show did + , "\" not described in postcondition" + ] + +-- | TODO RGS: Docs +newtype MirReferenceMuxConcrete tp = + MirReferenceMuxConcrete (Mir.MirReferenceMux Sym tp) + +instance W4.TestEquality MirReferenceMuxConcrete where + testEquality x y = PC.orderingF_refl (PC.compareF x y) + +instance PC.EqF MirReferenceMuxConcrete where + eqF x y = isJust (W4.testEquality x y) + +instance PC.OrdF MirReferenceMuxConcrete where + compareF (MirReferenceMuxConcrete x) (MirReferenceMuxConcrete y) = + cmpRefMuxConcretely Proxy x y + +-- | TODO RGS: Docs +cmpRefMuxConcretely :: + forall sym tp1 tp2 proxy. + Crucible.IsSymInterface sym => + proxy sym -> + Mir.MirReferenceMux sym tp1 -> + Mir.MirReferenceMux sym tp2 -> + PC.OrderingF tp1 tp2 +cmpRefMuxConcretely sym (Mir.MirReferenceMux fmt1) (Mir.MirReferenceMux fmt2) = + cmpRefConcretely sym + (fancyMuxTreeConcrete fmt1) (fancyMuxTreeConcrete fmt2) + where + fancyMuxTreeConcrete :: Mir.FancyMuxTree sym a -> a + fancyMuxTreeConcrete fmt = + case Mir.viewFancyMuxTree fmt of + [(x, p)] -> + if Just True == W4.asConstantPred p + then x + else error "TODO RGS: Fill me in" + [] -> + error "TODO RGS: Fill me in" + (_:_) -> + error "TODO RGS: Fill me in" + +-- | TODO RGS: Docs +cmpRefConcretely :: + Crucible.IsSymInterface sym => + proxy sym -> + Mir.MirReference sym tp1 -> + Mir.MirReference sym tp2 -> + PC.OrderingF tp1 tp2 +cmpRefConcretely sym (Mir.MirReference r1 p1) (Mir.MirReference r2 p2) = + cmpRootConcretely r1 r2 <<>> cmpPathConcretely sym p1 p2 +cmpRefConcretely sym (Mir.MirReference_Integer tpr1 i1) (Mir.MirReference_Integer tpr2 i2) = + PC.compareF tpr1 tpr2 <<>> cmpSymBVConcretely sym i1 i2 <<>> PC.EQF +cmpRefConcretely _ (Mir.MirReference _ _) (Mir.MirReference_Integer _ _) = + PC.LTF +cmpRefConcretely _ (Mir.MirReference_Integer _ _) (Mir.MirReference _ _) = + PC.GTF + +-- | TODO RGS: Docs +cmpRootConcretely :: + Mir.MirReferenceRoot sym tp1 -> + Mir.MirReferenceRoot sym tp2 -> + PC.OrderingF tp1 tp2 + +-- RefCell_RefRoot +cmpRootConcretely (Mir.RefCell_RefRoot rc1) (Mir.RefCell_RefRoot rc2) = + PC.compareF rc1 rc2 + +cmpRootConcretely (Mir.RefCell_RefRoot _) _ = PC.LTF +cmpRootConcretely _ (Mir.RefCell_RefRoot _) = PC.GTF + +-- GlobalVar_RefRoot +cmpRootConcretely (Mir.GlobalVar_RefRoot gv1) (Mir.GlobalVar_RefRoot gv2) = + PC.compareF gv1 gv2 +cmpRootConcretely (Mir.GlobalVar_RefRoot _) _ = PC.LTF +cmpRootConcretely _ (Mir.GlobalVar_RefRoot _) = PC.GTF + +-- Const_RefRoot +cmpRootConcretely (Mir.Const_RefRoot _ _) (Mir.Const_RefRoot _ _) = + error "TODO RGS: Copy error message from mirRef_eqIO" + +cmpPathConcretely :: + Crucible.IsSymInterface sym => + proxy sym -> + Mir.MirReferencePath sym tp tp1 -> + Mir.MirReferencePath sym tp tp2 -> + PC.OrderingF tp1 tp2 + +-- Empty_RefPath +cmpPathConcretely _ Mir.Empty_RefPath Mir.Empty_RefPath = PC.EQF +cmpPathConcretely _ Mir.Empty_RefPath _ = PC.LTF +cmpPathConcretely _ _ Mir.Empty_RefPath = PC.GTF + +-- Any_RefPath +cmpPathConcretely sym (Mir.Any_RefPath tpr1 p1) (Mir.Any_RefPath tpr2 p2) = + PC.compareF tpr1 tpr2 <<>> + cmpPathConcretely sym p1 p2 <<>> + PC.EQF +cmpPathConcretely _ (Mir.Any_RefPath _ _) _ = PC.LTF +cmpPathConcretely _ _ (Mir.Any_RefPath _ _) = PC.GTF + +-- Field_RefPath +cmpPathConcretely sym (Mir.Field_RefPath ctx1 p1 idx1) (Mir.Field_RefPath ctx2 p2 idx2) = + PC.compareF ctx1 ctx2 <<>> + PC.compareF idx1 idx2 <<>> + cmpPathConcretely sym p1 p2 <<>> + PC.EQF +cmpPathConcretely _ (Mir.Field_RefPath _ _ _) _ = PC.LTF +cmpPathConcretely _ _ (Mir.Field_RefPath _ _ _) = PC.GTF + +-- Variant_RefPath +cmpPathConcretely sym (Mir.Variant_RefPath discrTp1 ctx1 p1 idx1) (Mir.Variant_RefPath discrTp2 ctx2 p2 idx2) = + PC.compareF discrTp1 discrTp2 <<>> + PC.compareF ctx1 ctx2 <<>> + PC.compareF idx1 idx2 <<>> + cmpPathConcretely sym p1 p2 <<>> + PC.EQF +cmpPathConcretely _ (Mir.Variant_RefPath _ _ _ _) _ = PC.LTF +cmpPathConcretely _ _ (Mir.Variant_RefPath _ _ _ _) = PC.GTF + +-- Index_RefPath +cmpPathConcretely sym (Mir.Index_RefPath tpr1 p1 i1) (Mir.Index_RefPath tpr2 p2 i2) = + PC.compareF tpr1 tpr2 <<>> + cmpPathConcretely sym p1 p2 <<>> + cmpSymBVConcretely sym i1 i2 <<>> + PC.EQF +cmpPathConcretely _ (Mir.Index_RefPath _ _ _) _ = PC.LTF +cmpPathConcretely _ _ (Mir.Index_RefPath _ _ _) = PC.GTF + +-- Just_RefPath +cmpPathConcretely sym (Mir.Just_RefPath tpr1 p1) (Mir.Just_RefPath tpr2 p2) = + PC.compareF tpr1 tpr2 <<>> + cmpPathConcretely sym p1 p2 <<>> + PC.EQF +cmpPathConcretely _ (Mir.Just_RefPath _ _) _ = PC.LTF +cmpPathConcretely _ _ (Mir.Just_RefPath _ _) = PC.GTF + +-- VectorAsMirVector_RefPath +cmpPathConcretely sym (Mir.VectorAsMirVector_RefPath tpr1 p1) (Mir.VectorAsMirVector_RefPath tpr2 p2) = + PC.compareF tpr1 tpr2 <<>> + cmpPathConcretely sym p1 p2 <<>> + PC.EQF +cmpPathConcretely _ (Mir.VectorAsMirVector_RefPath _ _) _ = PC.LTF +cmpPathConcretely _ _ (Mir.VectorAsMirVector_RefPath _ _) = PC.GTF + +-- ArrayAsMirVector_RefPath +cmpPathConcretely sym (Mir.ArrayAsMirVector_RefPath tpr1 p1) (Mir.ArrayAsMirVector_RefPath tpr2 p2) = + PC.compareF tpr1 tpr2 <<>> + cmpPathConcretely sym p1 p2 <<>> + PC.EQF + +-- | TODO RGS: Docs +cmpSymBVConcretely :: + Crucible.IsSymInterface sym => + proxy sym -> + W4.SymBV sym w -> + W4.SymBV sym w -> + PC.OrderingF w w +cmpSymBVConcretely _ symBV1 symBV2 + | Just bv1 <- W4.asBV symBV1 + , Just bv2 <- W4.asBV symBV2 + = PC.fromOrdering $ compare bv1 bv2 + | otherwise + = error "TODO RGS: Fill me in" + +-- | TODO RGS: Docs: +infixr 6 <<>> +(<<>>) :: + forall j k (a :: j) (b :: j) (c :: k) (d :: k). + PC.OrderingF a b -> + (a ~ b => PC.OrderingF c d) -> + PC.OrderingF c d +(<<>>) = PC.joinOrderingF + +{- +-- TODO RGS: Delete me? + +-- | TODO RGS: Docs +refRootConcretelyEqual :: + Mir.MirReferenceRoot sym tp1 -> + Mir.MirReferenceRoot sym tp2 -> + Bool +refRootConcretelyEqual (Mir.RefCell_RefRoot rc1) (Mir.RefCell_RefRoot rc2) + | Just Refl <- W4.testEquality rc1 rc2 + = True + | otherwise + = False +refRootConcretelyEqual (Mir.GlobalVar_RefRoot gv1) (Mir.GlobalVar_RefRoot gv2) + | Just Refl <- W4.testEquality gv1 gv2 + = True + | otherwise + = False +refRootConcretelyEqual (Mir.Const_RefRoot _ _) (Mir.Const_RefRoot _ _) = + error "refRootConcretelyEqual: Cannot compare Const_RefRoots" +refRootConcretelyEqual _ _ = + False + +-- | TODO RGS: Docs +refPathConcretelyEqual :: + Crucible.IsSymInterface sym => + sym -> + Mir.MirReferencePath sym tp_base1 tp1 -> + Mir.MirReferencePath sym tp_base2 tp2 -> + Bool +refPathConcretelyEqual _ Mir.Empty_RefPath Mir.Empty_RefPath = + True +refPathConcretelyEqual sym (Mir.Any_RefPath tpr1 p1) (Mir.Any_RefPath tpr2 p2) + | Just Refl <- W4.testEquality tpr1 tpr2 + = refPathConcretelyEqual sym p1 p2 +refPathConcretelyEqual sym (Mir.Field_RefPath ctx1 p1 idx1) (Mir.Field_RefPath ctx2 p2 idx2) + | Just Refl <- W4.testEquality ctx1 ctx2 + , Just Refl <- W4.testEquality idx1 idx2 + = refPathConcretelyEqual sym p1 p2 + | otherwise + = False +refPathConcretelyEqual sym (Mir.Variant_RefPath _ ctx1 p1 idx1) (Mir.Variant_RefPath _ ctx2 p2 idx2) + | Just Refl <- W4.testEquality ctx1 ctx2 + , Just Refl <- W4.testEquality idx1 idx2 + = refPathConcretelyEqual sym p1 p2 + | otherwise + = False +refPathConcretelyEqual sym (Mir.Index_RefPath tpr1 p1 idx1) (Mir.Index_RefPath tpr2 p2 idx2) + | Just Refl <- W4.testEquality tpr1 tpr2 + = let pEq = refPathConcretelyEqual sym p1 p2 in + let idxEq = bvConcretelyEqual sym idx1 idx2 in + pEq && idxEq + | otherwise + = False +refPathConcretelyEqual sym (Mir.Just_RefPath tpr1 p1) (Mir.Just_RefPath tpr2 p2) + | Just Refl <- W4.testEquality tpr1 tpr2 + = refPathConcretelyEqual sym p1 p2 +refPathConcretelyEqual sym (Mir.VectorAsMirVector_RefPath tpr1 p1) (Mir.VectorAsMirVector_RefPath tpr2 p2) + | Just Refl <- W4.testEquality tpr1 tpr2 + = refPathConcretelyEqual sym p1 p2 + | otherwise + = False +refPathConcretelyEqual sym (Mir.ArrayAsMirVector_RefPath tpr1 p1) (Mir.ArrayAsMirVector_RefPath tpr2 p2) + | Just Refl <- W4.testEquality tpr1 tpr2 + = refPathConcretelyEqual sym p1 p2 + | otherwise + = False +refPathConcretelyEqual _ _ _ = + False + +-- | TODO RGS: Docs +mirRefConcretelyEqual :: + Crucible.IsSymInterface sym => + sym -> + Mir.MirReference sym tp -> + Mir.MirReference sym tp -> + Bool +mirRefConcretelyEqual sym (Mir.MirReference root1 path1) (Mir.MirReference root2 path2) = + let rootEq = refRootConcretelyEqual root1 root2 in + let pathEq = refPathConcretelyEqual sym path1 path2 in + rootEq && pathEq +mirRefConcretelyEqual sym (Mir.MirReference_Integer _ i1) (Mir.MirReference_Integer _ i2) = + bvConcretelyEqual sym i1 i2 +-- All valid references are disjoint from all integer references. +mirRefConcretelyEqual _ (Mir.MirReference _ _) (Mir.MirReference_Integer _ _) = + False +mirRefConcretelyEqual _ (Mir.MirReference_Integer _ _) (Mir.MirReference _ _) = + False + +-- | TODO RGS: Docs +bvConcretelyEqual :: + Crucible.IsSymInterface sym => + sym -> + W4.SymBV sym w -> + W4.SymBV sym w -> + Bool +bvConcretelyEqual _ symBV1 symBV2 + | Just bv1 <- W4.asBV symBV1 + , Just bv2 <- W4.asBV symBV2 + = bv1 == bv2 + | otherwise + = False +-} + computeReturnValue :: Options {- ^ saw script debug and print options -} -> MIRCrucibleContext {- ^ context of the crucible simulation -} -> @@ -226,10 +586,7 @@ executeCond :: executeCond opts sc cc cs ss = do refreshTerms sc ss F.traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) - -- TODO: We need to do something like this: - {- checkMutableAllocPostconds opts sc cc cs - -} -- Which checks that all of the mutable allocations and statics have been -- specified in the postconditions of overrides. (See the related TODOs -- in the test_mir_unsafe_assume_spec test case.)