Heapster: duplicate read memblocks

heapster-saw/examples/rust_data.rs

@@ -12,6 +12,17 @@ pub fn bool_and_pair (xy:(bool,bool)) -> bool {
     xy.0 & xy.1
 }
 
+/* Read two integers from references and return their sum */
+pub fn ref_sum <'a,'b> (x:&'a u64, y:&'a u64) -> u64 {
+    return *x + *y;
+}
+
+/* Double the integer pointed to by a reference by duplicating the reference and
+ * passing it to ref_sum */
+pub fn double_dup_ref <'a> (x:&'a u64) -> u64 {
+    return ref_sum (x, x);
+}
+
 #[repr(C)]
 pub struct BoolStruct { fst_bool:bool,snd_bool:bool }
 

heapster-saw/examples/rust_data.saw

@@ -221,6 +221,17 @@ heapster_assume_fun_rename env exchange_malloc_sym "exchange_malloc"
               \ ret:memblock(W,0,len,emptysh)"
   "\\ (len:Vec 64 Bool) -> returnM #() ()";
 
+// llvm.uadd.with.overflow.i64
+heapster_assume_fun env "llvm.uadd.with.overflow.i64"
+  "(). arg0:int64<>, arg1:int64<> -o ret:struct(int64<>,int1<>)"
+  "\\ (x y:Vec 64 Bool) -> \
+    \ returnM (Vec 64 Bool * Vec 1 Bool) (bvAdd 64 x y, single Bool (bvCarry 64 x y))";
+
+// llvm.expect.i1
+heapster_assume_fun env "llvm.expect.i1"
+  "().arg0:int1<>, arg1:int1<> -o ret:int1<>" "\\ (x y:Vec 1 Bool) -> returnM (Vec 1 Bool) x";
+
+
 // memcpy
 heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64"
   "(rw:rwmodality, l1:lifetime, l2:lifetime, sh:llvmshape 64, \
@@ -395,6 +406,16 @@ mk_two_values_sym <- heapster_find_symbol env "13mk_two_values";
 heapster_typecheck_fun_rename env mk_two_values_sym "mk_two_values" "<> fn (u32,u32) -> TwoValues";
 */
 
+// ref_sum
+ref_sum_sym <- heapster_find_symbol env "7ref_sum";
+heapster_typecheck_fun_rename env ref_sum_sym "ref_sum"
+  "<'a,'b> fn (x:&'a u64, y:&'a u64) -> u64";
+
+// double_dup_ref
+double_dup_ref_sym <- heapster_find_symbol env "14double_dup_ref";
+heapster_typecheck_fun_rename env double_dup_ref_sym "double_dup_ref"
+  "<'a,'b> fn (x:&'a u64) -> u64";
+
 // test_result
 test_result_sym <- heapster_find_symbol env "11test_result";
 heapster_typecheck_fun_rename env test_result_sym "test_result"

heapster-saw/src/Verifier/SAW/Heapster/Implication.hs

@@ -3920,9 +3920,36 @@ implEndLifetimeM ps l ps_in ps_out@(lownedPermsToDistPerms -> Just dps_out)
   | isJust (lownedPermsToDistPerms ps_in) =
     implSimplM ps (SImpl_EndLifetime l ps_in ps_out) >>>
     implTraceM (\i -> pretty "Ending lifetime:" <+> permPretty i l) >>>
+    implDropLifetimePermsM l >>>
     recombinePermsPartial ps (DistPermsCons dps_out l ValPerm_LFinished)
 implEndLifetimeM _ _ _ _ = implFailM "implEndLifetimeM: lownedPermsToDistPerms"
 
+-- | Drop any permissions of the form @x:[l]p@ in the primary permissions for
+-- @x@, which are supplied as an argument
+implDropLifetimeConjsM :: NuMatchingAny1 r => ExprVar LifetimeType ->
+                          ExprVar a -> [AtomicPerm a] ->
+                          ImplM vars s r ps ps ()
+implDropLifetimeConjsM l x ps
+  | Just i <- findIndex (\p -> atomicPermLifetime p == Just (PExpr_Var l)) ps =
+    implPushM x (ValPerm_Conj ps) >>>
+    implExtractSwapConjM x ps i >>>
+    implDropM x (ValPerm_Conj1 (ps!!i)) >>>
+    let ps' = deleteNth i ps in
+    implPopM x (ValPerm_Conj ps') >>>
+    implDropLifetimeConjsM l x ps'
+implDropLifetimeConjsM _ _ _ = return ()
+
+-- | Find all primary permissions of the form @x:[l]p@ and drop them, assuming
+-- that we have just ended lifetime @l@
+implDropLifetimePermsM :: NuMatchingAny1 r => ExprVar LifetimeType ->
+                          ImplM vars s r ps ps ()
+implDropLifetimePermsM l =
+  (NameMap.assocs <$> view varPermMap <$> getPerms) >>>= \vars_and_perms ->
+  forM_ vars_and_perms $ \case
+  NameAndElem x (ValPerm_Conj ps) ->
+    implDropLifetimeConjsM l x ps
+  _ -> return ()
+
 -- | Save a permission for later by splitting it into part that is in the
 -- current lifetime and part that is saved in the lifetime for later. Assume
 -- permissions
@@ -3941,6 +3968,7 @@ implSplitLifetimeM :: (KnownRepr TypeRepr a, NuMatchingAny1 r) =>
 implSplitLifetimeM x f args l l2 sub_ls ps_in ps_out =
   implTraceM (\i ->
                sep [pretty "Splitting lifetime to" <+> permPretty i l2 <> colon,
+                    permPretty i x <> colon <>
                     permPretty i (ltFuncMinApply f l)]) >>>
   implSimplM Proxy (SImpl_SplitLifetime x f args l l2 sub_ls ps_in ps_out) >>>
   getTopDistPerm l2 >>>= implPopM l2
@@ -4758,8 +4786,8 @@ recombinePerm' x x_p@(ValPerm_Exists _) p =
 recombinePerm' x (ValPerm_Conj x_ps) (ValPerm_Conj (p:ps)) =
   implExtractConjM x (p:ps) 0 >>>
   implSwapM x (ValPerm_Conj1 p) x (ValPerm_Conj ps) >>>
-  recombinePermConj x x_ps p >>>= \x_ps' ->
-  recombinePermExpl x (ValPerm_Conj x_ps') (ValPerm_Conj ps)
+  recombinePermConj x x_ps p >>>
+  recombinePerm x (ValPerm_Conj ps)
 recombinePerm' x x_p (ValPerm_Named npn args off)
   | TrueRepr <- nameIsConjRepr npn =
     implNamedToConjM x npn args off >>>
@@ -4770,7 +4798,7 @@ recombinePerm' x _ p = implDropM x p
 -- conjuctive permission @x_p1 * ... * x_pn@ for @x@, returning the resulting
 -- permission conjucts for @x@
 recombinePermConj :: NuMatchingAny1 r => ExprVar a -> [AtomicPerm a] ->
-                     AtomicPerm a -> ImplM vars s r as (as :> a) [AtomicPerm a]
+                     AtomicPerm a -> ImplM vars s r as (as :> a) ()
 
 -- If p is a field read permission that is already in x_ps, drop it
 recombinePermConj x x_ps p@(Perm_LLVMField fp)
@@ -4780,8 +4808,7 @@ recombinePermConj x x_ps p@(Perm_LLVMField fp)
                   _ -> False) x_ps
   , PExpr_Read <- llvmFieldRW fp
   , PExpr_Read <- llvmFieldRW fp' =
-    implDropM x (ValPerm_Conj1 p) >>>
-    pure x_ps
+    implDropM x (ValPerm_Conj1 p)
 
 -- If p is an array read permission whose offsets match an existing array
 -- permission, drop it
@@ -4792,41 +4819,17 @@ recombinePermConj x x_ps p@(Perm_LLVMArray ap)
                     bvEq (llvmArrayLen ap') (llvmArrayLen ap)
                   _ -> False) x_ps
   , PExpr_Read <- llvmArrayRW ap =
-    implDropM x (ValPerm_Conj1 p) >>>
-    pure x_ps
-
+    implDropM x (ValPerm_Conj1 p)
 
 -- If p is an is_llvmptr permission and x_ps already contains one, drop it
 recombinePermConj x x_ps p@Perm_IsLLVMPtr
   | elem Perm_IsLLVMPtr x_ps =
-    implDropM x (ValPerm_Conj1 p) >>>
-    pure x_ps
+    implDropM x (ValPerm_Conj1 p)
 
--- NOTE: the following is old, but it would never match anyway, because if we
+-- NOTE: we do not return a field that was borrowed from an array, because if we
 -- have a field (or block) that was borrowed from an array, it almost certainly
--- was borrowed because we accessed it, so it will contain eq permissions and
--- its shape will not equal that of the array it was borrowed from
-{-
--- If p is a field that was borrowed from an array, return it; i.e., if we are
--- returning x:ptr((rw,off+i*stride+j) |-> p) and x has a permission of the form
--- x:array(off,<len,*stride,fps,(i*stride+j):bs) where the jth element of fps
--- equals ptr((rw,j) |-> p), then remove (i*stride+j) from bs
-recombinePermConj x x_ps (Perm_LLVMField fp)
-  | (ap,i,ix):_ <-
-      flip mapMaybe (zip x_ps [0::Int ..]) $
-      \case (Perm_LLVMArray ap, i)
-              | Just ix <- matchLLVMArrayField ap (llvmFieldOffset fp)
-              , elem (FieldBorrow ix) (llvmArrayBorrows ap) ->
-                Just (ap,i,ix)
-            _ -> Nothing
-  , LLVMArrayField fp == llvmArrayFieldWithOffset ap ix =
-    implPushM x (ValPerm_Conj x_ps) >>> implExtractConjM x x_ps i >>>
-    let x_ps' = deleteNth i x_ps in
-    implPopM x (ValPerm_Conj x_ps') >>>
-    implLLVMArrayIndexReturn x ap ix >>>
-    recombinePermConj x x_ps' (Perm_LLVMArray $
-                               llvmArrayRemBorrow (FieldBorrow ix) ap)
--}
+-- was borrowed because we accessed it, so it will contain eq permissions, which
+-- make it a stronger permission than the cell permission in the array
 
 -- If p is an array that was borrowed from some other array, return it
 recombinePermConj x x_ps (Perm_LLVMArray ap)
@@ -4845,12 +4848,29 @@ recombinePermConj x x_ps (Perm_LLVMArray ap)
     implLLVMArrayReturn x ap_bigger ap >>>= \ap_bigger' ->
     recombinePermConj x x_ps' (Perm_LLVMArray ap_bigger')
 
+-- If p is a memblock permission whose range is a subset of that of a permission
+-- we already hold, drop it
+recombinePermConj x x_ps (Perm_LLVMBlock bp)
+  | any (llvmAtomicPermContainsRange $ llvmBlockRange bp) x_ps =
+    implDropM x $ ValPerm_LLVMBlock bp
+
+-- If p is a memblock permission whose range overlaps with but is not wholly
+-- contained in a permission we already hold, eliminate it and recombine
+--
+-- FIXME: if the elimination fails, this shouldn't fail, it should just
+-- recombine without eliminating, so we should special case those shapes where
+-- the elimination will fail
+recombinePermConj x x_ps (Perm_LLVMBlock bp)
+  | any (llvmAtomicPermOverlapsRange $ llvmBlockRange bp) x_ps =
+    implElimLLVMBlock x bp >>>
+    getTopDistPerm x >>>= \p ->
+    recombinePerm x p
+
 -- Default case: insert p at the end of the x_ps
 recombinePermConj x x_ps p =
   implPushM x (ValPerm_Conj x_ps) >>>
   implInsertConjM x p x_ps (length x_ps) >>>
-  implPopM x (ValPerm_Conj (x_ps ++ [p])) >>>
-  pure (x_ps ++ [p])
+  implPopM x (ValPerm_Conj (x_ps ++ [p]))
 
 
 -- | Recombine the permissions on the stack back into the permission set
@@ -5958,10 +5978,8 @@ proveVarLLVMBlock x ps mb_bp =
   do psubst <- getPSubst
      proveVarLLVMBlocks x ps psubst [mb_bp]
 
--- | Prove a conjunction of block and atomic permissions for @x@, assuming all
--- of the permissions for @x@ are on the top of the stack and given by the
--- second argument. The block permissions are the ones that we are currently
--- working on, and when they are all proved we bottom out to 'proveVarConjImpl'.
+-- | Prove a conjunction of block and atomic permissions for @x@ from the
+-- permissions on top of the stack, which are given by the second argument.
 --
 -- A central motivation of this algorithm is to do as little elimination on the
 -- left or introduction on the right as possible, in order to build the smallest
@@ -6056,7 +6074,7 @@ proveVarLLVMBlocks1 ::
 
 -- We are done, yay! Pop ps and build a true permission
 proveVarLLVMBlocks1 x ps _ [] =
-  implPopM x (ValPerm_Conj ps) >>> introConjM x
+  recombinePerm x (ValPerm_Conj ps) >>> introConjM x
 
 -- If the offset, length, and shape of the top block matches one that we already
 -- have, just cast the rwmodality and lifetime and prove the remaining perms
@@ -6079,6 +6097,12 @@ proveVarLLVMBlocks1 x ps psubst (mb_bp:mb_bps)
     -- Make the input block have the required modalities
     equalizeBlockModalities x bp mb_bp >>>= \bp' ->
 
+    -- Duplicate and save the block permission if it is copyable
+    (if atomicPermIsCopyable (Perm_LLVMBlock bp') then
+       implCopyM x (ValPerm_LLVMBlock bp') >>>
+       recombinePerm x (ValPerm_LLVMBlock bp')
+     else return ()) >>>
+
     -- Move it down below ps'
     implSwapM x (ValPerm_Conj ps') x (ValPerm_LLVMBlock bp') >>>
 

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

@@ -1874,7 +1874,7 @@ data LLVMArrayBorrow w
     -- ^ Borrow a specific cell of an array permission
   | RangeBorrow (BVRange w)
     -- ^ Borrow a range of array cells, where each cell is 'llvmArrayStride'
-    -- machine words long
+    -- bytes long
   deriving Eq
 
 
@@ -3553,6 +3553,13 @@ llvmAtomicPermToSomeBlock (Perm_LLVMBlock bp) =
   Just $ SomeLLVMBlockPerm $ bp
 llvmAtomicPermToSomeBlock _ = Nothing
 
+-- | Get the lifetime of an atomic perm if it is a field, array, or memblock
+atomicPermLifetime :: AtomicPerm a -> Maybe (PermExpr LifetimeType)
+atomicPermLifetime (Perm_LLVMField fp) = Just $ llvmFieldLifetime fp
+atomicPermLifetime (Perm_LLVMArray ap) = Just $ llvmArrayLifetime ap
+atomicPermLifetime (Perm_LLVMBlock bp) = Just $ llvmBlockLifetime bp
+atomicPermLifetime _ = Nothing
+
 -- | Get the offset of an atomic permission, if it has one
 llvmAtomicPermOffset :: AtomicPerm (LLVMPointerType w) ->
                         Maybe (PermExpr (BVType w))
@@ -4306,6 +4313,37 @@ llvmPermContainsOffset off (Perm_LLVMBlock bp)
     Just ([prop], bvPropHolds prop)
 llvmPermContainsOffset _ _ = Nothing
 
+-- | Test if an atomic LLVM permission contains (in the sense of 'bvPropHolds')
+-- all offsets in a given range
+llvmAtomicPermContainsRange :: (1 <= w, KnownNat w) => BVRange w ->
+                               AtomicPerm (LLVMPointerType w) -> Bool
+llvmAtomicPermContainsRange rng (Perm_LLVMArray ap)
+  | Just ix1 <- matchLLVMArrayIndex ap (bvRangeOffset rng)
+  , Just ix2 <- matchLLVMArrayIndex ap (bvRangeEnd rng)
+  , props <- llvmArrayBorrowInArray ap (RangeBorrow $ BVRange
+                                        (llvmArrayIndexCell ix1)
+                                        (llvmArrayIndexCell ix2)) =
+    all bvPropHolds props
+llvmAtomicPermContainsRange rng (Perm_LLVMField fp) =
+  bvRangeSubset rng (llvmFieldRange fp)
+llvmAtomicPermContainsRange rng (Perm_LLVMBlock bp) =
+  bvRangeSubset rng (llvmBlockRange bp)
+llvmAtomicPermContainsRange _ _ = False
+
+-- | Test if an atomic LLVM permission has a range that overlaps with (in the
+-- sense of 'bvPropHolds') the offsets in a given range
+llvmAtomicPermOverlapsRange :: (1 <= w, KnownNat w) => BVRange w ->
+                               AtomicPerm (LLVMPointerType w) -> Bool
+llvmAtomicPermOverlapsRange rng (Perm_LLVMArray ap) =
+  bvRangesOverlap rng (llvmArrayAbsOffsets ap) &&
+  not (null $ bvRangesDelete rng $
+       map (llvmArrayBorrowOffsets ap) (llvmArrayBorrows ap))
+llvmAtomicPermOverlapsRange rng (Perm_LLVMField fp) =
+  bvRangesOverlap rng (llvmFieldRange fp)
+llvmAtomicPermOverlapsRange rng (Perm_LLVMBlock bp) =
+  bvRangesOverlap rng (llvmBlockRange bp)
+llvmAtomicPermOverlapsRange _ _ = False
+
 -- | Search through a list of permissions for either some permission that
 -- definitely contains (as in 'bvPropHolds') the given offset or, failing that,
 -- and if the supplied 'Bool' flag is 'True', for all permissions that could (as

heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs

@@ -3601,6 +3601,15 @@ tcEmitLLVMStmt _arch _ctx _loc stmt =
 -- * Permission Checking for Jump Targets and Termination Statements
 ----------------------------------------------------------------------
 
+-- | Cast the primary permission for @x@ using any equality permissions in scope
+castPermForVar :: NuMatchingAny1 r => ExprVar a -> ImplM vars s r RNil RNil ()
+castPermForVar x =
+  getPerm x >>>= \p ->
+  substEqsWithProof p >>>= \eqp ->
+  implPushM x p >>>
+  implCastPermM x eqp >>>
+  implPopM x (someEqProofRHS eqp)
+
 -- | Simplify and drop permissions @p@ on variable @x@ so they only depend on
 -- the determined variables given in the supplied list
 simplify1PermForDetVars :: NuMatchingAny1 r =>
@@ -3661,6 +3670,7 @@ simplifyPermsForDetVars det_vars_list =
   let det_vars = NameSet.fromList det_vars_list in
   (permSetVars <$> getPerms) >>>= \vars ->
   mapM_ (\(SomeName x) ->
+          castPermForVar x >>>
           getPerm x >>>= simplify1PermForDetVars det_vars x) vars