diff --git a/deps/crucible b/deps/crucible index 9876d6986b..c811db88db 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 9876d6986b13ca4d2c0711da518c8204b1b57bd2 +Subproject commit c811db88db74110c99903f98f70c0f48bee46485 diff --git a/deps/macaw b/deps/macaw index c6eae87724..d3a53a6769 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit c6eae87724cc5d6a2e1e3d46befceeaa8ab2757f +Subproject commit d3a53a676920ab56c8252a8d171098f2ad884ea8 diff --git a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs index b4cfb28551..aaccef503b 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs @@ -45,6 +45,7 @@ import Data.Parameterized.Context hiding ((:>), empty, take, view) import qualified Data.Parameterized.Context as Ctx import Data.Parameterized.TraversableFC import Data.Parameterized.BoolRepr +import Data.Parameterized.Nonce (Nonce) -- import qualified Text.PrettyPrint.ANSI.Leijen as PP import qualified Prettyprinter as PP @@ -70,7 +71,7 @@ import Verifier.SAW.OpenTerm -- | The lens into an 'RAssign' associated with a 'Member' proof -- --- FIXME HERE: this should go into Hobbits, possibly using +-- FIXME HERE: this should go into Hobbits, possibly using member :: Member ctx a -> Lens' (RAssign f ctx) (f a) member memb = lens (RL.get memb) (flip (RL.set memb)) @@ -399,6 +400,17 @@ instance NuMatchingAny1 f => NuMatchingAny1 (LLVMExtensionExpr f) where $(mkNuMatching [t| forall w f tp. NuMatchingAny1 f => LLVMStmt w f tp |]) -} +$(mkNuMatching [t| forall tp. GlobalVar tp |]) + +instance NuMatching (Nonce s tp) where + nuMatchingProof = unsafeMbTypeRepr + +instance Closable (Nonce s tp) where + toClosed = unsafeClose + +instance Liftable (Nonce s tp) where + mbLift = unClosed . mbLift . fmap toClosed + instance Closable (BV.BV w) where toClosed = unsafeClose @@ -729,7 +741,7 @@ cruCtxLookup (CruCtxCons _ tp) Member_Base = tp cruCtxLookup (CruCtxCons ctx _) (Member_Step memb) = cruCtxLookup ctx memb -- | Build a 'CruCtx' of the given length. -cruCtxReplicate :: NatRepr n -> TypeRepr a -> Some CruCtx +cruCtxReplicate :: NatRepr n -> TypeRepr a -> Some CruCtx cruCtxReplicate n tp = case isZeroNat n of ZeroNat -> Some CruCtxNil diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index df49b4e60f..4608dfcc18 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -470,7 +470,7 @@ data TypedLLVMStmt ret ps_in ps_out where -- Type: -- > ps, x:ptr((rw,0) |-> p), cur_ps -- > -o ps, x:ptr((rw,0) |-> eq(ret)), ret:p, cur_ps - TypedLLVMLoad :: + TypedLLVMLoad :: (HasPtrWidth w, 1 <= sz, KnownNat sz) => !(TypedReg (LLVMPointerType w)) -> !(LLVMFieldPerm w sz) -> @@ -540,7 +540,7 @@ data TypedLLVMStmt ret ps_in ps_out where -- referred to by a function pointer, assuming we know it has one: -- -- Type: @x:llvm_funptr(p) -o ret:p@ - TypedLLVMLoadHandle :: + TypedLLVMLoadHandle :: HasPtrWidth w => !(TypedReg (LLVMPointerType w)) -> !(TypeRepr (FunctionHandleType cargs ret)) -> @@ -1338,7 +1338,7 @@ entryByID entryID = over typedBlockEntries (replaceNth (blockEntryIx entryID blk) e) blk) --- | Build an empty 'TypedBlock' +-- | Build an empty 'TypedBlock' emptyBlockOfSort :: [Maybe String] -> Assignment CtxRepr cblocks -> @@ -1943,7 +1943,7 @@ runPermCheckM names entryID args ghosts mb_perms_in m = (tops_ns, args_ns) = RL.split Proxy args_prxs tops_args (arg_names, local_names) = initialNames args names st = emptyPermCheckState (distPermSet perms_in) tops_ns entryID local_names in - + let go x = runGenStateContT x st (\_ () -> pure ()) in go $ setVarTypes (Just "top") (noNames' stTopCtx) tops_ns stTopCtx >>> @@ -1967,7 +1967,7 @@ initialNames CruCtxNil xs = (MNil, xs) initialNames (CruCtxCons ts _) xs = case initialNames ts xs of (ys, z:zs) -> (ys :>: Constant z, zs) - (ys, [] ) -> (ys :>: Constant Nothing, []) + (ys, [] ) -> (ys :>: Constant Nothing, []) -- | Compute an empty debug name assignment from a known context noNames :: @@ -2641,7 +2641,7 @@ ppCruRegAndPerms ctx r = -- their permissions, the variables in those permissions etc., as in -- 'varPermsTransFreeVars' getRelevantPerms :: [SomeName CrucibleType] -> - PermCheckM ext cblocks blocks tops ret r ps r ps + PermCheckM ext cblocks blocks tops ret r ps r ps (Some DistPerms) getRelevantPerms (namesListToNames -> SomeRAssign ns) = gets stCurPerms >>>= \perms -> @@ -3121,7 +3121,7 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerIte w cond_reg then_reg else_reg) = PExpr_Bool True -> dbgNames >>= \names -> emitStmt knownRepr names loc - (TypedSetRegPermExpr knownRepr $ + (TypedSetRegPermExpr knownRepr $ PExpr_Var $ typedRegVar tthen_reg) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3140,7 +3140,7 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerIte w cond_reg then_reg else_reg) = pure (addCtxName ctx ret) -- For LLVM side conditions, treat each side condition as an assert -tcEmitLLVMSetExpr ctx loc (LLVM_SideConditions tp conds reg) = +tcEmitLLVMSetExpr ctx loc (LLVM_SideConditions _ tp conds reg) = let treg = tcReg ctx reg in foldr (\(LLVMSideCondition cond_reg ub) rest_m -> diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 32a3431019..a781fc2a88 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -742,7 +742,11 @@ checkSpecReturnType cc mspec = -- Returns a tuple of (arguments, preconditions, pointer values, -- memory). verifyPrestate :: - (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ( ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => Options -> LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> @@ -882,7 +886,11 @@ resolveArguments cc mem mspec env = mapM resolveArg [0..(nArgs-1)] -- | For each "llvm_global_alloc" in the method specification, allocate and -- register the appropriate memory. setupGlobalAllocs :: forall arch. - (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) => + ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> MemImpl -> @@ -928,7 +936,12 @@ setupGlobalAllocs cc mspec mem0 = foldM go mem0 $ mspec ^. MS.csGlobalAllocs -- function spec, write the given value to the address of the given -- pointer. setupPrePointsTos :: forall arch. - (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => MS.CrucibleMethodSpecIR (LLVM arch) -> Options -> LLVMCrucibleContext arch -> @@ -1010,7 +1023,11 @@ assertEqualVals cc v1 v2 = -- TODO(langston): combine with/move to executeAllocation doAlloc :: - (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ( ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => LLVMCrucibleContext arch -> AllocIndex -> LLVMAllocSpec -> @@ -1390,7 +1407,7 @@ setupLLVMCrucibleContext pathSat lm action = { Crucible.laxPointerOrdering = laxPointerOrdering } let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions - let ?recordLLVMAnnotation = \_ _ -> return () + let ?recordLLVMAnnotation = \_ _ _ -> return () let ?w4EvalTactic = W4EvalTactic { doW4Eval = what4Eval } let ?checkAllocSymInit = allocSymInitCheck cc <- diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 431e14edb7..0a0e2f439e 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -633,7 +633,12 @@ methodSpecHandler_prestate opts sc cc args cs = -- and computing postcondition predicates. methodSpecHandler_poststate :: forall arch ret. - (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> LLVMCrucibleContext arch {- ^ context for interacting with Crucible -} -> @@ -706,7 +711,12 @@ enforceCompleteSubstitution loc ss = -- execute a pre/post condition -executeCond :: (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) +executeCond :: ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => Options -> SharedContext -> LLVMCrucibleContext arch @@ -1615,6 +1625,7 @@ instantiateExtResolveSAWSymBV sc cc w tm = do -- Return a map containing the overwritten memory allocations. invalidateMutableAllocs :: ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions , ?w4EvalTactic :: W4EvalTactic , Crucible.HasPtrWidth (Crucible.ArchWidth arch) , Crucible.HasLLVMAnn Sym @@ -1707,7 +1718,12 @@ invalidateMutableAllocs opts sc cc cs = do -- | Perform an allocation as indicated by an @llvm_alloc@ or -- @llvm_fresh_pointer@ statement from the postcondition section. executeAllocation :: - (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1734,7 +1750,11 @@ executeAllocation opts sc cc (var, LLVMAllocSpec mut memTy alignment sz loc fres assignVar cc loc var ptr doAllocSymInit :: - (Crucible.IsSymInterface sym, Crucible.HasPtrWidth wptr, Crucible.HasLLVMAnn sym) => + ( ?memOpts :: Crucible.MemOptions + , Crucible.IsSymInterface sym + , Crucible.HasPtrWidth wptr + , Crucible.HasLLVMAnn sym + ) => sym -> Crucible.MemImpl sym -> Crucible.Mutability -> @@ -1799,7 +1819,12 @@ executeGhost _sc _var (TypedTerm tp _) = -- the CrucibleSetup block. First we compute the value indicated by -- 'val', and then write it to the address indicated by 'ptr'. executePointsTo :: - (?lc :: Crucible.TypeContext, ?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ( ?lc :: Crucible.TypeContext + , ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => Options -> SharedContext -> LLVMCrucibleContext arch -> @@ -1830,7 +1855,11 @@ executePointsTo opts sc cc spec overwritten_allocs (LLVMPointsTo _loc cond ptr v writeGlobal memVar mem' storePointsToValue :: - (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => + ( ?memOpts :: Crucible.MemOptions + , ?w4EvalTactic :: W4EvalTactic + , Crucible.HasPtrWidth (Crucible.ArchWidth arch) + , Crucible.HasLLVMAnn Sym + ) => Options -> LLVMCrucibleContext arch -> Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 03aa1efb8d..e24ea665d6 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -299,7 +299,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se start <- io getCurrentTime let ?ptrWidth = knownNat @64 let ?memOpts = C.LLVM.defaultMemOptions - let ?recordLLVMAnnotation = \_ _ -> return () + let ?recordLLVMAnnotation = \_ _ _ -> return () sc <- getSharedContext opts <- getOptions basic_ss <- getBasicSS diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index d2fb004ed5..815d398dad 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -401,7 +401,7 @@ translate opts elf fun = sayLn ("Translating function: " ++ BSC.unpack name) let ?memOpts = Crucible.defaultMemOptions - let ?recordLLVMAnnotation = \_ _ -> return () + let ?recordLLVMAnnotation = \_ _ _ -> return () let sym = backend opts sopts = Opts { optsSym = sym, optsCry = cryEnv opts, optsMvar = memvar opts }