diff --git a/deps/crucible b/deps/crucible index 584d47d384..708719b32c 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 584d47d384104c06a92b3820882639e9898e4b0d +Subproject commit 708719b32c43a2dfd63a5b357d96676fda7ba4d8 diff --git a/deps/flexdis86 b/deps/flexdis86 index 4e6f4950be..6d6e8c39e7 160000 --- a/deps/flexdis86 +++ b/deps/flexdis86 @@ -1 +1 @@ -Subproject commit 4e6f4950be909b41852b50e5648d243d948fa0c9 +Subproject commit 6d6e8c39e754dc4c9910b1c0dc494e2eef8e309f diff --git a/deps/macaw b/deps/macaw index d9fa8af6c8..764de152ce 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit d9fa8af6c8b2b9519883e150e7bed01665c5f9d4 +Subproject commit 764de152ceb0166aa04ec1a0ddbb2806b2595926 diff --git a/examples/salsa20/salsa20.bc b/examples/salsa20/salsa20.bc index 808474461b..bac4c70a9e 100644 Binary files a/examples/salsa20/salsa20.bc and b/examples/salsa20/salsa20.bc differ diff --git a/heapster-saw/heapster-saw.cabal b/heapster-saw/heapster-saw.cabal index 7c904aa5ff..c8d2a8c1cf 100644 --- a/heapster-saw/heapster-saw.cabal +++ b/heapster-saw/heapster-saw.cabal @@ -52,6 +52,7 @@ library Verifier.SAW.Heapster.Parser Verifier.SAW.Heapster.Permissions Verifier.SAW.Heapster.PermParser + Verifier.SAW.Heapster.NamePropagation Verifier.SAW.Heapster.RustTypes Verifier.SAW.Heapster.SAWTranslation Verifier.SAW.Heapster.Token diff --git a/heapster-saw/src/Verifier/SAW/Heapster/NamePropagation.hs b/heapster-saw/src/Verifier/SAW/Heapster/NamePropagation.hs new file mode 100644 index 0000000000..5fd0d662a2 --- /dev/null +++ b/heapster-saw/src/Verifier/SAW/Heapster/NamePropagation.hs @@ -0,0 +1,65 @@ +{-# Language ScopedTypeVariables #-} +{-# Language GADTs #-} +module Verifier.SAW.Heapster.NamePropagation where + +import Data.Functor.Constant +import Data.Parameterized.TraversableFC ( FoldableFC(toListFC), FunctorFC(fmapFC) ) +import Lang.Crucible.Analysis.Fixpoint +import Lang.Crucible.CFG.Core ( Some(Some), CFG(cfgHandle) ) +import Lang.Crucible.FunctionHandle ( FnHandle(handleArgTypes) ) +import Lang.Crucible.LLVM.Extension ( LLVM, LLVMStmt(..), LLVM_Dbg(..) ) +import qualified Data.Parameterized.Context as Ctx +import qualified Data.Parameterized.Map as PM +import qualified Text.LLVM.AST as L + +type NameDom = Pointed (Constant String) + +nameJoin :: Constant String a -> Constant String a -> NameDom a +nameJoin (Constant x) (Constant y) | x == y = Pointed (Constant x) +nameJoin _ _ = Top + +nameDomain :: Domain (Pointed (Constant String)) +nameDomain = pointed nameJoin (==) WTO + +nameInterpretation :: Interpretation LLVM NameDom +nameInterpretation = Interpretation + { interpExpr = \_ _ _ names -> (Just names, Bottom) + , interpCall = \_ _ _ _ _ names -> (Just names, Bottom) + , interpReadGlobal = \_ names -> (Just names, Bottom) + , interpWriteGlobal = \_ _ names -> Just names + , interpBr = \_ _ _ _ names -> (Just names, Just names) + , interpMaybe = \_ _ _ names -> (Just names, Bottom, Just names) + , interpExt = \_ stmt names -> + let names' = + case stmt of + LLVM_Debug (LLVM_Dbg_Declare ptr di _) | Just n <- L.dilvName di -> + modifyAbstractRegValue names ptr (\_ -> Pointed (Constant ("&" ++ n))) + LLVM_Debug (LLVM_Dbg_Addr ptr di _) | Just n <- L.dilvName di -> + modifyAbstractRegValue names ptr (\_ -> Pointed (Constant ("&" ++ n))) + LLVM_Debug (LLVM_Dbg_Value _ val di _) | Just n <- L.dilvName di -> + modifyAbstractRegValue names val (\_ -> Pointed (Constant n)) + _ -> names + in (Just names', Bottom) + } + +computeNames :: + forall blocks init ret. + CFG LLVM blocks init ret -> + Ctx.Assignment (Constant [Maybe String]) blocks +computeNames cfg = + case alg of + (_, end, _) -> fmapFC (\(Ignore (Some p)) -> Constant (toListFC flatten (_paRegisters p))) end + where + flatten :: NameDom a -> Maybe String + flatten Top = Nothing + flatten Bottom = Nothing + flatten (Pointed (Constant x)) = Just x + + sz = Ctx.size (handleArgTypes (cfgHandle cfg)) + alg = + forwardFixpoint' + nameDomain + nameInterpretation + cfg + PM.empty + (Ctx.replicate sz Bottom) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index c761009ecf..9da457a795 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -599,6 +599,8 @@ instance TransInfo info => return $ error "translate: RealValRepr" [nuMP| ComplexRealRepr |] -> return $ error "translate: ComplexRealRepr" + [nuMP| SequenceRepr{} |] -> + return $ error "translate: SequenceRepr" [nuMP| BVRepr w |] -> returnType1 =<< bitvectorTransM (translate w) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs index 3724d07053..2579b458b5 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs @@ -331,6 +331,7 @@ tcExpr WordMapRepr {} e = tcError (pos e) "Expected wordmap" tcExpr StringMapRepr {} e = tcError (pos e) "Expected stringmap" tcExpr SymbolicArrayRepr {} e = tcError (pos e) "Expected symbolicarray" tcExpr SymbolicStructRepr{} e = tcError (pos e) "Expected symbolicstruct" +tcExpr SequenceRepr {} e = tcError (pos e) "Expected sequencerepr" -- | Check for a unit literal tcUnit :: AstExpr -> Tc (PermExpr UnitType) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index 6eb98d5af4..3a48529668 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -77,6 +77,7 @@ import Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB import Verifier.SAW.Heapster.CruUtil import Verifier.SAW.Heapster.GenMonad import Verifier.SAW.Heapster.Implication +import Verifier.SAW.Heapster.NamePropagation import Verifier.SAW.Heapster.Permissions import Verifier.SAW.Heapster.Widening @@ -939,7 +940,6 @@ instance SubstVar PermVarSubst m => [nuMP| TypedLLVMIte w r1 r2 r3 |] -> TypedLLVMIte (mbLift w) <$> genSubst s r1 <*> genSubst s r2 <*> genSubst s r3 - instance (PermCheckExtC ext, SubstVar PermVarSubst m) => Substable PermVarSubst (TypedStmt ext rets ps_in ps_out) m where genSubst s mb_x = case mbMatch mb_x of @@ -1268,7 +1268,9 @@ data TypedBlock phase ext (blocks :: RList (RList CrucibleType)) tops ret args = -- disallowed for user-supplied permissions typedBlockCanWiden :: Bool, -- | The entrypoints into this block - _typedBlockEntries :: [Some (TypedEntry phase ext blocks tops ret args)] + _typedBlockEntries :: [Some (TypedEntry phase ext blocks tops ret args)], + -- | Debug name information for the current block + _typedBlockNames :: [Maybe String] } makeLenses ''TypedBlock @@ -1312,34 +1314,40 @@ entryByID entryID = -- | Build an empty 'TypedBlock' -emptyBlockOfSort :: Assignment CtxRepr cblocks -> TypedBlockSort -> - Block ext cblocks ret cargs -> - TypedBlock TCPhase ext (CtxCtxToRList - cblocks) tops ret (CtxToRList cargs) -emptyBlockOfSort cblocks sort blk +emptyBlockOfSort :: + [Maybe String] -> + Assignment CtxRepr cblocks -> + TypedBlockSort -> + Block ext cblocks ret cargs -> + TypedBlock TCPhase ext (CtxCtxToRList + cblocks) tops ret (CtxToRList cargs) +emptyBlockOfSort names cblocks sort blk | Refl <- reprReprToCruCtxCtxEq cblocks = TypedBlock (indexCtxToMember (size cblocks) $ - blockIDIndex $ blockID blk) blk sort True [] + blockIDIndex $ blockID blk) blk sort True [] names -- | Build a block with a user-supplied input permission -emptyBlockForPerms :: Assignment CtxRepr cblocks -> - Block ext cblocks ret cargs -> CruCtx tops -> - TypeRepr ret -> CruCtx ghosts -> - MbValuePerms ((tops :++: CtxToRList cargs) :++: ghosts) -> - MbValuePerms (tops :> ret) -> - TypedBlock TCPhase ext (CtxCtxToRList - cblocks) tops ret (CtxToRList cargs) -emptyBlockForPerms cblocks blk tops ret ghosts perms_in perms_out +emptyBlockForPerms :: + [Maybe String] -> + Assignment CtxRepr cblocks -> + Block ext cblocks ret cargs -> CruCtx tops -> + TypeRepr ret -> CruCtx ghosts -> + MbValuePerms ((tops :++: CtxToRList cargs) :++: ghosts) -> + MbValuePerms (tops :> ret) -> + TypedBlock TCPhase ext (CtxCtxToRList + cblocks) tops ret (CtxToRList cargs) +emptyBlockForPerms names cblocks blk tops ret ghosts perms_in perms_out | Refl <- reprReprToCruCtxCtxEq cblocks , blockID <- indexCtxToMember (size cblocks) $ blockIDIndex $ blockID blk , args <- mkCruCtx (blockInputs blk) = TypedBlock blockID blk JoinSort False - [Some $ TypedEntry { + [Some TypedEntry { typedEntryID = TypedEntryID blockID 0, typedEntryTops = tops, typedEntryArgs = args, typedEntryRet = ret, typedEntryCallers = [], typedEntryGhosts = ghosts, typedEntryPermsIn = perms_in, typedEntryPermsOut = perms_out, typedEntryBody = Nothing }] + names -- | Transition a 'TypedBlock' from type-checking to translation phase, by -- making sure that all of data needed for the translation phase is present @@ -1548,6 +1556,7 @@ funPermToBlockInputs fun_perm = -- supplied 'PermEnv' along with a list of 'Bool' flags indicating which blocks -- are at the head of a loop (or other strongly-connected component) initTypedBlockMap :: + KnownRepr ExtRepr ext => PermEnv -> FunPerm ghosts (CtxToRList init) ret -> CFG ext cblocks init ret -> @@ -1557,26 +1566,34 @@ initTypedBlockMap :: initTypedBlockMap env fun_perm cfg sccs = let block_map = cfgBlockMap cfg cblocks = fmapFC blockInputs block_map + namess = computeCfgNames knownRepr (size sccs) cfg ret = funPermRet fun_perm tops = funPermTops fun_perm top_perms_in = funPermToBlockInputs fun_perm perms_out = funPermOuts fun_perm in assignToRListRList - (\(Pair blk (Constant is_scc)) -> + (\(Pair blk (Pair (Constant is_scc) (Constant names))) -> let blkID = blockID blk hints = lookupBlockHints env (cfgHandle cfg) cblocks blkID in case hints of _ | Just Refl <- testEquality (cfgEntryBlockID cfg) blkID -> - emptyBlockForPerms cblocks blk tops ret CruCtxNil top_perms_in perms_out + emptyBlockForPerms names cblocks blk tops ret CruCtxNil top_perms_in perms_out (find isBlockEntryHint -> Just (BlockEntryHintSort tops' ghosts perms_in)) | Just Refl <- testEquality tops tops' -> - emptyBlockForPerms cblocks blk tops ret ghosts perms_in perms_out + emptyBlockForPerms names cblocks blk tops ret ghosts perms_in perms_out _ | is_scc || any isJoinPointHint hints -> - emptyBlockOfSort cblocks JoinSort blk - _ -> emptyBlockOfSort cblocks MultiEntrySort blk) $ - Ctx.zipWith Pair block_map sccs + emptyBlockOfSort names cblocks JoinSort blk + _ -> emptyBlockOfSort names cblocks MultiEntrySort blk) $ + Ctx.zipWith Pair block_map (Ctx.zipWith Pair sccs namess) +computeCfgNames :: + ExtRepr ext -> + Size cblocks -> + CFG ext cblocks init ret -> + Ctx.Assignment (Constant [Maybe String]) cblocks +computeCfgNames ExtRepr_LLVM _ cfg = computeNames cfg +computeCfgNames ExtRepr_Unit s _ = Ctx.replicate s (Constant []) -- | A typed Crucible CFG data TypedCFG @@ -1675,6 +1692,7 @@ makeLenses ''TopPermCheckState -- | Build an empty 'TopPermCheckState' from a Crucible 'BlockMap' emptyTopPermCheckState :: HasPtrWidth w => + KnownRepr ExtRepr ext => PermEnv -> FunPerm ghosts (CtxToRList init) ret -> EndianForm -> @@ -1788,21 +1806,27 @@ data PermCheckState ext blocks tops ret ps = stCurEntry :: !(Some (TypedEntryID blocks)), stVarTypes :: !(NameMap TypeRepr), stPPInfo :: !PPInfo, - stErrPrefix :: !(Maybe (Doc ())) + stErrPrefix :: !(Maybe (Doc ())), + stDebug :: ![Maybe String] } -- | Build a default, empty 'PermCheckState' -emptyPermCheckState :: KnownRepr ExtRepr ext => PermSet ps -> - RAssign ExprVar tops -> TypedEntryID blocks args -> - PermCheckState ext blocks tops ret ps -emptyPermCheckState perms tops entryID = +emptyPermCheckState :: + KnownRepr ExtRepr ext => + PermSet ps -> + RAssign ExprVar tops -> + TypedEntryID blocks args -> + [Maybe String] -> + PermCheckState ext blocks tops ret ps +emptyPermCheckState perms tops entryID names = PermCheckState { stCurPerms = perms, stExtState = emptyPermCheckExtState knownRepr, stTopVars = tops, stCurEntry = Some entryID, stVarTypes = NameMap.empty, stPPInfo = emptyPPInfo, - stErrPrefix = Nothing } + stErrPrefix = Nothing, + stDebug = names } -- | Like the 'set' method of a lens, but allows the @ps@ argument to change setSTCurPerms :: PermSet ps2 -> PermCheckState ext blocks tops ret ps1 -> @@ -1815,6 +1839,13 @@ modifySTCurPerms :: (PermSet ps1 -> PermSet ps2) -> PermCheckState ext blocks tops ret ps2 modifySTCurPerms f_perms st = setSTCurPerms (f_perms $ stCurPerms st) st +nextDebugName :: + PermCheckM ext cblocks blocks tops ret a ps a ps + (Maybe String) +nextDebugName = + do st <- get + put st { stDebug = drop 1 (stDebug st)} + pure (foldr (\x _ -> x) Nothing (stDebug st)) -- | The generalized monad for permission-checking type PermCheckM ext cblocks blocks tops ret r1 ps1 r2 ps2 = @@ -1870,14 +1901,16 @@ setInputExtState ExtRepr_LLVM _ _ = -- of top-level arguments, local arguments, ghost variables, and permissions on -- all three, and return a result inside a binding for these variables runPermCheckM :: - KnownRepr ExtRepr ext => TypedEntryID blocks some_args -> + KnownRepr ExtRepr ext => + [Maybe String] -> + TypedEntryID blocks some_args -> CruCtx args -> CruCtx ghosts -> MbValuePerms ((tops :++: args) :++: ghosts) -> (RAssign ExprVar tops -> RAssign ExprVar args -> RAssign ExprVar ghosts -> DistPerms ((tops :++: args) :++: ghosts) -> PermCheckM ext cblocks blocks tops ret () ps_out r ((tops :++: args) :++: ghosts) ()) -> TopPermCheckM ext cblocks blocks tops ret (Mb ((tops :++: args) :++: ghosts) r) -runPermCheckM entryID args ghosts mb_perms_in m = +runPermCheckM names entryID args ghosts mb_perms_in m = get >>= \(TopPermCheckState {..}) -> let args_prxs = cruCtxProxies args ghosts_prxs = cruCtxProxies ghosts in @@ -1885,16 +1918,66 @@ runPermCheckM entryID args ghosts mb_perms_in m = flip nuMultiWithElim1 (mbValuePermsToDistPerms mb_perms_in) $ \ns perms_in -> let (tops_args, ghosts_ns) = RL.split Proxy ghosts_prxs ns (tops_ns, args_ns) = RL.split Proxy args_prxs tops_args - st = emptyPermCheckState (distPermSet perms_in) tops_ns entryID in + (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 "top" tops_ns stTopCtx >>> - setVarTypes "local" args_ns args >>> - setVarTypes "ghost" ghosts_ns ghosts >>> + setVarTypes "top" (noNames' stTopCtx) tops_ns stTopCtx >>> + setVarTypes "local" arg_names args_ns args >>> + setVarTypes "ghost" (noNames' ghosts) ghosts_ns ghosts >>> setInputExtState knownRepr ghosts ghosts_ns >>> m tops_ns args_ns ghosts_ns perms_in +rassignLen :: RAssign f x -> Int +rassignLen = go 0 + where + go :: Int -> RAssign f x -> Int + go acc MNil = acc + go acc (xs :>: _) = (go $! (acc+1)) xs + +initialNames :: + CruCtx tps -> + [Maybe String] -> + (RAssign (Constant (Maybe String)) tps, [Maybe String]) +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, []) + +-- | Compute an empty debug name assignment from a known context +noNames :: + KnownRepr CruCtx tps => + RAssign (Constant (Maybe String)) tps +noNames = noNames' knownRepr + +-- | Compute an empty debug name assignment from a given context +noNames' :: + CruCtx tps -> + RAssign (Constant (Maybe String)) tps +noNames' CruCtxNil = MNil +noNames' (CruCtxCons xs _) = noNames' xs :>: Constant Nothing + +-- | Call 'debugNames'' with a known type list. +dbgNames :: + KnownRepr CruCtx tps => + PermCheckM ext cblocks blocks tops ret a ps a ps + (RAssign (Constant (Maybe String)) tps) +dbgNames = dbgNames' knownRepr + +-- | Pop as many local variable names from the debug information +-- as needed to populate the given type list. +dbgNames' :: + CruCtx tps -> + PermCheckM ext cblocks blocks tops ret a ps a ps + (RAssign (Constant (Maybe String)) tps) +dbgNames' CruCtxNil = pure MNil +dbgNames' (CruCtxCons ts _) = + do ns <- dbgNames' ts + n <- nextDebugName + pure (ns :>: Constant n) + -- | Emit a 'TypedBlockMapDelta', which must be 'Closed', in an -- 'InnerPermCheckM' computation innerEmitDelta :: Closed (TypedBlockMapDelta blocks tops ret) -> @@ -2093,20 +2176,34 @@ getVarTypes MNil = pure CruCtxNil getVarTypes (xs :>: x) = CruCtxCons <$> getVarTypes xs <*> getVarType x -- | Remember the type of a free variable, and ensure that it has a permission -setVarType :: String -> ExprVar a -> TypeRepr a -> - PermCheckM ext cblocks blocks tops ret r ps r ps () -setVarType str x tp = +setVarType :: + String -> + Maybe String -> + ExprVar a -> + TypeRepr a -> + PermCheckM ext cblocks blocks tops ret r ps r ps () +setVarType str dbg x tp = + let str' = + case dbg of + Nothing -> str + Just d -> "C[" ++ d ++ "]" + in modify $ \st -> st { stCurPerms = initVarPerm x (stCurPerms st), stVarTypes = NameMap.insert x tp (stVarTypes st), - stPPInfo = ppInfoAddExprName str x (stPPInfo st) } + stPPInfo = ppInfoAddExprName str' x (stPPInfo st) } -- | Remember the types of a sequence of free variables -setVarTypes :: String -> RAssign Name tps -> CruCtx tps -> - PermCheckM ext cblocks blocks tops ret r ps r ps () -setVarTypes _ _ CruCtxNil = pure () -setVarTypes str (xs :>: x) (CruCtxCons tps tp) = - setVarTypes str xs tps >>> setVarType str x tp +setVarTypes :: + String -> + RAssign (Constant (Maybe String)) tps -> + RAssign Name tps -> + CruCtx tps -> + PermCheckM ext cblocks blocks tops ret r ps r ps () +setVarTypes _ MNil MNil CruCtxNil = pure () +setVarTypes str (ds :>: Constant d) (ns :>: n) (CruCtxCons ts t) = + do setVarTypes str ds ns ts + setVarType str d n t -- | Get the current 'PPInfo' permGetPPInfo :: PermCheckM ext cblocks blocks tops ret r ps r ps PPInfo @@ -2330,9 +2427,10 @@ convertRegType _ loc reg (BVRepr w1) tp2@(BVRepr w2) | Left LeqProof <- decideLeq (knownNat :: NatRepr 1) w2 , NatCaseGT LeqProof <- testNatCases w1 w2 = withKnownNat w2 $ - emitStmt knownRepr loc (TypedSetReg tp2 $ - TypedExpr (BVTrunc w2 w1 $ RegNoVal reg) - Nothing) >>>= \(_ :>: x) -> + emitStmt knownRepr noNames loc + (TypedSetReg tp2 $ + TypedExpr (BVTrunc w2 w1 $ RegNoVal reg) + Nothing) >>>= \(MNil :>: x) -> stmtRecombinePerms >>> pure (TypedReg x) convertRegType _ loc reg (BVRepr w1) tp2@(BVRepr w2) @@ -2342,9 +2440,10 @@ convertRegType _ loc reg (BVRepr w1) tp2@(BVRepr w2) -- FIXME: should this use endianness? -- (stEndianness <$> top_get) >>>= \endianness -> withKnownNat w2 $ - emitStmt knownRepr loc (TypedSetReg tp2 $ - TypedExpr (BVSext w2 w1 $ RegNoVal reg) - Nothing) >>>= \(_ :>: x) -> + emitStmt knownRepr noNames loc + (TypedSetReg tp2 $ + TypedExpr (BVSext w2 w1 $ RegNoVal reg) + Nothing) >>>= \(MNil :>: x) -> stmtRecombinePerms >>> pure (TypedReg x) convertRegType ExtRepr_LLVM loc reg (LLVMPointerRepr w1) (BVRepr w2) @@ -2352,7 +2451,7 @@ convertRegType ExtRepr_LLVM loc reg (LLVMPointerRepr w1) (BVRepr w2) withKnownNat w1 $ stmtProvePerm reg (llvmExEqWord w1) >>>= \sbst -> let e = substLookup sbst Member_Base in - emitLLVMStmt knownRepr loc (DestructLLVMWord reg e) >>>= \x -> + emitLLVMStmt knownRepr Nothing loc (DestructLLVMWord reg e) >>>= \x -> stmtRecombinePerms >>> pure (TypedReg x) convertRegType ext loc reg (LLVMPointerRepr w1) (BVRepr w2) = @@ -2361,7 +2460,7 @@ convertRegType ext loc reg (LLVMPointerRepr w1) (BVRepr w2) = convertRegType ExtRepr_LLVM loc reg (BVRepr w2) (LLVMPointerRepr w1) | Just Refl <- testEquality w1 w2 = withKnownNat w1 $ - emitLLVMStmt knownRepr loc (ConstructLLVMWord reg) >>>= \x -> + emitLLVMStmt knownRepr Nothing loc (ConstructLLVMWord reg) >>>= \x -> stmtRecombinePerms >>> pure (TypedReg x) convertRegType ext loc reg (BVRepr w1) (LLVMPointerRepr w2) = convertRegType ext loc reg (BVRepr w1) (BVRepr w2) >>>= \reg' -> @@ -2393,9 +2492,10 @@ extractBVBytes loc sz off_bytes (reg :: TypedReg (BVType w)) = | Just (Some off) <- someNat (bytesToBits off_bytes) , Left off_sz_w_pf <- decideLeq (addNat off sz) w -> withLeqProof sz_pf $ withLeqProof off_sz_w_pf $ - emitStmt knownRepr loc (TypedSetReg (BVRepr sz) $ - TypedExpr (BVSelect off sz w $ RegNoVal reg) - Nothing) >>>= \(_ :>: x) -> + emitStmt knownRepr noNames loc + (TypedSetReg (BVRepr sz) $ + TypedExpr (BVSelect off sz w $ RegNoVal reg) + Nothing) >>>= \(MNil :>: x) -> stmtRecombinePerms >>> pure (TypedReg x) @@ -2406,9 +2506,10 @@ extractBVBytes loc sz off_bytes (reg :: TypedReg (BVType w)) = - intValue sz) , Left idx_sz_w_pf <- decideLeq (addNat idx sz) w -> withLeqProof sz_pf $ withLeqProof idx_sz_w_pf $ - emitStmt knownRepr loc (TypedSetReg (BVRepr sz) $ - TypedExpr (BVSelect idx sz w $ RegNoVal reg) - Nothing) >>>= \(_ :>: x) -> + emitStmt knownRepr noNames loc + (TypedSetReg (BVRepr sz) $ + TypedExpr (BVSelect idx sz w $ RegNoVal reg) + Nothing) >>>= \(MNil :>: x) -> stmtRecombinePerms >>> pure (TypedReg x) _ -> error "extractBVBytes: negative offset!" @@ -2418,26 +2519,32 @@ extractBVBytes loc sz off_bytes (reg :: TypedReg (BVType w)) = -- function says how that statement modifies the current permissions, given the -- freshly-bound names for the return values. Return those freshly-bound names -- for the return values. -emitStmt :: CruCtx rets -> ProgramLoc -> - TypedStmt ext rets ps_in ps_out -> - StmtPermCheckM ext cblocks blocks tops ret ps_out ps_in - (RAssign Name rets) -emitStmt tps loc stmt = +emitStmt :: + CruCtx rets -> + RAssign (Constant (Maybe String)) rets -> + ProgramLoc -> + TypedStmt ext rets ps_in ps_out -> + StmtPermCheckM ext cblocks blocks tops ret ps_out ps_in + (RAssign Name rets) +emitStmt tps names loc stmt = gopenBinding ((TypedConsStmt loc stmt (cruCtxProxies tps) <$>) . strongMbM) (mbPure (cruCtxProxies tps) ()) >>>= \(ns, ()) -> - setVarTypes "x" ns tps >>> + setVarTypes "x" names ns tps >>> gmodify (modifySTCurPerms (applyTypedStmt stmt ns)) >>> pure ns -- | Call emitStmt with a 'TypedLLVMStmt' -emitLLVMStmt :: TypeRepr tp -> ProgramLoc -> +emitLLVMStmt :: + TypeRepr tp -> + Maybe String -> + ProgramLoc -> TypedLLVMStmt tp ps_in ps_out -> StmtPermCheckM LLVM cblocks blocks tops ret ps_out ps_in (Name tp) -emitLLVMStmt tp loc stmt = - RL.head <$> emitStmt (singletonCruCtx tp) loc (TypedLLVMStmt stmt) +emitLLVMStmt tp name loc stmt = + RL.head <$> emitStmt (singletonCruCtx tp) (RL.singleton (Constant name)) loc (TypedLLVMStmt stmt) -- | A program location for code which was generated by the type-checker checkerProgramLoc :: ProgramLoc @@ -2513,17 +2620,23 @@ getRelevantPerms (namesListToNames -> SomeRAssign ns) = -- to, and then pretty-print the permissions on those variables and all -- variables they contain, as well as the top-level input variables and the -- extension-specific variables -ppCruRegsAndTopsPerms :: CtxTrans ctx -> [Some (Reg ctx)] -> - PermCheckM ext cblocks blocks tops ret r ps r ps (Doc (), Doc ()) -ppCruRegsAndTopsPerms ctx regs = +ppCruRegsAndTopsPerms :: + [Maybe String] -> + CtxTrans ctx -> + [Some (Reg ctx)] -> + PermCheckM ext cblocks blocks tops ret r ps r ps (Doc (), Doc ()) +ppCruRegsAndTopsPerms names ctx regs = permGetPPInfo >>>= \ppInfo -> gets stTopVars >>>= \tops -> gets (permCheckExtStateNames . stExtState) >>>= \(Some ext_ns) -> let vars_pp = fillSep $ punctuate comma $ - map (\case Some r -> - pretty r <+> pretty '=' <+> - permPretty ppInfo (tcReg ctx r)) regs + map (\(Some r) -> + let name = listToMaybe (drop (indexVal (regIndex r)) names) in + pretty r <+> pretty '=' <+> + permPretty ppInfo (tcReg ctx r) <> + foldMap (\n -> pretty " @" <+> pretty n) name) + (nub regs) vars = namesToNamesList tops ++ namesToNamesList ext_ns ++ map (\(Some r) -> SomeName $ typedRegVar $ tcReg ctx r) regs in @@ -2532,10 +2645,15 @@ ppCruRegsAndTopsPerms ctx regs = Some perms -> pure (vars_pp, permPretty ppInfo perms) -- | Set the current prefix string to give context to error messages -setErrorPrefix :: ProgramLoc -> Doc () -> CtxTrans ctx -> [Some (Reg ctx)] -> - PermCheckM ext cblocks blocks tops ret r ps r ps () -setErrorPrefix loc stmt_pp ctx regs = - ppCruRegsAndTopsPerms ctx regs >>>= \(regs_pp, perms_pp) -> +setErrorPrefix :: + [Maybe String] -> + ProgramLoc -> + Doc () -> + CtxTrans ctx -> + [Some (Reg ctx)] -> + PermCheckM ext cblocks blocks tops ret r ps r ps () +setErrorPrefix names loc stmt_pp ctx regs = + ppCruRegsAndTopsPerms names ctx regs >>>= \(regs_pp, perms_pp) -> let prefix = PP.sep [PP.group (pretty "At" <+> ppShortFileName (plSourceLoc loc) @@ -2787,7 +2905,9 @@ tcEmitStmt' ctx loc (SetReg tp (App e)) = traverseFC (tcRegWithVal ctx) e >>= \e_with_vals -> tcExpr e_with_vals >>= \maybe_val -> let typed_e = TypedExpr e_with_vals maybe_val in - emitStmt (singletonCruCtx tp) loc (TypedSetReg tp typed_e) >>>= \(_ :>: x) -> + let rets = (singletonCruCtx tp) in + dbgNames' rets >>= \names -> + emitStmt rets names loc (TypedSetReg tp typed_e) >>>= \(_ :>: x) -> stmtRecombinePerms >>> pure (addCtxName ctx x) @@ -2827,9 +2947,11 @@ tcEmitStmt' ctx loc (CallHandle ret freg_untyped _args_ctx args_untyped) = stmtProvePermsAppend CruCtxNil (emptyMb $ eqDistPerms ghosts_ns gexprs) >>>= \_ -> stmtProvePerm freg (emptyMb $ ValPerm_Conj1 $ Perm_Fun fun_perm) >>>= \_ -> - (emitStmt (singletonCruCtx ret) loc - (TypedCall freg fun_perm (varsToTypedRegs - ghosts_ns) gexprs args)) >>>= \(_ :>: ret') -> + let rets = singletonCruCtx ret in + dbgNames' rets >>>= \names -> + emitStmt rets names loc + (TypedCall freg fun_perm + (varsToTypedRegs ghosts_ns) gexprs args) >>>= \(_ :>: ret') -> stmtRecombinePerms >>> pure (addCtxName ctx ret') @@ -2838,7 +2960,7 @@ tcEmitStmt' ctx loc (Assert reg msg) = getRegEqualsExpr treg >>= \case PExpr_Bool True -> pure ctx PExpr_Bool False -> stmtFailM (\_ -> pretty "Failed assertion") - _ -> ctx <$ emitStmt CruCtxNil loc (TypedAssert (tcReg ctx reg) (tcReg ctx msg)) + _ -> ctx <$ emitStmt CruCtxNil MNil loc (TypedAssert (tcReg ctx reg) (tcReg ctx msg)) tcEmitStmt' _ _ _ = error "tcEmitStmt: unsupported statement" @@ -2858,8 +2980,9 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerExpr w blk_reg off_reg) = tblk_reg = tcReg ctx blk_reg in resolveConstant tblk_reg >>= \case Just 0 -> + nextDebugName >>>= \name -> withKnownNat w $ - emitLLVMStmt knownRepr loc (ConstructLLVMWord toff_reg) >>>= \x -> + emitLLVMStmt knownRepr name loc (ConstructLLVMWord toff_reg) >>>= \x -> stmtRecombinePerms >>> pure (addCtxName ctx x) _ -> stmtFailM (\i -> pretty "LLVM_PointerExpr: Non-zero pointer block: " @@ -2882,14 +3005,18 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerBlock w ptr_reg) = withKnownNat w $ getAtomicOrWordLLVMPerms tptr_reg >>>= \case Left e -> - emitLLVMStmt knownRepr loc (AssertLLVMWord tptr_reg e) >>>= \ret -> + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc (AssertLLVMWord tptr_reg e) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) Right _ -> stmtRecombinePerms >>> stmtProvePerm tptr_reg (emptyMb $ ValPerm_Conj1 Perm_IsLLVMPtr) >>> - emitLLVMStmt knownRepr loc (AssertLLVMPtr tptr_reg) >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ + emitLLVMStmt knownRepr Nothing loc (AssertLLVMPtr tptr_reg) >>> + dbgNames >>>= \names -> + emitStmt + knownRepr names loc + (TypedSetReg knownRepr $ TypedExpr (NatLit 1) (Just $ PExpr_Nat 1)) >>>= \(_ :>: ret) -> stmtRecombinePerms >>> @@ -2912,17 +3039,20 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerOffset w ptr_reg) = getAtomicOrWordLLVMPerms tptr_reg >>>= \eith -> case eith of Left e -> - emitLLVMStmt knownRepr loc (DestructLLVMWord + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc (DestructLLVMWord tptr_reg e) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) Right _ -> stmtRecombinePerms >>> stmtProvePerm tptr_reg (emptyMb $ ValPerm_Conj1 Perm_IsLLVMPtr) >>> - emitLLVMStmt knownRepr loc (AssertLLVMPtr tptr_reg) >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BVLit w $ BV.mkBV w 0) - (Just $ bvInt 0)) >>>= \(_ :>: ret) -> + emitLLVMStmt knownRepr Nothing loc (AssertLLVMPtr tptr_reg) >>> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BVLit w $ BV.mkBV w 0) + (Just $ bvInt 0)) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -2935,17 +3065,22 @@ tcEmitLLVMSetExpr ctx loc (LLVM_PointerIte w cond_reg then_reg else_reg) = telse_reg = tcReg ctx else_reg in getRegEqualsExpr tcond_reg >>= \case PExpr_Bool True -> - emitStmt knownRepr loc (TypedSetRegPermExpr knownRepr $ PExpr_Var $ - typedRegVar tthen_reg) >>>= \(_ :>: ret) -> + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetRegPermExpr knownRepr $ + PExpr_Var $ typedRegVar tthen_reg) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) PExpr_Bool False -> - emitStmt knownRepr loc (TypedSetRegPermExpr knownRepr $ PExpr_Var $ - typedRegVar telse_reg) >>>= \(_ :>: ret) -> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetRegPermExpr knownRepr $ + PExpr_Var $ typedRegVar telse_reg) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) _ -> - emitLLVMStmt knownRepr loc (TypedLLVMIte w + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc (TypedLLVMIte w tcond_reg tthen_reg telse_reg) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -2962,15 +3097,20 @@ tcEmitLLVMSetExpr ctx loc (LLVM_SideConditions tp conds reg) = rest_m PExpr_Bool False -> stmtFailM (\_ -> pretty err_str) _ -> - emitStmt knownRepr loc (TypedSetRegPermExpr knownRepr $ - PExpr_String err_str) >>>= \(_ :>: str_var) -> + emitStmt knownRepr noNames loc + (TypedSetRegPermExpr knownRepr $ + PExpr_String err_str) >>>= \(MNil :>: str_var) -> stmtRecombinePerms >>> - emitStmt CruCtxNil loc (TypedAssert tcond_reg $ - TypedReg str_var) >>>= \_ -> + emitStmt CruCtxNil MNil loc + (TypedAssert tcond_reg $ + TypedReg str_var) >>>= \MNil -> stmtRecombinePerms >>> rest_m) - (emitStmt (singletonCruCtx tp) loc (TypedSetRegPermExpr tp $ PExpr_Var $ - typedRegVar treg) >>>= \(_ :>: ret) -> + (let rets = singletonCruCtx tp in + dbgNames' rets >>>= \names -> + emitStmt rets names loc + (TypedSetRegPermExpr tp $ PExpr_Var $ + typedRegVar treg) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret)) conds @@ -3019,7 +3159,7 @@ emitTypedLLVMLoad :: (Name (LLVMPointerType sz)) emitTypedLLVMLoad _ loc treg fp ps = withLifetimeCurrentPerms (llvmFieldLifetime fp) $ \cur_perms -> - emitLLVMStmt knownRepr loc (TypedLLVMLoad treg fp ps cur_perms) + emitLLVMStmt knownRepr Nothing loc (TypedLLVMLoad treg fp ps cur_perms) -- | Emit a 'TypedLLVMStore' instruction, assuming the given LLVM field @@ -3030,6 +3170,7 @@ emitTypedLLVMLoad _ loc treg fp ps = emitTypedLLVMStore :: (HasPtrWidth w, 1 <= sz, KnownNat sz) => Proxy arch -> + Maybe String -> ProgramLoc -> TypedReg (LLVMPointerType w) -> LLVMFieldPerm w sz -> @@ -3039,9 +3180,9 @@ emitTypedLLVMStore :: (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) (Name UnitType) -emitTypedLLVMStore _ loc treg_ptr fp e ps = +emitTypedLLVMStore _ name loc treg_ptr fp e ps = withLifetimeCurrentPerms (llvmFieldLifetime fp) $ \cur_perms -> - emitLLVMStmt knownRepr loc (TypedLLVMStore treg_ptr fp e ps cur_perms) + emitLLVMStmt knownRepr name loc (TypedLLVMStore treg_ptr fp e ps cur_perms) open :: HasPtrWidth wptr => f (LLVMPointerType wptr) -> NatRepr wptr open _ = ?ptrWidth @@ -3088,7 +3229,8 @@ tcEmitLLVMStmt arch ctx loc (LLVM_Store _ ptr tp storage _ val) stmtProvePerm tptr (llvmWriteTrueExLPerm sz $ bvInt 0) >>>= \sbst -> let l = substLookup sbst Member_Base in let fp = llvmFieldWriteTrueL sz (bvInt 0) l in - emitTypedLLVMStore arch loc tptr fp + nextDebugName >>>= \name -> + emitTypedLLVMStore arch name loc tptr fp (PExpr_Var $ typedRegVar tval') DistPermsNil >>>= \z -> stmtRecombinePerms >>> pure (addCtxName ctx z) @@ -3104,13 +3246,15 @@ tcEmitLLVMStmt arch ctx loc (LLVM_MemClear _ (ptr :: Reg ctx (LLVMPointerType wp (forM_ @_ @_ @_ @() flds $ \case LLVMArrayField fp -> stmtProvePerm tptr (emptyMb $ ValPerm_Conj1 $ Perm_LLVMField fp) >>> - emitTypedLLVMStore arch loc tptr fp (PExpr_LLVMWord (bvInt 0)) DistPermsNil >>> + emitTypedLLVMStore arch Nothing loc tptr fp (PExpr_LLVMWord (bvInt 0)) DistPermsNil >>> stmtRecombinePerms) >>> -- Return a fresh unit variable - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr EmptyApp - (Just PExpr_Unit)) >>>= \(_ :>: z) -> + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr EmptyApp + (Just PExpr_Unit)) >>>= \(MNil :>: z) -> stmtRecombinePerms >>> pure (addCtxName ctx z) @@ -3143,7 +3287,9 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_Alloca w _ sz_reg _ _) = case (maybe_fp, fp_perm, maybe_sz) of (Just fp, ValPerm_Conj [Perm_LLVMFrame fperms], Just sz) -> stmtProvePerm fp (emptyMb fp_perm) >>>= \_ -> - emitLLVMStmt knownRepr loc (TypedLLVMAlloca fp fperms sz) >>>= \y -> + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc + (TypedLLVMAlloca fp fperms sz) >>>= \y -> stmtRecombinePerms >>> pure (addCtxName ctx y) (_, _, Nothing) -> @@ -3160,11 +3306,13 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_Alloca w _ sz_reg _ _) = tcEmitLLVMStmt _arch ctx loc (LLVM_PushFrame _ _) = fmap stArchWidth top_get >>>= \SomePtrWidth -> withKnownNat ?ptrWidth $ - emitLLVMStmt knownRepr loc TypedLLVMCreateFrame >>>= \fp -> + emitLLVMStmt knownRepr Nothing loc TypedLLVMCreateFrame >>>= \fp -> setFramePtr ?ptrWidth (TypedReg fp) >>> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetReg knownRepr - (TypedExpr EmptyApp Nothing)) >>>= \(_ :>: y) -> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr + (TypedExpr EmptyApp Nothing)) >>>= \(MNil :>: y) -> stmtRecombinePerms >>> pure (addCtxName ctx y) @@ -3178,8 +3326,9 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PopFrame _) = | Some del_perms <- llvmFrameDeletionPerms fperms -> stmtProvePerms knownRepr (distPermsToExDistPerms del_perms) >>>= \_ -> stmtProvePerm fp (emptyMb fp_perm) >>>= \_ -> - emitLLVMStmt knownRepr loc (TypedLLVMDeleteFrame - fp fperms del_perms) >>>= \y -> + nextDebugName >>>= \name -> + emitLLVMStmt knownRepr name loc + (TypedLLVMDeleteFrame fp fperms del_perms) >>>= \y -> modify (\st -> st { stExtState = PermCheckExtState_LLVM Nothing }) >>> pure (addCtxName ctx y) _ -> stmtFailM (const $ pretty "LLVM_PopFrame: no frame perms") @@ -3189,8 +3338,9 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrAddOffset _w _ ptr off) = let tptr = tcReg ctx ptr toff = tcReg ctx off in getRegEqualsExpr toff >>>= \off_expr -> + nextDebugName >>>= \name -> withKnownNat ?ptrWidth $ - emitLLVMStmt knownRepr loc (OffsetLLVMValue tptr off_expr) >>>= \ret -> + emitLLVMStmt knownRepr name loc (OffsetLLVMValue tptr off_expr) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3208,7 +3358,8 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_LoadHandle _ _ ptr args ret) = , Just Refl <- testEquality tp (FunctionHandleRepr args ret) -> stmtEmbedImplM (implCopyConjM x ps i >>> recombinePerm x (ValPerm_Conj ps)) >>> - emitLLVMStmt (FunctionHandleRepr args ret) loc + nextDebugName >>>= \name -> + emitLLVMStmt (FunctionHandleRepr args ret) name loc (TypedLLVMLoadHandle tptr tp p) >>>= \ret' -> stmtRecombinePerms >>> pure (addCtxName ctx ret') @@ -3219,8 +3370,9 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_ResolveGlobal w _ gsym) = (stPermEnv <$> top_get) >>>= \env -> case lookupGlobalSymbol env gsym w of Just (p, _) -> + nextDebugName >>>= \name -> withKnownNat ?ptrWidth $ - emitLLVMStmt knownRepr loc (TypedLLVMResolveGlobal gsym p) >>>= \ret -> + emitLLVMStmt knownRepr name loc (TypedLLVMResolveGlobal gsym p) >>>= \ret -> stmtRecombinePerms >>> pure (addCtxName ctx ret) Nothing -> @@ -3318,17 +3470,19 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) -- FIXME: if we have bvEq e1' e2' or not (bvCouldEqual e1' e2') then we -- should return a known Boolean value in place of the Nothing (PExpr_LLVMWord e1', PExpr_LLVMWord e2') -> - emitStmt knownRepr loc (TypedSetRegPermExpr - knownRepr e1') >>>= \(_ :>: n1) -> + emitStmt knownRepr noNames loc (TypedSetRegPermExpr + knownRepr e1') >>>= \(MNil :>: n1) -> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetRegPermExpr - knownRepr e2') >>>= \(_ :>: n2) -> + emitStmt knownRepr noNames loc (TypedSetRegPermExpr + knownRepr e2') >>>= \(MNil :>: n2) -> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BaseIsEq knownRepr - (RegWithVal (TypedReg n1) e1') - (RegWithVal (TypedReg n2) e2')) - Nothing) >>>= \(_ :>: ret) -> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BaseIsEq knownRepr + (RegWithVal (TypedReg n1) e1') + (RegWithVal (TypedReg n2) e2')) + Nothing) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3337,17 +3491,19 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) -- FIXME: test off1 == off2 like above (asLLVMOffset -> Just (x1', off1), asLLVMOffset -> Just (x2', off2)) | x1' == x2' -> - emitStmt knownRepr loc (TypedSetRegPermExpr - knownRepr off1) >>>= \(_ :>: n1) -> + emitStmt knownRepr noNames loc (TypedSetRegPermExpr + knownRepr off1) >>>= \(MNil :>: n1) -> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetRegPermExpr - knownRepr off2) >>>= \(_ :>: n2) -> + emitStmt knownRepr noNames loc (TypedSetRegPermExpr + knownRepr off2) >>>= \(MNil :>: n2) -> stmtRecombinePerms >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BaseIsEq knownRepr - (RegWithVal (TypedReg n1) off1) - (RegWithVal (TypedReg n2) off2)) - Nothing) >>>= \(_ :>: ret) -> + dbgNames >>>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BaseIsEq knownRepr + (RegWithVal (TypedReg n1) off1) + (RegWithVal (TypedReg n2) off2)) + Nothing) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3357,10 +3513,12 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) (PExpr_LLVMWord _e, asLLVMOffset -> Just (x', _)) -> let r' = TypedReg x' in stmtProvePerm r' (emptyMb $ ValPerm_Conj1 Perm_IsLLVMPtr) >>> - emitLLVMStmt knownRepr loc (AssertLLVMPtr r') >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BoolLit False) - Nothing) >>>= \(_ :>: ret) -> + emitLLVMStmt knownRepr Nothing loc (AssertLLVMPtr r') >>> + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BoolLit False) + Nothing) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3368,10 +3526,12 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) (asLLVMOffset -> Just (x', _), PExpr_LLVMWord _e) -> let r' = TypedReg x' in stmtProvePerm r' (emptyMb $ ValPerm_Conj1 Perm_IsLLVMPtr) >>> - emitLLVMStmt knownRepr loc (AssertLLVMPtr r') >>> - emitStmt knownRepr loc (TypedSetReg knownRepr $ - TypedExpr (BoolLit False) - Nothing) >>>= \(_ :>: ret) -> + emitLLVMStmt knownRepr Nothing loc (AssertLLVMPtr r') >>> + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr $ + TypedExpr (BoolLit False) + Nothing) >>>= \(MNil :>: ret) -> stmtRecombinePerms >>> pure (addCtxName ctx ret) @@ -3382,6 +3542,14 @@ tcEmitLLVMStmt _arch ctx loc (LLVM_PtrEq _ (r1 :: Reg ctx (LLVMPointerType wptr) sep [pretty "Could not compare LLVM pointer values", permPretty i x1, pretty "and", permPretty i x2]) +tcEmitLLVMStmt _arch ctx loc LLVM_Debug{} = +-- let tptr = tcReg ctx ptr in + dbgNames >>= \names -> + emitStmt knownRepr names loc + (TypedSetReg knownRepr (TypedExpr EmptyApp Nothing)) >>>= \(MNil :>: ret) -> + stmtRecombinePerms >>> + pure (addCtxName ctx ret) + tcEmitLLVMStmt _arch _ctx _loc stmt = error ("tcEmitLLVMStmt: unimplemented statement - " ++ show (ppApp (\_ -> mempty) stmt)) @@ -3701,30 +3869,32 @@ tcTermStmt _ tstmt = -- an empty stack of distinguished permissions tcEmitStmtSeq :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => + [Maybe String] -> CtxTrans ctx -> StmtSeq ext cblocks ret ctx -> PermCheckM ext cblocks blocks tops ret () RNil (TypedStmtSeq ext blocks tops ret RNil) RNil () -tcEmitStmtSeq ctx (ConsStmt loc stmt stmts) = - setErrorPrefix loc (ppStmt (Ctx.size ctx) stmt) ctx (stmtInputRegs stmt) >>> - tcEmitStmt ctx loc stmt >>>= \ctx' -> tcEmitStmtSeq ctx' stmts -tcEmitStmtSeq ctx (TermStmt loc tstmt) = - setErrorPrefix loc (pretty tstmt) ctx (termStmtRegs tstmt) >>> +tcEmitStmtSeq names ctx (ConsStmt loc stmt stmts) = + setErrorPrefix names loc (ppStmt (Ctx.size ctx) stmt) ctx (stmtInputRegs stmt) >>> + tcEmitStmt ctx loc stmt >>>= \ctx' -> tcEmitStmtSeq names ctx' stmts +tcEmitStmtSeq names ctx (TermStmt loc tstmt) = + setErrorPrefix names loc (pretty tstmt) ctx (termStmtRegs tstmt) >>> tcTermStmt ctx tstmt >>>= \typed_tstmt -> gmapRet (>> return (TypedTermStmt loc typed_tstmt)) -- | Type-check the body of a Crucible block as the body of an entrypoint tcBlockEntryBody :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => + [Maybe String] -> Block ext cblocks ret args -> TypedEntry TCPhase ext blocks tops ret (CtxToRList args) ghosts -> TopPermCheckM ext cblocks blocks tops ret (Mb ((tops :++: CtxToRList args) :++: ghosts) (TypedStmtSeq ext blocks tops ret ((tops :++: CtxToRList args) :++: ghosts))) -tcBlockEntryBody blk entry@(TypedEntry {..}) = - runPermCheckM typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $ +tcBlockEntryBody names blk entry@(TypedEntry {..}) = + runPermCheckM names typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $ \tops_ns args_ns ghosts_ns perms -> let ctx = mkCtxTrans (blockInputs blk) args_ns ns = RL.append (RL.append tops_ns args_ns) ghosts_ns in @@ -3740,7 +3910,7 @@ tcBlockEntryBody blk entry@(TypedEntry {..}) = pretty "Input perms:" <> align (permPretty i perms)) >>> stmtRecombinePerms >>> - tcEmitStmtSeq ctx (blk ^. blockStmts) + tcEmitStmtSeq names ctx (blk ^. blockStmts) -- | Prove that the permissions held at a call site from the given source @@ -3755,7 +3925,7 @@ proveCallSiteImpl :: ((tops :++: args) :++: vars) tops args ghosts) proveCallSiteImpl srcID destID args ghosts vars mb_perms_in mb_perms_out = - fmap CallSiteImpl $ runPermCheckM srcID args vars mb_perms_in $ + fmap CallSiteImpl $ runPermCheckM [] srcID args vars mb_perms_in $ \tops_ns args_ns _ perms_in -> let perms_out = give (cruCtxProxies ghosts) $ @@ -3825,22 +3995,23 @@ widenEntry (TypedEntry {..}) = -- 'True', recompute the entrypoint input permissions using widening visitEntry :: (PermCheckExtC ext, CtxToRList cargs ~ args, KnownRepr ExtRepr ext) => + [Maybe String] -> Bool -> Block ext cblocks ret cargs -> TypedEntry TCPhase ext blocks tops ret args ghosts -> TopPermCheckM ext cblocks blocks tops ret (Some (TypedEntry TCPhase ext blocks tops ret args)) -- If the entry is already complete, do nothing -visitEntry _ _ entry +visitEntry _ _ _ entry | isJust $ completeTypedEntry entry = trace ("visitEntry " ++ show (typedEntryID entry) ++ ": no change") $ return $ Some entry -- Otherwise, visit the call sites, widen if needed, and type-check the body -visitEntry _ _ (TypedEntry {..}) +visitEntry _ _ _ (TypedEntry {..}) | tracePretty (vsep [pretty ("visitEntry " ++ show typedEntryID ++ " with input perms:"), permPretty emptyPPInfo typedEntryPermsIn]) False = undefined -visitEntry can_widen blk entry = +visitEntry names can_widen blk entry = mapM (traverseF $ visitCallSite entry) (typedEntryCallers entry) >>= \callers -> if can_widen && any (anyF typedCallSiteImplFails) callers then @@ -3849,17 +4020,18 @@ visitEntry can_widen blk entry = -- If we widen then we are throwing away the old body, so all of its -- callees are no longer needed and can be deleted modifying stBlockMap (deleteEntryCallees $ typedEntryID entry) >> - visitEntry False blk entry' + visitEntry names False blk entry' else if isJust (typedEntryBody entry) then -- If the body was complete when we started and we are not widening, there -- is no reason to re-type-check the body, so just update the callers return $ Some $ entry { typedEntryCallers = callers } else - do body <- maybe (tcBlockEntryBody blk entry) return (typedEntryBody entry) + do body <- maybe (tcBlockEntryBody names blk entry) return (typedEntryBody entry) return $ Some $ entry { typedEntryCallers = callers, typedEntryBody = Just body } + -- | Visit a block by visiting all its entrypoints visitBlock :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => @@ -3870,7 +4042,7 @@ visitBlock blk@(TypedBlock {..}) = (stCBlocksEq <$> get) >>= \Refl -> flip (set typedBlockEntries) blk <$> mapM (\(Some entry) -> - visitEntry typedBlockCanWiden typedBlockBlock entry) _typedBlockEntries + visitEntry _typedBlockNames typedBlockCanWiden typedBlockBlock entry) _typedBlockEntries -- | Flatten a list of topological ordering components to a list of nodes in -- topological order paired with a flag denoting which nodes were loop heads diff --git a/intTests/test0069_unfinished/test.saw b/intTests/test0069_unfinished/test.saw new file mode 100644 index 0000000000..3399406c50 --- /dev/null +++ b/intTests/test0069_unfinished/test.saw @@ -0,0 +1,14 @@ +enable_experimental; + +let andI = core_axiom "(a b : Bool) -> EqTrue a -> EqTrue b -> EqTrue (and a b)"; +let script = do { simplify (cryptol_ss()); goal_apply andI; trivial; }; + +b <- fresh_symbolic "b" {| Bit |}; + +print "The following proof should fail because the proof is incomplete."; +fails (prove_print script {{ True && b }}); + +print "Now we check that the 'prove' command also does the correct thing."; +r <- prove script {{ True && b }}; +caseProofResult r (\_ -> fails (print "We should not get a theorem!")) + (\x -> do { prove_print z3 {{ x == () }}; return ();} ); diff --git a/intTests/test0069_unfinished/test.sh b/intTests/test0069_unfinished/test.sh new file mode 100644 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test0069_unfinished/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs index e6cca931a6..45f9681972 100644 --- a/src/SAWScript/Crucible/Common.hs +++ b/src/SAWScript/Crucible/Common.hs @@ -58,7 +58,7 @@ sawCoreState sym = pure (onlineUserState (W4.sbUserState sym)) ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc ann) -> AbortedResult Sym ext -> PP.Doc ann -ppAbortedResult _ (AbortedExec InfeasibleBranch _) = +ppAbortedResult _ (AbortedExec InfeasibleBranch{} _) = PP.pretty "Infeasible branch" ppAbortedResult ppGP (AbortedExec abt gp) = do PP.vcat diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index 795da169d1..6032f84365 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -59,7 +59,6 @@ import qualified Data.Map as Map import Data.Maybe (fromMaybe, isNothing) import Data.Set (Set) import qualified Data.Set as Set -import qualified Data.Sequence as Seq import Data.Text (Text) import qualified Data.Text as Text import Data.Time.Clock (getCurrentTime, diffUTCTime) @@ -132,6 +131,7 @@ import SAWScript.Crucible.JVM.Override import SAWScript.Crucible.JVM.ResolveSetupValue import SAWScript.Crucible.JVM.BuiltinsJVM () +type AssumptionReason = (W4.ProgramLoc, String) type SetupValue = MS.SetupValue CJ.JVM type Lemma = MS.ProvedSpec CJ.JVM type MethodSpec = MS.CrucibleMethodSpecIR CJ.JVM @@ -276,7 +276,7 @@ verifyObligations :: JVMCrucibleContext -> MethodSpec -> ProofScript () -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> [(String, W4.ProgramLoc, Term)] -> TopLevel (SolverStats, Set TheoremNonce) verifyObligations cc mspec tactic assumes asserts = @@ -333,7 +333,7 @@ verifyPrestate :: MethodSpec -> Crucible.SymGlobalState Sym -> IO ([(J.Type, JVMVal)], - [Crucible.LabeledPred Term Crucible.AssumptionReason], + [Crucible.LabeledPred Term AssumptionReason], Map AllocIndex JVMRefVal, Crucible.SymGlobalState Sym) verifyPrestate cc mspec globals0 = @@ -511,7 +511,7 @@ setupPrestateConditions :: JVMCrucibleContext -> Map AllocIndex JVMRefVal -> [SetupCondition] -> - IO [Crucible.LabeledPred Term Crucible.AssumptionReason] + IO [Crucible.LabeledPred Term AssumptionReason] setupPrestateConditions mspec cc env = aux [] where tyenv = MS.csAllocations mspec @@ -523,11 +523,11 @@ setupPrestateConditions mspec cc env = aux [] do val1' <- resolveSetupVal cc env tyenv nameEnv val1 val2' <- resolveSetupVal cc env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' - let lp = Crucible.LabeledPred t (Crucible.AssumptionReason loc "equality precondition") + let lp = Crucible.LabeledPred t (loc, "equality precondition") aux (lp:acc) xs aux acc (MS.SetupCond_Pred loc tm : xs) = - let lp = Crucible.LabeledPred (ttTerm tm) (Crucible.AssumptionReason loc "precondition") in + let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in aux (lp:acc) xs aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_ @@ -593,7 +593,7 @@ verifySimulate :: [Crucible.GenericExecutionFeature Sym] -> MethodSpec -> [(a, JVMVal)] -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> W4.ProgramLoc -> [Lemma] -> Crucible.SymGlobalState Sym -> @@ -630,9 +630,10 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat = mapM_ (registerOverride opts cc simctx top_loc) (groupOn (view csMethodName) (map (view MS.psSpec) lemmas)) liftIO $ putStrLn "registering assumptions" - liftIO $ do - preds <- (traverse . Crucible.labeledPred) (resolveSAWPred cc) assumes - Crucible.addAssumptions sym (Seq.fromList preds) + liftIO $ + for_ assumes $ \(Crucible.LabeledPred p (loc, reason)) -> + do expr <- resolveSAWPred cc p + Crucible.addAssumption sym (Crucible.GenericAssumption loc reason expr) liftIO $ putStrLn "simulating function" fnCall Crucible.executeCrucible (map Crucible.genericToExecutionFeature feats) @@ -731,14 +732,14 @@ verifyPoststate cc mspec env0 globals ret = obligations <- io $ Crucible.getProofObligations sym io $ Crucible.clearProofObligations sym - io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations) + io $ mapM (verifyObligation sc) (maybe [] Crucible.goalsToList obligations) where sym = cc^.jccBackend verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError loc err))) = do st <- sawCoreState sym - hypTerm <- scAndList sc =<< mapM (toSC sym st) (toListOf (folded . Crucible.labeledPred) hyps) + hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps conclTerm <- toSC sym st concl obligation <- scImplies sc hypTerm conclTerm return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, loc, obligation) diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 4d43bcc447..7e9c35f199 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -243,13 +243,15 @@ methodSpecHandler opts sc cc top_loc css h = do case res of Left (OF loc rsn) -> -- TODO, better pretty printing for reasons - liftIO $ Crucible.abortExecBecause - (Crucible.AssumedFalse (Crucible.AssumptionReason loc (show rsn))) + liftIO + $ Crucible.abortExecBecause + $ Crucible.AssertionFailure + $ Crucible.SimError loc + $ Crucible.AssertFailureSimError "assumed false" (show rsn) Right (ret,st') -> do liftIO $ forM_ (st'^.osAssumes) $ \asum -> Crucible.addAssumption (cc ^. jccBackend) - (Crucible.LabeledPred asum - (Crucible.AssumptionReason (st^.osLocation) "override postcondition")) + $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum Crucible.writeGlobals (st'^.overrideGlobals) Crucible.overrideReturn' (Crucible.RegEntry retTy ret) , Just (W4.plSourceLoc (cs ^. MS.csLoc)) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 25a76c0196..e7a33e0f30 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -198,6 +198,8 @@ import SAWScript.Crucible.LLVM.Override import SAWScript.Crucible.LLVM.ResolveSetupValue import SAWScript.Crucible.LLVM.MethodSpecIR +type AssumptionReason = (W4.ProgramLoc, String) + type MemImpl = Crucible.MemImpl Sym data LLVMVerificationException @@ -603,7 +605,7 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp = verifyObligations :: LLVMCrucibleContext arch -> MS.CrucibleMethodSpecIR (LLVM arch) -> ProofScript () - -> [Crucible.LabeledPred Term Crucible.AssumptionReason] + -> [Crucible.LabeledPred Term AssumptionReason] -> [(String, W4.ProgramLoc, Term)] -> TopLevel (SolverStats, Set TheoremNonce) verifyObligations cc mspec tactic assumes asserts = @@ -738,7 +740,7 @@ verifyPrestate :: MS.CrucibleMethodSpecIR (LLVM arch) -> Crucible.SymGlobalState Sym -> IO ([(Crucible.MemType, LLVMVal)], - [Crucible.LabeledPred Term Crucible.AssumptionReason], + [Crucible.LabeledPred Term AssumptionReason], Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)), Crucible.SymGlobalState Sym) verifyPrestate opts cc mspec globals = @@ -772,7 +774,7 @@ assumptionsContainContradiction :: (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> ProofScript () -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> TopLevel Bool assumptionsContainContradiction cc tactic assumptions = do @@ -803,7 +805,7 @@ computeMinimalContradictingCore :: (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> ProofScript () -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> TopLevel () computeMinimalContradictingCore cc tactic assumes = do @@ -814,8 +816,9 @@ computeMinimalContradictingCore cc tactic assumes = findM (assumptionsContainContradiction cc tactic) cores >>= \case Nothing -> printOutLnTop Warn "No minimal core: the assumptions did not contains a contradiction." Just core -> - forM_ core $ \ assumption -> - printOutLnTop Warn (show . Crucible.ppAssumptionReason $ assumption ^. Crucible.labeledPredMsg) + forM_ core $ \assume -> + case assume^.Crucible.labeledPredMsg of + (loc, reason) -> printOutLnTop Warn (show loc ++ ": " ++ reason) printOutLnTop Warn "Because of the contradiction, the following proofs may be vacuous." -- | Checks whether the given list of assumptions contains a contradiction, and @@ -824,7 +827,7 @@ checkAssumptionsForContradictions :: (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) => LLVMCrucibleContext arch -> ProofScript () -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> TopLevel () checkAssumptionsForContradictions cc tactic assumes = whenM @@ -953,7 +956,7 @@ setupPrestateConditions :: Map AllocIndex (LLVMPtr (Crucible.ArchWidth arch)) -> Crucible.SymGlobalState Sym -> [MS.SetupCondition (LLVM arch)] -> - IO (Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term Crucible.AssumptionReason]) + IO (Crucible.SymGlobalState Sym, [Crucible.LabeledPred Term AssumptionReason]) setupPrestateConditions mspec cc mem env = aux [] where tyenv = MS.csAllocations mspec @@ -965,11 +968,11 @@ setupPrestateConditions mspec cc mem env = aux [] do val1' <- resolveSetupVal cc mem env tyenv nameEnv val1 val2' <- resolveSetupVal cc mem env tyenv nameEnv val2 t <- assertEqualVals cc val1' val2' - let lp = Crucible.LabeledPred t (Crucible.AssumptionReason loc "equality precondition") + let lp = Crucible.LabeledPred t (loc, "equality precondition") aux (lp:acc) globals xs aux acc globals (MS.SetupCond_Pred loc tm : xs) = - let lp = Crucible.LabeledPred (ttTerm tm) (Crucible.AssumptionReason loc "precondition") in + let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in aux (lp:acc) globals xs aux acc globals (MS.SetupCond_Ghost () _loc var val : xs) = @@ -1155,7 +1158,7 @@ verifySimulate :: [Crucible.GenericExecutionFeature Sym] -> MS.CrucibleMethodSpecIR (LLVM arch) -> [(Crucible.MemType, LLVMVal)] -> - [Crucible.LabeledPred Term Crucible.AssumptionReason] -> + [Crucible.LabeledPred Term AssumptionReason] -> W4.ProgramLoc -> [MS.ProvedSpec (LLVM arch)] -> Crucible.SymGlobalState Sym -> @@ -1209,8 +1212,9 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat as do mapM_ (registerOverride opts cc simCtx top_loc) (groupOn (view csName) funcLemmas) liftIO $ - do preds <- (traverse . Crucible.labeledPred) (resolveSAWPred cc) assumes - Crucible.addAssumptions sym (Seq.fromList preds) + for_ assumes $ \(Crucible.LabeledPred p (loc, reason)) -> + do expr <- resolveSAWPred cc p + Crucible.addAssumption sym (Crucible.GenericAssumption loc reason expr) Crucible.regValue <$> (Crucible.callBlock cfg entryId args') res <- Crucible.executeCrucible execFeatures initExecState case res of @@ -1302,7 +1306,7 @@ verifyPoststate cc mspec env0 globals ret = obligations <- io $ Crucible.getProofObligations sym io $ Crucible.clearProofObligations sym - sc_obligations <- io $ mapM (verifyObligation sc) (Crucible.proofGoalsToList obligations) + sc_obligations <- io $ mapM (verifyObligation sc) (maybe [] Crucible.goalsToList obligations) return (sc_obligations, st) where @@ -1310,7 +1314,7 @@ verifyPoststate cc mspec env0 globals ret = verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err@(Crucible.SimError loc _))) = do st <- Common.sawCoreState sym - hypTerm <- toSC sym st =<< W4.andAllOf sym (folded . Crucible.labeledPred) hyps + hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps conclTerm <- toSC sym st concl obligation <- scImplies sc hypTerm conclTerm return (unlines ["safety assertion:", show err], loc, obligation) diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 39a9924072..826f1d0f4d 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -475,13 +475,15 @@ methodSpecHandler opts sc cc top_loc css h = do case res of Left (OF loc rsn) -> -- TODO, better pretty printing for reasons - liftIO $ Crucible.abortExecBecause - (Crucible.AssumedFalse (Crucible.AssumptionReason loc (show rsn))) + liftIO + $ Crucible.abortExecBecause + $ Crucible.AssertionFailure + $ Crucible.SimError loc + $ Crucible.AssertFailureSimError "assumed false" (show rsn) Right (ret,st') -> do liftIO $ forM_ (st'^.osAssumes) $ \asum -> Crucible.addAssumption (cc^.ccBackend) - (Crucible.LabeledPred asum - (Crucible.AssumptionReason (st^.osLocation) "override postcondition")) + $ Crucible.GenericAssumption (st^.osLocation) "override postcondition" asum Crucible.writeGlobals (st'^.overrideGlobals) Crucible.overrideReturn' (Crucible.RegEntry retTy ret) , Just (W4.plSourceLoc (cs ^. MS.csLoc)) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 43f48450c2..88dbcfff99 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -914,8 +914,8 @@ assertPost globals env premem preregs = do st <- case result of Left err -> throwX86 $ show err Right (_, st) -> pure st - liftIO . forM_ (view O.osAssumes st) $ \p -> - C.addAssumption sym . C.LabeledPred p $ C.AssumptionReason (st ^. O.osLocation) "precondition" + liftIO . forM_ (view O.osAssumes st) $ + C.addAssumption sym . C.GenericAssumption (st ^. O.osLocation) "precondition" liftIO . forM_ (view LO.osAsserts st) $ \(W4.LabeledPred p r) -> C.addAssertion sym $ C.LabeledPred p r diff --git a/src/SAWScript/HeapsterBuiltins.hs b/src/SAWScript/HeapsterBuiltins.hs index ff2491c915..1900049dd8 100644 --- a/src/SAWScript/HeapsterBuiltins.hs +++ b/src/SAWScript/HeapsterBuiltins.hs @@ -40,6 +40,7 @@ module SAWScript.HeapsterBuiltins , heapster_find_trait_method_symbol , heapster_assume_fun , heapster_assume_fun_rename + , heapster_assume_fun_rename_prim , heapster_assume_fun_multi , heapster_print_fun_trans , heapster_export_coq @@ -869,6 +870,53 @@ heapster_assume_fun_rename _bic _opts henv nm nm_to perms_string term_string = (globalOpenTerm term_ident) liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'' +-- | Create a new SAW core primitive named @nm@ with type @tp@ in the module +-- associated with the supplied Heapster environment, and return its identifier +insPrimitive :: HeapsterEnv -> String -> Term -> TopLevel Ident +insPrimitive henv nm tp = + do sc <- getSharedContext + let mnm = heapsterEnvSAWModule henv + let ident = mkSafeIdent mnm nm + i <- liftIO $ scFreshGlobalVar sc + liftIO $ scRegisterName sc i (ModuleIdentifier ident) + let pn = PrimName i ident tp + t <- liftIO $ scFlatTermF sc (Primitive pn) + liftIO $ scRegisterGlobal sc ident t + liftIO $ scModifyModule sc mnm $ \m -> + insDef m $ Def { defIdent = ident, + defQualifier = PrimQualifier, + defType = tp, + defBody = Nothing } + return ident + +-- | Assume that the given named function has the supplied type and translates +-- to a SAW core definition given by the second name +heapster_assume_fun_rename_prim :: BuiltinContext -> Options -> HeapsterEnv -> + String -> String -> String -> TopLevel () +heapster_assume_fun_rename_prim _bic _opts henv nm nm_to perms_string = + do Some lm <- failOnNothing ("Could not find symbol: " ++ nm) + (lookupModContainingSym henv nm) + sc <- getSharedContext + let w = llvmModuleArchReprWidth lm + leq_proof <- case decideLeq (knownNat @1) w of + Left pf -> return pf + Right _ -> fail "LLVM arch width is 0!" + env <- liftIO $ readIORef $ heapsterEnvPermEnvRef henv + (Some cargs, Some ret) <- lookupFunctionType lm nm + let args = mkCruCtx cargs + withKnownNat w $ withLeqProof leq_proof $ do + SomeFunPerm fun_perm <- + parseFunPermStringMaybeRust "permissions" w env args ret perms_string + env' <- liftIO $ readIORef (heapsterEnvPermEnvRef henv) + fun_typ <- liftIO $ translateCompleteFunPerm sc env fun_perm + term_ident <- insPrimitive henv nm_to fun_typ + let env'' = permEnvAddGlobalSymFun env' + (GlobalSymbol $ fromString nm) + w + fun_perm + (globalOpenTerm term_ident) + liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'' + -- | Assume that the given named function has the supplied type and translates -- to a SAW core definition given by name heapster_assume_fun :: BuiltinContext -> Options -> HeapsterEnv -> diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index fc2b49e190..aa0b8de25d 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -3187,6 +3187,15 @@ primitives = Map.fromList , " trans is not an identifier then it is bound to the defined name nm_to." ] + , prim "heapster_assume_fun_rename_prim" + "HeapsterEnv -> String -> String -> String -> TopLevel HeapsterEnv" + (bicVal heapster_assume_fun_rename_prim) + Experimental + [ + "heapster_assume_fun_rename_prim nm nm_to perms assumes that function nm" + , " has permissions perms as a primitive." + ] + , prim "heapster_assume_fun_multi" "HeapsterEnv -> String -> [(String, String)] -> TopLevel HeapsterEnv" (bicVal heapster_assume_fun_multi) diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index 384d75b38f..01b143ff21 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -27,7 +27,7 @@ module SAWScript.X86 ) where -import Control.Lens (toListOf, folded, (^.)) +import Control.Lens ((^.)) import Control.Exception(Exception(..),throwIO) import Control.Monad.IO.Class(liftIO) @@ -72,7 +72,8 @@ import Lang.Crucible.Simulator.ExecutionTree ) import Lang.Crucible.Simulator.SimError(SimError(..), SimErrorReason) import Lang.Crucible.Backend - (getProofObligations,ProofGoal(..),labeledPredMsg,labeledPred,proofGoalsToList) + (getProofObligations,ProofGoal(..),labeledPredMsg,labeledPred,goalsToList + ,assumptionsPred) import Lang.Crucible.FunctionHandle(HandleAllocator,newHandleAllocator,insertHandleMap,emptyHandleMap) @@ -564,15 +565,15 @@ gGoal sc g0 = boolToProp sc [] =<< go (gAssumes g) getGoals :: Sym -> IO [Goal] getGoals sym = - do obls <- proofGoalsToList <$> getProofObligations sym + do obls <- maybe [] goalsToList <$> getProofObligations sym st <- sawCoreState sym mapM (toGoal st) obls where toGoal st (ProofGoal asmps g) = - do as <- mapM (toSC sym st) (toListOf (folded . labeledPred) asmps) + do a1 <- toSC sym st =<< assumptionsPred sym asmps p <- toSC sym st (g ^. labeledPred) let SimError loc msg = g^.labeledPredMsg - return Goal { gAssumes = as + return Goal { gAssumes = [a1] , gShows = p , gLoc = loc , gMessage = msg diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index 1c53e145d8..05ff826a3e 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -103,9 +103,9 @@ import qualified Lang.Crucible.LLVM.MemModel as Crucible import Lang.Crucible.Simulator.SimError(SimErrorReason(AssertFailureSimError)) import Lang.Crucible.Backend - (addAssumption, getProofObligations, proofGoalsToList - ,assert, AssumptionReason(..) - ,LabeledPred(..), ProofGoal(..), labeledPredMsg) + (addAssumption, getProofObligations, goalsToList + ,assert, CrucibleAssumption(..) + ,ProofGoal(..), labeledPredMsg) import Lang.Crucible.Simulator.ExecutionTree import Lang.Crucible.Simulator.OverrideSim @@ -826,7 +826,8 @@ makeEquiv opts s (Pair (Rep t _) (Equiv xs ys)) = let same a = do p <- evalSame sym t v a let loc = mkProgramLoc "" InternalPos - addAssumption sym (LabeledPred p (AssumptionReason loc "equivalance class assumption")) + addAssumption sym + $ GenericAssumption loc "equivalance class assumption" p mapM_ same rest @@ -847,7 +848,7 @@ addAsmp opts s (msg,p) = _ -> do p' <- evalProp opts p s let loc = mkProgramLoc "" InternalPos -- FIXME - addAssumption (optsSym opts) (LabeledPred p' (AssumptionReason loc msg)) + addAssumption (optsSym opts) (GenericAssumption loc msg p') setCryPost :: forall p. (Eval p, Crucible.HasLLVMAnn Sym) => Opts -> S p -> (String,Prop p) -> IO (S p) setCryPost opts s (_nm,p) = @@ -1132,7 +1133,7 @@ debugPPReg r s = _debugDumpGoals :: Sym -> IO () _debugDumpGoals sym = - do obls <- proofGoalsToList <$> getProofObligations sym + do obls <- maybe [] goalsToList <$> getProofObligations sym mapM_ sh (toList obls) where sh (ProofGoal _hyps g) = print (view labeledPredMsg g) diff --git a/vim-saw/doc/saw.txt b/vim-saw/doc/saw.txt new file mode 100644 index 0000000000..820f6291e5 --- /dev/null +++ b/vim-saw/doc/saw.txt @@ -0,0 +1,10 @@ +*saw.txt* functionality for developing sawscript scripts + +This plugin adds basic syntax highlighting and a vim-slime override. This +allows using vim-slime to send sawscript snippets from a sawscript file to a +running sawscript interpreter. See the official vim-slime documentation for how +to use vim-slime. The most basic command is , which sends the whole +paragraph the cursor is in. Note that the saw interpreter will correctly parse +single top-level statements, but not multpile top-level statements. + +Dependencies: vim-slime diff --git a/vim-saw/ftdetect/saw.vim b/vim-saw/ftdetect/saw.vim new file mode 100644 index 0000000000..121b01ba77 --- /dev/null +++ b/vim-saw/ftdetect/saw.vim @@ -0,0 +1 @@ +autocmd BufNewFile,BufRead *.saw set filetype=saw diff --git a/vim-saw/plugin/saw.vim b/vim-saw/plugin/saw.vim new file mode 100644 index 0000000000..75b6225b63 --- /dev/null +++ b/vim-saw/plugin/saw.vim @@ -0,0 +1,18 @@ +" a function that overrides vim-slime's default behavior: +function SlimeOverride_EscapeText_saw(text) + " create temp buffer + split __saw_slime_temp_buffer__ + setlocal buftype=nofile + " paste text in buffer + set paste + exe "normal! i" . a:text . "\" + set nopaste + " remove blank things: + silent! keepp g/^\s*\n/d + silent! keepp g/^\n/d + silent! keepp g/^\s*\/\/.*\n/d + silent! keepp %s/\/\/.*$//eg " remove end-of-line comments + let res = join(getline(1, '$'), "\\\n") " copy buffer contents into res, adding a backslash at the end of each line + bdelete __saw_slime_temp_buffer__ " delete temp buffer (the following didn't work reliably: setlocal bufhidden=delete) + return res . "\n" +endfunction diff --git a/vim-saw/syntax/saw.vim b/vim-saw/syntax/saw.vim new file mode 100644 index 0000000000..98455932ec --- /dev/null +++ b/vim-saw/syntax/saw.vim @@ -0,0 +1,10 @@ +hi link SAWKeyword Keyword +setlocal commentstring=//%s " is this useless? the doc says only used for folding +setlocal comments=s1:/*,mb:*,ex:*/,://" +syntax match SAWComment "\v//.*$" contains=@Spell +syntax region SAWComment start="/\*" end="\*/" contains=@Spell +highlight link SAWComment Comment +setlocal formatoptions=tcqr + +" all SAW builtins included: +syn keyword SAWKeyword do let import abc get_opt offline_cnf abstract_symbolic goal_apply offline_cnf_external add_cryptol_defs goal_assume offline_coq add_cryptol_eqs goal_eval offline_extcore add_prelude_defs goal_eval_unint offline_smtlib2 add_prelude_eqs goal_insert offline_unint_smtlib2 add_x86_preserved_reg goal_intro offline_verilog addsimp goal_num_ite offline_w4_unint_cvc4 addsimp' goal_num_when offline_w4_unint_yices addsimps goal_when offline_w4_unint_z3 addsimps' head parse_core admit hoist_ifs parser_printer_roundtrip approxmc include print assume_unsat java_array print_goal assume_valid java_bool print_goal_consts auto_match java_byte print_goal_depth basic_ss java_char print_goal_size beta_reduce_goal java_class print_term beta_reduce_term java_double print_term_depth boolector java_float print_type caseProofResult java_int prove caseSatResult java_load_class prove_core check_convertible java_long prove_print check_goal java_short qc_print check_term jvm_alloc_array quickcheck codegen jvm_alloc_object read_aig concat jvm_array_is read_bytes core_axiom jvm_elem_is read_core core_thm jvm_execute_func replace crucible_alloc jvm_extract return crucible_alloc_aligned jvm_field_is rewrite crucible_alloc_global jvm_fresh_var rme crucible_alloc_readonly jvm_modifies_elem run crucible_alloc_readonly_aligned jvm_modifies_field sat crucible_alloc_with_size jvm_modifies_static_field sat_print crucible_array jvm_null sbv_abc crucible_conditional_points_to jvm_postcond sbv_boolector crucible_conditional_points_to_untyped jvm_precond sbv_cvc4 crucible_declare_ghost_state jvm_return sbv_mathsat crucible_elem jvm_static_field_is sbv_unint_cvc4 crucible_equal jvm_term sbv_unint_yices crucible_execute_func jvm_unsafe_assume_spec sbv_unint_z3 crucible_field jvm_verify sbv_yices crucible_fresh_cryptol_var lambda sbv_z3 crucible_fresh_expanded_val lambdas set_ascii crucible_fresh_pointer length set_base crucible_fresh_var list_term set_color crucible_ghost_value llvm_alias set_timeout crucible_global llvm_alloc set_x86_stack_base_align crucible_global_initializer llvm_alloc_aligned sharpSAT crucible_java_extract llvm_alloc_global show crucible_llvm_array_size_profile llvm_alloc_readonly show_cfg crucible_llvm_compositional_extract llvm_alloc_readonly_aligned show_term crucible_llvm_extract llvm_alloc_with_size simplify crucible_llvm_unsafe_assume_spec llvm_array skeleton_arg crucible_llvm_verify llvm_array_size_profile skeleton_arg_index crucible_llvm_verify_x86 llvm_array_value skeleton_arg_index_pointer crucible_null llvm_boilerplate skeleton_arg_pointer crucible_packed_struct llvm_cfg skeleton_exec crucible_points_to llvm_compositional_extract skeleton_globals_post crucible_points_to_array_prefix llvm_conditional_points_to skeleton_globals_pre crucible_points_to_untyped llvm_conditional_points_to_at_type skeleton_guess_arg_sizes crucible_postcond llvm_conditional_points_to_untyped skeleton_poststate crucible_precond llvm_declare_ghost_state skeleton_prestate crucible_return llvm_double skeleton_resize_arg crucible_spec_size llvm_elem skeleton_resize_arg_index crucible_spec_solvers llvm_equal split_goal crucible_struct llvm_execute_func str_concat crucible_symbolic_alloc llvm_extract summarize_verification crucible_term llvm_field tail cryptol_add_path llvm_float term_size cryptol_extract llvm_fresh_cryptol_var term_tree_size cryptol_load llvm_fresh_expanded_val test_mr_solver cryptol_prims llvm_fresh_pointer time cryptol_ss llvm_fresh_var trivial cvc4 llvm_ghost_value true default_x86_preserved_reg llvm_global type default_x86_stack_base_align llvm_global_initializer undefined define llvm_int unfold_term disable_crucible_assert_then_assume llvm_load_module unfolding disable_crucible_profiling llvm_null unint_cvc4 disable_smt_array_memory_model llvm_packed_struct_type unint_yices disable_what4_hash_consing llvm_packed_struct_value unint_z3 disable_x86_what4_hash_consing llvm_pointer w4 dsec_print llvm_points_to w4_abc_smtlib2 dump_file_AST llvm_points_to_array_prefix w4_abc_verilog empty_ss llvm_points_to_at_type w4_offline_smtlib2 enable_crucible_assert_then_assume llvm_points_to_untyped w4_unint_cvc4 enable_crucible_profiling llvm_postcond w4_unint_yices enable_deprecated llvm_precond w4_unint_z3 enable_experimental llvm_return with_time enable_lax_arithmetic llvm_sizeof write_aig enable_smt_array_memory_model llvm_spec_size write_aig_external enable_what4_hash_consing llvm_spec_solvers write_cnf enable_x86_what4_hash_consing llvm_struct write_cnf_external env llvm_struct_type write_coq_cryptol_module eval_bool llvm_struct_value write_coq_cryptol_primitives_for_sawcore eval_int llvm_symbolic_alloc write_coq_sawcore_prelude eval_list llvm_term write_coq_term eval_size llvm_type write_core exec llvm_unsafe_assume_spec write_saig exit llvm_verify write_saig' external_aig_solver llvm_verify_x86 write_smtlib2 external_cnf_solver mathsat write_smtlib2_w4 fails module_skeleton write_verilog false nth yices for null z3 fresh_symbolic offline_aig function_skeleton offline_aig_external