From d089eed97f06903e5366748b05a651a7572a7dfe Mon Sep 17 00:00:00 2001 From: Chris Phifer Date: Tue, 20 Jul 2021 15:37:13 -0500 Subject: [PATCH 1/4] Implement a command to introduce new SAWCore primitives via Heapster --- src/SAWScript/HeapsterBuiltins.hs | 48 +++++++++++++++++++++++++++++++ src/SAWScript/Interpreter.hs | 9 ++++++ 2 files changed, 57 insertions(+) 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) From 4785a08a3caa0ebe61eb86e7066454c99a6ed19f Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Tue, 20 Jul 2021 17:32:12 -0700 Subject: [PATCH 2/4] did some work to improve the implication prover for opaque named shapes, including: modalizeShape for opaque named shapes is now a no-op; and proveVarLLVMBlock now eliminates a perm on the LHS when it cannot find a match to prove opaque named shapes on the right --- .../src/Verifier/SAW/Heapster/Implication.hs | 39 ++++++++++++++++--- .../src/Verifier/SAW/Heapster/Permissions.hs | 5 +++ 2 files changed, 39 insertions(+), 5 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index 457aa272bb..d78da02448 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -3929,7 +3929,8 @@ implIntroLLVMBlockNamed _ _ = error "implIntroLLVMBlockNamed: malformed permission" -- | Eliminate a @memblock@ permission on the top of the stack, if possible, --- otherwise fail +-- otherwise fail. The elimination does not have to completely remove any +-- @memblock@ permission, it just needs to make some sort of progress. implElimLLVMBlock :: (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) -> LLVMBlockPerm w -> ImplM vars s r (ps :> LLVMPointerType w) @@ -3953,16 +3954,22 @@ implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape = implElimLLVMBlock x (bp { llvmBlockShape = sh' }) implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape = PExpr_EqShape (PExpr_Var y) }) = - -- For shape eqsh(y), prove y:block(sh) for some sh, apply + -- For shape eqsh(y), prove y:block(sh) for some sh, and apply -- SImpl_IntroLLVMBlockFromEq, and then recursively eliminate the resulting - -- memblock permission + -- memblock permission, unless the resulting shape cannot be eliminated, in + -- which case we have still made progress so we can just stop mbVarsM () >>>= \mb_unit -> withExtVarsM (proveVarImplInt y $ mbCombine RL.typeCtxProxies $ flip fmap mb_unit $ const $ nu $ \sh -> ValPerm_Conj1 $ Perm_LLVMBlockShape $ PExpr_Var sh) >>>= \(_, sh) -> let bp' = bp { llvmBlockShape = sh } in implSimplM Proxy (SImpl_IntroLLVMBlockFromEq x bp' y) >>> - implElimLLVMBlock x bp' + case sh of + PExpr_NamedShape _ _ nmsh _ + | not (namedShapeCanUnfold nmsh) -> + -- Opaque shapes cannot be further eliminated, so stop + return () + _ -> implElimLLVMBlock x bp' implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape = PExpr_PtrShape maybe_rw maybe_l sh }) | Just len <- llvmShapeLength sh = @@ -5375,7 +5382,8 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of implSwapInsertConjM x (Perm_LLVMBlock bp_out) ps'' 0 - -- If proving a named shape, prove its unfolding first and then fold it + -- If proving an unfoldable named shape, prove its unfolding first and then + -- fold it [nuMP| mb_bp : mb_bps |] | [nuMP| PExpr_NamedShape rw l nmsh args |] <- mbMatch $ fmap llvmBlockShape mb_bp , [nuMP| TrueRepr |] <- mbMatch $ fmap namedShapeCanUnfoldRepr nmsh @@ -5402,6 +5410,27 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of implSwapInsertConjM x (Perm_LLVMBlock bp') ps_out' 0 + -- If proving an opaque named shape, the only way to prove the memblock + -- permission is to have it on the left, but we don't have a memblock + -- permission on the left with this exactly offset, length, and shape, because + -- it would have matched some previous case, so try to eliminate a memblock + -- and recurse + [nuMP| mb_bp : mb_bps |] + | [nuMP| PExpr_NamedShape _ _ nmsh _ |] <- mbMatch $ fmap llvmBlockShape mb_bp + , [nuMP| FalseRepr |] <- mbMatch $ fmap namedShapeCanUnfoldRepr nmsh + , Just off <- partialSubst psubst $ fmap llvmBlockOffset mb_bp + , Just i <- findIndex (\case + p@(Perm_LLVMBlock _) -> + isJust (llvmPermContainsOffset off p) + _ -> False) ps + , Perm_LLVMBlock bp <- ps!!i -> + implGetPopConjM x ps i >>> implElimPopLLVMBlock x bp >>> + proveVarImplInt x (fmap ValPerm_Conj $ + mbMap2 (++) + (fmap (map Perm_LLVMBlock) $ mbMap2 (:) mb_bp mb_bps) + mb_ps) + + -- If proving an equality shape eqsh(z) for evar z which has already been set, -- substitute for z and recurse [nuMP| mb_bp : mb_bps |] diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 19d7652461..5a43e27973 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -3368,6 +3368,11 @@ modalizeShape _ _ (PExpr_Var _) = -- adding a modalized variable shape constructor Nothing modalizeShape _ _ PExpr_EmptyShape = Just PExpr_EmptyShape +modalizeShape _ _ sh@(PExpr_NamedShape _ _ nmsh _) + | not (namedShapeCanUnfold nmsh) = + -- Opaque shapes are not affected by modalization, because we assume they do + -- not have any top-level pointers in them + Just sh modalizeShape rw l (PExpr_NamedShape rw' l' nmsh args) = -- If a named shape already has modalities, they take precedence Just $ PExpr_NamedShape (rw' <|> rw) (l' <|> l) nmsh args From d2f14cb66a329c5dfdfe0bddaa9ba7c07cae5ee2 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 22 Jul 2021 06:31:34 -0700 Subject: [PATCH 3/4] generated Coq file changed a bit --- heapster-saw/examples/string_set.v | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/heapster-saw/examples/string_set.v b/heapster-saw/examples/string_set.v index 49b0ee4f60..a1f7650c6e 100644 --- a/heapster-saw/examples/string_set.v +++ b/heapster-saw/examples/string_set.v @@ -42,23 +42,24 @@ Definition string_set_remove : forall (p0 : string_set), forall (p1 : string), C @listRemoveM (@SAWCoreScaffolding.String) (@SAWCoreScaffolding.equalString). Definition insert_remove__tuple_fun : @CompM.lrtTupleType (@CompM.LRT_Cons (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit)))))) (@CompM.LRT_Nil)) := - @CompM.multiFixM (@CompM.LRT_Cons (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit)))))) (@CompM.LRT_Nil)) (fun (insert_remove : @CompM.lrtToType (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit))))))) => pair (fun (p0 : string_set) (p1 : string) (p2 : string) => @CompM.letRecM (@CompM.LRT_Nil) (prod string_set (prod string unit)) tt (@errorM CompM _ (prod string_set (prod string unit)) "At string_set.c:15:3 ($14 = call $13($10, $11);) - Regs: $13 = x22, $10 = x19, $11 = x20 + @CompM.multiFixM (@CompM.LRT_Cons (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit)))))) (@CompM.LRT_Nil)) (fun (insert_remove : @CompM.lrtToType (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit))))))) => pair (fun (p0 : string_set) (p1 : string) (p2 : string) => @CompM.letRecM (@CompM.LRT_Nil) (prod string_set (prod string unit)) tt (@errorM CompM _ (prod string_set (prod string unit)) "At string_set.c:15:3 ($17 = call $16($13, $14);) + Regs: $16 = x25 @ , $13 = x22 @ , $14 = x23 @ Input perms: top1:true, top2:string_set, top3:string<>, - top4:string<>, ghost8:llvmframe [x12:8, x11:8, x10:8], - x22:(ghost26:lifetime). - ghost26:true, arg25:string_set, arg24:string<> + top4:string<>, ghost8:llvmframe [C[&str2]12:8, C[&str1]11:8, + C[&set]10:8], + x25:(ghost29:lifetime). + ghost29:true, arg28:string_set, arg27:string<> -o - ghost26:true, arg25:string_set, arg24:true, - ret23:true, x19:eq(top2), x20:eq(top3), x10:ptr((W,0) |-> - eq(x19)), - x11:ptr((W,0) |-> eq(x20)), x12:ptr((W,0) |-> eq(local7)), - local7:eq(top4) + ghost29:true, arg28:string_set, arg27:true, + ret26:true, x22:eq(top2), x23:eq(top3), + C[&set]10:ptr((W,0) |-> eq(x22)), C[&str1]11:ptr((W,0) |-> + eq(x23)), + C[&str2]12:ptr((W,0) |-> eq(local7)), local7:eq(top4) Could not prove - (z23). z23:true, x19:string_set, x20:string<> + (z26). z26:true, x22:string_set, x23:string<> Could not determine enough variables to prove permissions: - (z23). z23:true, x19:string_set"%string)) tt). + (z26). z26:true, x22:string_set"%string)) tt). Definition insert_remove : @CompM.lrtToType (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit)))))) := SAWCoreScaffolding.fst insert_remove__tuple_fun. From 2aa97b40c812ccf5f4310352eff23235a0b8a2a7 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 22 Jul 2021 11:22:52 -0700 Subject: [PATCH 4/4] small fix to comment --- heapster-saw/src/Verifier/SAW/Heapster/Implication.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index d78da02448..d648b68b75 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -5412,7 +5412,7 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of -- If proving an opaque named shape, the only way to prove the memblock -- permission is to have it on the left, but we don't have a memblock - -- permission on the left with this exactly offset, length, and shape, because + -- permission on the left with this exact offset, length, and shape, because -- it would have matched some previous case, so try to eliminate a memblock -- and recurse [nuMP| mb_bp : mb_bps |]