From 50ddf87306912422192c10eefec732c4aeaf350b Mon Sep 17 00:00:00 2001 From: Alexander Bakst Date: Fri, 29 Apr 2022 10:15:22 -0700 Subject: [PATCH 1/8] Eliminate field-shaped blocks in the array prover. --- heapster-saw/src/Verifier/SAW/Heapster/Implication.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index d1608cef1a..c8d07edea6 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -6689,6 +6689,15 @@ proveVarLLVMArrayH x p psubst ps mb_ap | PExpr_ArrayShape {} <- llvmBlockShape bp = True arrayBlock _ = False +proveVarLLVMArrayH x p psubst ps mb_ap + | Just i <- findIndex seqFieldBlock ps = + implElimAppendIthLLVMBlock x ps i >>>= \ps' -> + proveVarLLVMArrayH x p psubst ps' mb_ap + where + seqFieldBlock (Perm_LLVMBlock bp) + | Just flds <- matchLLVMFieldShapeSeq (llvmBlockShape bp) = length flds > 1 + seqFieldBlock _ = False + -- Otherwise, try and build a completely borrowed array that references existing -- permissions that cover the range of mb_ap, and recurse (hitting the special -- case above). From 147d85c0e7e4d1f63b2ae871c1cb1985567cec9f Mon Sep 17 00:00:00 2001 From: Alexander Bakst Date: Fri, 29 Apr 2022 10:21:36 -0700 Subject: [PATCH 2/8] Add test for blocks with sequence of field shapes --- heapster-saw/proverTests/Main.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/heapster-saw/proverTests/Main.hs b/heapster-saw/proverTests/Main.hs index bf7bccfbda..4ef68f2678 100644 --- a/heapster-saw/proverTests/Main.hs +++ b/heapster-saw/proverTests/Main.hs @@ -138,6 +138,16 @@ int64ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 8 (fieldShape (intVal int32ArrayPerm :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> LLVMArrayPerm 64 int32ArrayPerm off len = arrayPerm (toIdx off) (toIdx len) 4 (fieldShape (intValuePerm @32)) +charShape :: PermExpr (LLVMShapeType 64) +charShape = fieldShape (intValuePerm @8) + +charArray :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> AtomicPerm (LLVMPointerType 64) +charArray off len = Perm_LLVMArray (arrayPerm (toIdx off) (toIdx len) 1 (fieldShape (intValuePerm @8))) + +strBlock :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> AtomicPerm (LLVMPointerType 64) +strBlock off len = Perm_LLVMBlock $ + memblockPerm off len (PExpr_SeqShape charShape (PExpr_SeqShape charShape charShape)) + arrayPerm :: PermExpr (BVType w) -> PermExpr (BVType w) -> @@ -178,6 +188,7 @@ arrayTests = [ int64field 0, int64field 8, int64field 16 ] ===> int64array 8 3 , testCase "insufficient fields (2)" $ fails $ [ int64field 0, int64field 8, int64field 16 ] ===> int64array 0 4 + , testCase "string" $ passes $ strBlock 0 6 ===> charArray 0 6 ] , testGroup "mix of permission types" From 9220cecb9a467fbe45cc9efa500777b2899f0b3b Mon Sep 17 00:00:00 2001 From: Alexander Bakst Date: Fri, 29 Apr 2022 16:36:06 -0700 Subject: [PATCH 3/8] Fix broken testcase --- heapster-saw/proverTests/Main.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/heapster-saw/proverTests/Main.hs b/heapster-saw/proverTests/Main.hs index 4ef68f2678..3f000087ba 100644 --- a/heapster-saw/proverTests/Main.hs +++ b/heapster-saw/proverTests/Main.hs @@ -144,9 +144,9 @@ charShape = fieldShape (intValuePerm @8) charArray :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> AtomicPerm (LLVMPointerType 64) charArray off len = Perm_LLVMArray (arrayPerm (toIdx off) (toIdx len) 1 (fieldShape (intValuePerm @8))) -strBlock :: (ArrayIndexExpr a1, ArrayIndexExpr a2) => a1 -> a2 -> AtomicPerm (LLVMPointerType 64) -strBlock off len = Perm_LLVMBlock $ - memblockPerm off len (PExpr_SeqShape charShape (PExpr_SeqShape charShape charShape)) +str3Block :: (ArrayIndexExpr a) => a -> AtomicPerm (LLVMPointerType 64) +str3Block off = Perm_LLVMBlock $ + memblockPerm off 3 (PExpr_SeqShape charShape (PExpr_SeqShape charShape charShape)) arrayPerm :: PermExpr (BVType w) -> @@ -188,7 +188,7 @@ arrayTests = [ int64field 0, int64field 8, int64field 16 ] ===> int64array 8 3 , testCase "insufficient fields (2)" $ fails $ [ int64field 0, int64field 8, int64field 16 ] ===> int64array 0 4 - , testCase "string" $ passes $ strBlock 0 6 ===> charArray 0 6 + , testCase "string" $ passes $ str3Block 0 ===> charArray 0 3 ] , testGroup "mix of permission types" From 12e1d87954fb32130e766d7b29cb3390d06507a4 Mon Sep 17 00:00:00 2001 From: Alexander Bakst Date: Fri, 29 Apr 2022 13:44:11 -0700 Subject: [PATCH 4/8] Try solving for array lifetime/rw modality. --- .../src/Verifier/SAW/Heapster/Implication.hs | 42 +++++++++++++++++++ .../src/Verifier/SAW/Heapster/Permissions.hs | 7 ++++ 2 files changed, 49 insertions(+) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index c8d07edea6..acdb6a9df6 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -6606,6 +6606,42 @@ borrowedLLVMArrayForArray lhs rhs = | otherwise = bs_skip ++ bs_lhs +-- | TODO: hide the bool parameter +solveForArray :: + (1 <= w, KnownNat w, NuMatchingAny1 r) => + Bool -> + [AtomicPerm (LLVMPointerType w)] -> + Mb vars (LLVMArrayPerm w) -> + ImplM vars s r ps ps () +solveForArray should_fail ps mb_ap = + getPSubst >>>= \psubst -> + case partialSubst psubst mb_ap of + Just _ap -> return () + Nothing + | should_fail -> + implFailM "goo goo" + | otherwise -> + solveForArrayH ps psubst mb_ap + +solveForArrayH :: + (1 <= w, KnownNat w, NuMatchingAny1 r) => + [AtomicPerm (LLVMPointerType w)] -> + PartialSubst vars -> + Mb vars (LLVMArrayPerm w) -> + ImplM vars s r ps ps () +solveForArrayH ps psubst mb_ap + | Nothing <- partialSubst psubst $ mbLLVMArrayLifetime mb_ap + , Just l:_ <- atomicPermLifetime <$> ps = + tryUnifyVars l (mbLLVMArrayLifetime mb_ap) >>> + solveForArray False ps mb_ap +solveForArrayH ps psubst mb_ap + | Nothing <- partialSubst psubst $ mbLLVMArrayRW mb_ap + , Just l:_ <- atomicPermModality <$> ps = + tryUnifyVars l (mbLLVMArrayRW mb_ap) >>> + solveForArray False ps mb_ap +solveForArrayH ps _ mb_ap = + solveForArray True ps mb_ap + -- | Prove an LLVM array permission @ap@ from permissions @x:(p1 * ... *pn)@ on -- the top of the stack, ensuring that any remaining permissions for @x@ get @@ -6701,6 +6737,12 @@ proveVarLLVMArrayH x p psubst ps mb_ap -- Otherwise, try and build a completely borrowed array that references existing -- permissions that cover the range of mb_ap, and recurse (hitting the special -- case above). +proveVarLLVMArrayH x first_p psubst ps mb_ap + | Nothing <- partialSubst psubst mb_ap = + solveForArray False ps mb_ap >>> + getPSubst >>>= \psubst' -> + proveVarLLVMArrayH x first_p psubst' ps mb_ap + proveVarLLVMArrayH x first_p psubst ps mb_ap | Just ap <- partialSubst psubst mb_ap -- NOTE: borrowedLLVMArrayForArray only returns a single possible covering, though diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index c60bb5cfdb..f4af7ac63a 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -4058,6 +4058,13 @@ atomicPermLifetime (Perm_LLVMArray ap) = Just $ llvmArrayLifetime ap atomicPermLifetime (Perm_LLVMBlock bp) = Just $ llvmBlockLifetime bp atomicPermLifetime _ = Nothing +-- | Get the modality of an atomic perm if it is a field, array, or memblock +atomicPermModality :: AtomicPerm a -> Maybe (PermExpr RWModalityType) +atomicPermModality (Perm_LLVMField fp) = Just $ llvmFieldRW fp +atomicPermModality (Perm_LLVMArray ap) = Just $ llvmArrayRW ap +atomicPermModality (Perm_LLVMBlock bp) = Just $ llvmBlockRW bp +atomicPermModality _ = Nothing + -- | Get the starting offset of an atomic permission, if it has one. This -- includes array permissions which may have some cells borrowed. llvmAtomicPermOffset :: AtomicPerm (LLVMPointerType w) -> From 92b699af851e411490ca56ced65703c32a14e692 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 2 May 2022 11:50:53 -0700 Subject: [PATCH 5/8] updated the translation of LLVM global constants to not use the "show" method to convert symbol names to strings --- heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index 32f121c673..8b63988c41 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -243,9 +243,9 @@ permEnvAddGlobalConst sc mod_name dlevel endianness w env global = case translateLLVMValueTop dlevel endianness w env global of Nothing -> return env Just (sh, t) -> - do ident <- - scFreshenGlobalIdent sc $ - mkSafeIdent mod_name $ show $ L.globalSym global + do let (L.Symbol glob_str) = L.globalSym global + ident <- + scFreshenGlobalIdent sc $ mkSafeIdent mod_name $ show glob_str complete_t <- completeOpenTerm sc t tp <- completeOpenTermType sc t scInsertDef sc mod_name ident tp complete_t From fa82780fe0a7f3c0a020f430de1ece7800602b32 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 2 May 2022 12:58:05 -0700 Subject: [PATCH 6/8] fixed a type error message, which was saying "not a sort" when it was supposed to say "not a tuple" --- saw-core/src/Verifier/SAW/SCTypeCheck.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/saw-core/src/Verifier/SAW/SCTypeCheck.hs b/saw-core/src/Verifier/SAW/SCTypeCheck.hs index 9d41822947..9d94d5eef2 100644 --- a/saw-core/src/Verifier/SAW/SCTypeCheck.hs +++ b/saw-core/src/Verifier/SAW/SCTypeCheck.hs @@ -584,7 +584,7 @@ ensureSort tp = ensureRecognizer asSort (NotSort tp) tp -- | Ensure a 'Term' is a pair type, normalizing if necessary, and return the -- two components of that pair type ensurePairType :: Term -> TCM (Term, Term) -ensurePairType tp = ensureRecognizer asPairType (NotSort tp) tp +ensurePairType tp = ensureRecognizer asPairType (NotTupleType tp) tp -- | Ensure a 'Term' is a record type, normalizing if necessary, and return the -- components of that record type From 5f6f718040a0e10280af568a18b4e4f0f3db2464 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 2 May 2022 12:58:44 -0700 Subject: [PATCH 7/8] fixed translateLLVMValue on string values, which was somehow giving an incorrect translation; also fixed up the comments on translateLLVMValue to help clarify what it is supposed to return --- heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs index 8b63988c41..7a37b3d2b5 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs @@ -83,7 +83,8 @@ ppLLVMConstExpr :: L.ConstExpr -> String ppLLVMConstExpr ce = L.withConfig (L.Config True True True) (show $ PPHPJ.nest 2 $ L.ppConstExpr ce) --- | Translate a typed LLVM 'L.Value' to a Heapster permission + translation +-- | Translate a typed LLVM 'L.Value' to a Heapster shape + an element of the +-- translation of that shape to a SAW core type translateLLVMValue :: (1 <= w, KnownNat w) => NatRepr w -> L.Type -> L.Value -> LLVMTransM (PermExpr (LLVMShapeType w), OpenTerm) translateLLVMValue w tp@(L.PrimType (L.Integer n)) (L.ValInteger i) = @@ -124,7 +125,8 @@ translateLLVMValue _ _ (L.ValString bytes) = foldr1 PExpr_SeqShape $ map (PExpr_FieldShape . LLVMFieldShape . ValPerm_Eq . PExpr_LLVMWord . bvBV . BV.word8) bytes in - return (sh, unitOpenTerm) + let tm = foldr1 pairOpenTerm $ map (const unitOpenTerm) bytes in + return (sh, tm) -- NOTE: we don't translate strings to one big bitvector value because that -- seems to mess up the endianness {- From ba63344c1dc61ff160bdc997b5b401a3ab1445ee Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Mon, 2 May 2022 14:20:03 -0700 Subject: [PATCH 8/8] bug fix: changed implLLVMArrayBorrowed to check for the block permission used by the rule having the same shape as the array permission cell; changed the call to this rule in proveLLVMArray to ensure this property holds --- .../src/Verifier/SAW/Heapster/Implication.hs | 51 ++++++++++--------- 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index 529ea7faee..bcdf68f388 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -773,15 +773,15 @@ data SimplImpl ps_in ps_out where ExprVar (LLVMPointerType w) -> LLVMArrayPerm w -> SimplImpl RNil (RNil :> LLVMPointerType w) - -- | Prove an array whose borrows @bs@ cover the entire array. - -- The input memblock is proof that @x@ is a pointer, and can be located - -- anywhere as long as it has the same shape as the output array. - -- - -- NOTE: the block permission is used by the SAW translation to produce - -- the default cell value for the translation of the output array. + -- | Prove an array whose borrows @bs@ cover the entire array using a + -- permission that instantiates at least one of its cells. This latter + -- permission ensures that the @x@ is a pointer, and is also used in the + -- translation to give a default value to the cells of the output array + -- permission: -- - -- > x:[l2]memblock(rw,off1, -o x:[2]memblock(rw,off1, x:[l2]memblock(rw,off1, -o x:[2]memblock(rw,off1, * x:[l]array(rw,off, ExprVar (LLVMPointerType w) -> @@ -1979,15 +1979,11 @@ simplImplIn (SImpl_LLVMArrayToField x ap _) = simplImplIn (SImpl_LLVMArrayEmpty _ ap) = if bvIsZero (llvmArrayLen ap) then DistPermsNil else error "simplImplIn: SImpl_LLVMArrayEmpty: malformed empty array permission" - simplImplIn (SImpl_LLVMArrayBorrowed x bp ap) = - if bvIsZero (llvmArrayLen ap) then - error "simplImplIn: SImpl_LLVMArrayBorrowed: empty array permission" - else if not (llvmArrayIsBorrowed ap) then - error "simplImplIn: SImpl_LLVMArrayBorrowed: array permission not completely borrowed" - else + if llvmArrayIsBorrowed ap && llvmBlockShape bp == llvmArrayCellShape ap then distPerms1 x (ValPerm_Conj1 $ Perm_LLVMBlock bp) - + else + error "simplImplIn: SImpl_LLVMArrayBorrowed: array permission not completely borrowed or of the wrong shape" simplImplIn (SImpl_LLVMArrayFromBlock x bp) = distPerms1 x $ ValPerm_LLVMBlock bp @@ -5157,11 +5153,14 @@ implLLVMArrayEmpty :: ImplM vars s r (ps :> LLVMPointerType w) ps () implLLVMArrayEmpty x ap = implSimplM Proxy (SImpl_LLVMArrayEmpty x ap) +-- | Prove an array permission whose borrows cover the array using a permission +-- that instantiates at least one of its cells implLLVMArrayBorrowed :: (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) -> LLVMBlockPerm w -> LLVMArrayPerm w -> ImplM vars s r (ps :> LLVMPointerType w :> LLVMPointerType w) (ps :> LLVMPointerType w) () -implLLVMArrayBorrowed x blk ap = implSimplM Proxy (SImpl_LLVMArrayBorrowed x blk ap) +implLLVMArrayBorrowed x blk ap = + implSimplM Proxy (SImpl_LLVMArrayBorrowed x blk ap) -- | Prove the @memblock@ permission returned by @'llvmAtomicPermToBlock' p@ -- from a proof of @p@ on top of the stack, assuming it returned one @@ -6597,9 +6596,10 @@ proveVarLLVMFieldH2 x p _ mb_fp = ---------------------------------------------------------------------- -- | Search for a permission that _could_ prove a block at an offset in the --- given range. +-- given range findSomeBlock :: forall w. (1 <= w, KnownNat w) => - [AtomicPerm (LLVMPointerType w)] -> BVRange w -> Maybe (LLVMBlockPerm w) + [AtomicPerm (LLVMPointerType w)] -> BVRange w -> + Maybe (LLVMBlockPerm w) findSomeBlock ps range = msum (couldProve <$> ps) where couldProve :: AtomicPerm (LLVMPointerType w) -> Maybe (LLVMBlockPerm w) @@ -6849,13 +6849,14 @@ proveVarLLVMArrayH x first_p psubst ps mb_ap -- there may be multiple. It may be necessary to modify this to return a list, but -- we'd like to avoid the blowup in branches (see `borrowedLLVMArrayForArray`) , Just (ps', borrowed) <- borrowedLLVMArrayForArray ps ap - , Just bp <- findSomeBlock ps' (llvmArrayAbsOffsets ap) = - mbVarsM bp >>>= \mb_bp -> - proveVarLLVMBlock x ps mb_bp >>> - implLLVMArrayBorrowed x bp borrowed >>> - recombinePerm x (ValPerm_Conj1 (Perm_LLVMBlock bp)) >>> - -- The recursive call should now hit the case above - proveVarLLVMArrayH x first_p psubst [Perm_LLVMArray borrowed] mb_ap + , Just bp_lhs <- findSomeBlock ps' (llvmArrayAbsOffsets ap) = + let bp = bp_lhs { llvmBlockShape = llvmArrayCellShape ap } in + mbVarsM bp >>>= \mb_bp -> + proveVarLLVMBlock x ps mb_bp >>> + implLLVMArrayBorrowed x bp borrowed >>> + recombinePerm x (ValPerm_Conj1 (Perm_LLVMBlock bp)) >>> + -- The recursive call should now hit the case above + proveVarLLVMArrayH x first_p psubst [Perm_LLVMArray borrowed] mb_ap proveVarLLVMArrayH x _ _ ps mb_ap = -- TODO: Review this note?