diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index 9e95350f94..d6a096ec1c 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -1817,7 +1817,7 @@ lookupEntryTrans entryID blkMap = maybe (error "lookupEntryTrans") id $ find (\(Some entryTrans) -> entryID == typedEntryID (typedEntryTransEntry entryTrans)) $ - typedBlockTransEntries (RL.get (entryBlockID entryID) blkMap) + typedBlockTransEntries (RL.get (entryBlockMember entryID) blkMap) -- | Look up the translation of an entry by entry ID and make sure that it has -- the supplied ghost arguments diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index cd4b589cb5..b92b9ace50 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -220,9 +220,28 @@ typedFnHandleRetType (TypedFnHandle _ h) = handleReturnType h -- | As in standard Crucible, blocks are identified by membership proofs that --- their input arguments are in the @blocks@ list -type TypedBlockID (a :: RList (RList CrucibleType)) = - Member a -- :: (b :: RList CrucibleType) -> Type +-- their input arguments are in the @blocks@ list. We also track an 'Int' that +-- gives the 'indexVal' of the original Crucible block ID, so that typed block +-- IDs can be printed the same way as standard Crucible block IDs. The issue +-- here is that 'Member' proofs count from the right of an 'RList', while +-- Crucible uses membership proofs that count from the left, and so the sizes +-- are not the same. +data TypedBlockID (ctx :: RList (RList CrucibleType)) args = + TypedBlockID { typedBlockIDMember :: Member ctx args, typedBlockIDIx :: Int } + deriving Eq + +instance TestEquality (TypedBlockID ctx) where + testEquality (TypedBlockID memb1 _) (TypedBlockID memb2 _) = + testEquality memb1 memb2 + +instance Show (TypedBlockID ctx args) where + show tblkID = "%" ++ show (typedBlockIDIx tblkID) + +-- | Convert a Crucible 'Index' to a 'TypedBlockID' +indexToTypedBlockID :: Size ctx -> Index ctx args -> + TypedBlockID (CtxCtxToRList ctx) (CtxToRList args) +indexToTypedBlockID sz ix = + TypedBlockID (indexCtxToMember sz ix) (Ctx.indexVal ix) -- | All of our blocks have multiple entry points, for different inferred types, -- so a "typed" 'BlockID' is a normal Crucible 'BlockID' (which is just an index @@ -232,19 +251,17 @@ data TypedEntryID (blocks :: RList (RList CrucibleType)) (args :: RList Crucible TypedEntryID { entryBlockID :: TypedBlockID blocks args, entryIndex :: Int } deriving Eq --- | Compute the length of a 'Member' proof, which corresponds to its deBruijn --- index, i.e., number of hops from the right -memberLength :: Member a as -> Int -memberLength Member_Base = 0 -memberLength (Member_Step memb) = 1 + memberLength memb +-- | Get the 'Member' proof of the 'TypedBlockID' of a 'TypedEntryID' +entryBlockMember :: TypedEntryID blocks args -> Member blocks args +entryBlockMember = typedBlockIDMember . entryBlockID -- | Compute the indices corresponding to the 'BlockID' and 'entryIndex' of a -- 'TypedEntryID', for printing purposes entryIDIndices :: TypedEntryID blocks args -> (Int, Int) -entryIDIndices (TypedEntryID memb ix) = (memberLength memb, ix) +entryIDIndices (TypedEntryID tblkID ix) = (typedBlockIDIx tblkID, ix) instance Show (TypedEntryID blocks args) where - show entryID = "" + show (TypedEntryID {..}) = show entryBlockID ++ "(" ++ show entryIndex ++ ")" instance TestEquality (TypedEntryID blocks) where testEquality (TypedEntryID memb1 i1) (TypedEntryID memb2 i2) @@ -312,6 +329,7 @@ instance NuMatchingAny1 RegWithVal where $(mkNuMatching [t| forall ext tp. NuMatchingExtC ext => TypedExpr ext tp |]) $(mkNuMatching [t| forall ghosts args ret. TypedFnHandle ghosts args ret |]) +$(mkNuMatching [t| forall blocks args. TypedBlockID blocks args |]) $(mkNuMatching [t| forall blocks args. TypedEntryID blocks args |]) $(mkNuMatching [t| forall blocks args ghosts. TypedCallSiteID blocks args ghosts |]) $(mkNuMatching [t| forall blocks tops ps_in. TypedJumpTarget blocks tops ps_in |]) @@ -319,9 +337,20 @@ $(mkNuMatching [t| forall blocks tops ps_in. TypedJumpTarget blocks tops ps_in | instance NuMatchingAny1 (TypedJumpTarget blocks tops) where nuMatchingAny1Proof = nuMatchingProof +instance NuMatchingAny1 (TypedBlockID blocks) where + nuMatchingAny1Proof = nuMatchingProof + instance NuMatchingAny1 (TypedEntryID blocks) where nuMatchingAny1Proof = nuMatchingProof +instance Closable (TypedBlockID blocks args) where + toClosed (TypedBlockID memb ix) = + $(mkClosed [| TypedBlockID |]) + `clApply` toClosed memb `clApply` toClosed ix + +instance Liftable (TypedBlockID blocks args) where + mbLift = unClosed . mbLift . fmap toClosed + instance Closable (TypedEntryID blocks args) where toClosed (TypedEntryID entryBlockID entryIndex) = $(mkClosed [| TypedEntryID |]) @@ -1323,7 +1352,7 @@ emptyBlockOfSort :: cblocks) tops ret (CtxToRList cargs) emptyBlockOfSort names cblocks sort blk | Refl <- reprReprToCruCtxCtxEq cblocks - = TypedBlock (indexCtxToMember (size cblocks) $ + = TypedBlock (indexToTypedBlockID (size cblocks) $ blockIDIndex $ blockID blk) blk sort True [] names -- | Build a block with a user-supplied input permission @@ -1338,7 +1367,7 @@ emptyBlockForPerms :: 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 + , blockID <- indexToTypedBlockID (size cblocks) $ blockIDIndex $ blockID blk , args <- mkCruCtx (blockInputs blk) = TypedBlock blockID blk JoinSort False [Some TypedEntry { @@ -1459,7 +1488,7 @@ type TypedBlockMap phase ext blocks tops ret = instance Show (TypedEntry phase ext blocks tops ret args ghosts) where show (TypedEntry { .. }) = - "" + "" instance Show (TypedBlock phase ext blocks tops ret args) where show = concatMap (\(Some entry) -> show entry) . (^. typedBlockEntries) @@ -1478,7 +1507,9 @@ blockByID :: TypedBlockID blocks args -> Lens' (TypedBlockMap phase ext blocks tops ret) (TypedBlock phase ext blocks tops ret args) -blockByID blkID = lens (RL.get blkID) (flip $ RL.set blkID) +blockByID blkID = + let memb = typedBlockIDMember blkID in + lens (RL.get memb) (flip $ RL.set memb) -- | Look up a 'TypedEntry' by its 'TypedEntryID' lookupEntry :: TypedEntryID blocks args -> @@ -1512,12 +1543,12 @@ deleteEntryCallees topEntryID = execState (deleteCallees topEntryID) where deleteCallees callerID = get >>= \blkMap -> mapM_ (\(Some calleeID) -> - deleteCaller callerID calleeID) (entryCallees callerID blkMap) + deleteCall callerID calleeID) (entryCallees callerID blkMap) -- Delete call sites of a caller to a particular callee - deleteCaller :: TypedEntryID blocks args1 -> TypedEntryID blocks args2 -> - State (TypedBlockMap phase ext blocks tops ret) () - deleteCaller callerID calleeID = + deleteCall :: TypedEntryID blocks args1 -> TypedEntryID blocks args2 -> + State (TypedBlockMap phase ext blocks tops ret) () + deleteCall callerID calleeID = (typedBlockSort <$> use (blockByID $ entryBlockID calleeID)) >>= \case JoinSort -> -- The target has JoinSort, so we want to keep the callee entrypoint. Thus @@ -1526,7 +1557,7 @@ deleteEntryCallees topEntryID = execState (deleteCallees topEntryID) where . entryByID calleeID) $ \(Some callee) -> let callers' = flip filter (typedEntryCallers callee) $ \(Some site) -> - callSiteIDCallerEq callerID $ typedCallSiteID site in + not $ callSiteIDCallerEq callerID $ typedCallSiteID site in Some $ callee { typedEntryCallers = callers' } MultiEntrySort -> -- The target has MultiEntrySort, so callerID is the only caller to this @@ -1641,19 +1672,13 @@ addCtxName ctx x = extend ctx (TypedReg x) -- | The translation of a Crucible block id newtype BlockIDTrans blocks args = - BlockIDTrans { unBlockIDTrans :: Member blocks (CtxToRList args) } - -extendBlockIDTrans :: BlockIDTrans blocks args -> - BlockIDTrans (blocks :> tp) args -extendBlockIDTrans (BlockIDTrans memb) = BlockIDTrans $ Member_Step memb + BlockIDTrans { unBlockIDTrans :: TypedBlockID blocks (CtxToRList args) } -- | Build a map from Crucible block IDs to 'Member' proofs -buildBlockIDMap :: Assignment f cblocks -> +buildBlockIDMap :: Size cblocks -> Assignment (BlockIDTrans (CtxCtxToRList cblocks)) cblocks -buildBlockIDMap (viewAssign -> AssignEmpty) = Ctx.empty -buildBlockIDMap (viewAssign -> AssignExtend asgn _) = - Ctx.extend (fmapFC extendBlockIDTrans $ buildBlockIDMap asgn) - (BlockIDTrans Member_Base) +buildBlockIDMap sz = + Ctx.generate sz $ \ix -> BlockIDTrans (indexToTypedBlockID sz ix) data SomePtrWidth where SomePtrWidth :: HasPtrWidth w => SomePtrWidth @@ -1707,7 +1732,7 @@ emptyTopPermCheckState env fun_perm endianness cfg sccs = { stTopCtx = funPermTops fun_perm , stRetType = funPermRet fun_perm , stRetPerms = funPermOuts fun_perm - , stBlockTrans = buildBlockIDMap blkMap + , stBlockTrans = buildBlockIDMap (Ctx.size blkMap) , _stBlockMap = initTypedBlockMap env fun_perm cfg sccs , stPermEnv = env , stBlockTypes = fmapFC blockInputs blkMap @@ -1762,7 +1787,7 @@ applyTypedBlockMapDelta :: TypedBlockMapDelta blocks tops ret -> TopPermCheckState ext cblocks blocks tops ret -> TopPermCheckState ext cblocks blocks tops ret applyTypedBlockMapDelta (TypedBlockMapAddCallSite siteID perms_in) top_st = - over (stBlockMap . member (entryBlockID $ callSiteDest siteID)) + over (stBlockMap . member (entryBlockMember $ callSiteDest siteID)) (blockAddCallSite siteID (stTopCtx top_st) (stRetType top_st) perms_in (stRetPerms top_st)) top_st @@ -1997,7 +2022,7 @@ callBlockWithPerms :: TypedEntryID blocks args_src -> InnerPermCheckM ext cblocks blocks tops ret (TypedCallSiteID blocks args vars) callBlockWithPerms srcEntryID destID vars cl_perms_in = - do blk <- view (stBlockMap . member destID) <$> ask + do blk <- view (stBlockMap . member (typedBlockIDMember destID)) <$> ask let siteID = newCallSiteID srcEntryID vars blk innerEmitDelta ($(mkClosed [| TypedBlockMapAddCallSite |]) `clApply` toClosed siteID `clApply` cl_perms_in) @@ -3989,6 +4014,7 @@ widenEntry :: PermCheckExtC ext => TypedEntry TCPhase ext blocks tops ret args ghosts -> Some (TypedEntry TCPhase ext blocks tops ret args) widenEntry (TypedEntry {..}) = + trace ("Widening entrypoint: " ++ show typedEntryID) $ case foldl1' (widen typedEntryTops typedEntryArgs) $ map (fmapF typedCallSiteArgVarPerms) typedEntryCallers of Some (ArgVarPerms ghosts perms_in) -> @@ -4004,7 +4030,7 @@ widenEntry (TypedEntry {..}) = -- with those input permissions, if it has not been type-checked already. -- -- If any of the call site implications fail, and the input "can widen" flag is --- 'True', recompute the entrypoint input permissions using widening +-- 'True', recompute the entrypoint input permissions using widening. visitEntry :: (PermCheckExtC ext, CtxToRList cargs ~ args, KnownRepr ExtRepr ext) => [Maybe String] -> @@ -4047,14 +4073,17 @@ visitEntry names can_widen blk entry = -- | Visit a block by visiting all its entrypoints visitBlock :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => + Bool -> {- ^ Whether widening can be applied in type-checking this block -} TypedBlock TCPhase ext blocks tops ret args -> TopPermCheckM ext cblocks blocks tops ret (TypedBlock TCPhase ext blocks tops ret args) -visitBlock blk@(TypedBlock {..}) = +visitBlock can_widen blk@(TypedBlock {..}) = (stCBlocksEq <$> get) >>= \Refl -> flip (set typedBlockEntries) blk <$> mapM (\(Some entry) -> - visitEntry _typedBlockNames typedBlockCanWiden typedBlockBlock entry) _typedBlockEntries + visitEntry _typedBlockNames (can_widen && 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 @@ -4076,6 +4105,11 @@ cfgOrderWithSCCs cfg = (fmapFC (const $ Constant False) $ cfgBlockMap cfg) nodes_sccs) +-- | The maximum number of iterations through the CFG while we allow widening +-- when type-checking before we give up and force everything to be done +maxWideningIters :: Int +maxWideningIters = 5 + -- | Type-check a Crucible CFG tcCFG :: forall w ext cblocks ghosts inits ret. @@ -4092,23 +4126,32 @@ tcCFG w env endianness fun_perm cfg = init_st = let ?ptrWidth = w in emptyTopPermCheckState env fun_perm endianness cfg sccs tp_nodes = map (\(Some blkID) -> Some $ stLookupBlockID blkID init_st) nodes in - let tp_blk_map = flip evalState init_st $ main_loop tp_nodes in + let tp_blk_map = + flip evalState init_st $ main_loop maxWideningIters tp_nodes in TypedCFG { tpcfgHandle = TypedFnHandle ghosts h , tpcfgFunPerm = fun_perm , tpcfgBlockMap = tp_blk_map , tpcfgEntryID = TypedEntryID (stLookupBlockID (cfgEntryBlockID cfg) init_st) 0 } where - main_loop :: [Some (TypedBlockID blocks :: RList CrucibleType -> Type)] -> + main_loop :: Int -> + [Some (TypedBlockID blocks :: RList CrucibleType -> Type)] -> TopPermCheckM ext cblocks blocks tops ret (TypedBlockMap TransPhase ext blocks tops ret) - main_loop nodes = + main_loop rem_iters _ + -- We may have to iterate through the CFG twice with widening turned off + -- to finally get everything to quiesce, once to ensure all block bodies + -- have type-checked and once again to ensure any back edged produced in + -- that last iteration have completed + | rem_iters < -2 = error "tcCFG: failed to complete on last iteration" + main_loop rem_iters nodes = get >>= \st -> case completeTypedBlockMap $ view stBlockMap st of Just blkMapOut -> return blkMapOut Nothing -> forM_ nodes (\(Some tpBlkID) -> - use (stBlockMap . member tpBlkID) >>= - (visitBlock >=> - assign (stBlockMap . member tpBlkID))) >> - main_loop nodes + let memb = typedBlockIDMember tpBlkID in + use (stBlockMap . member memb) >>= + (visitBlock (rem_iters > 0) >=> + assign (stBlockMap . member memb))) >> + main_loop (rem_iters - 1) nodes