Heapster Widening and Implication Prover Improvements

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

@@ -5791,9 +5791,30 @@ recombinePerm' x (ValPerm_Conj x_ps) (ValPerm_Conj (p:ps)) =
   recombinePermConj x x_ps p >>>
   recombinePerm x (ValPerm_Conj ps)
 recombinePerm' x x_p (ValPerm_Named npn args off)
+  -- When recombining a conjuctive named permission, turn it into a conjunction
+  -- and recombine it
   | TrueRepr <- nameIsConjRepr npn =
     implNamedToConjM x npn args off >>>
     recombinePermExpl x x_p (ValPerm_Conj1 $ Perm_NamedConj npn args off)
+recombinePerm' x x_p (ValPerm_Named npn args off)
+  -- When recombining a non-conjuctive but unfoldable named permission, unfold
+  -- it and recombine it
+  | TrueRepr <- nameCanFoldRepr npn =
+    implUnfoldNamedM x npn args off >>>= \p' ->
+    recombinePermExpl x x_p p'
+recombinePerm' x x_p@(ValPerm_Named npn args off) p
+  -- When recombining into a conjuctive named permission, turn it into a
+  -- conjunction and recombine it
+  | TrueRepr <- nameIsConjRepr npn =
+    implPushM x x_p >>> implNamedToConjM x npn args off >>>
+    let x_p' = ValPerm_Conj1 $ Perm_NamedConj npn args off in
+    implPopM x x_p' >>> recombinePermExpl x x_p' p
+recombinePerm' x x_p@(ValPerm_Named npn args off) p
+  -- When recombining into a non-conjuctive but unfoldable named permission, unfold
+  -- it and recombine it
+  | TrueRepr <- nameCanFoldRepr npn =
+    implPushM x x_p >>> implUnfoldNamedM x npn args off >>>= \x_p' ->
+    implPopM x x_p' >>> recombinePermExpl x x_p' p
 recombinePerm' x _ p = implDropM x p
 
 -- | Recombine a single conjuct @x:p@ on top of the stack back into the existing

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

@@ -4748,37 +4748,46 @@ mbExBlockToSubShape a =
   mbMapCl ($(mkClosed [| exBlockToSubShape |]) `clApply` toClosed a)
 
 -- | Split a block permission into portions that are before and after a given
--- offset, if possible, assuming the offset is in the block permission
-splitLLVMBlockPerm :: (1 <= w, KnownNat w) => PermExpr (BVType w) ->
-                      LLVMBlockPerm w ->
-                      Maybe (LLVMBlockPerm w, LLVMBlockPerm w)
-splitLLVMBlockPerm off bp
+-- offset, if possible, assuming the offset is in the block permission. The
+-- supplied function provides a partial substitution from variables of
+-- 'LLVMBlockType' to their shapes, in order to split @eqsh@ shapes.
+splitLLVMBlockPerm ::
+  (1 <= w, KnownNat w) =>
+  (ExprVar (LLVMBlockType w) -> Maybe (PermExpr (LLVMShapeType w))) ->
+  PermExpr (BVType w) -> LLVMBlockPerm w ->
+  Maybe (LLVMBlockPerm w, LLVMBlockPerm w)
+splitLLVMBlockPerm _ off bp
   | bvEq off (llvmBlockOffset bp)
   = Just (bp { llvmBlockLen = bvInt 0, llvmBlockShape = PExpr_EmptyShape },
           bp)
-splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_EmptyShape) =
+splitLLVMBlockPerm _ off bp@(llvmBlockShape -> PExpr_EmptyShape) =
   Just (bp { llvmBlockLen = bvSub off (llvmBlockOffset bp) },
         bp { llvmBlockOffset = off,
              llvmBlockLen = bvSub (llvmBlockEndOffset bp) off })
-splitLLVMBlockPerm off bp@(LLVMBlockPerm { llvmBlockShape = sh })
+splitLLVMBlockPerm blsubst off bp@(LLVMBlockPerm { llvmBlockShape = sh })
   | Just sh_len <- llvmShapeLength sh
   , bvLt sh_len (bvSub off (llvmBlockOffset bp)) =
     -- If we are splitting after the end of the natural length of a shape, then
     -- pad out the block permission to its natural length and fall back to the
     -- sequence shape case below
-    splitLLVMBlockPerm off (bp { llvmBlockShape =
-                                   PExpr_SeqShape sh PExpr_EmptyShape })
-splitLLVMBlockPerm _ (llvmBlockShape -> PExpr_Var _) = Nothing
-splitLLVMBlockPerm off bp@(llvmBlockShape ->
-                           PExpr_NamedShape maybe_rw maybe_l nmsh args)
+    splitLLVMBlockPerm blsubst off (bp { llvmBlockShape =
+                                         PExpr_SeqShape sh PExpr_EmptyShape })
+splitLLVMBlockPerm _ _ (llvmBlockShape -> PExpr_Var _) = Nothing
+splitLLVMBlockPerm blsubst off bp@(llvmBlockShape ->
+                                   PExpr_NamedShape maybe_rw maybe_l nmsh args)
   | TrueRepr <- namedShapeCanUnfoldRepr nmsh
   , Just sh' <- unfoldModalizeNamedShape maybe_rw maybe_l nmsh args =
-    splitLLVMBlockPerm off (bp { llvmBlockShape = sh' })
-splitLLVMBlockPerm _ (llvmBlockShape -> PExpr_NamedShape _ _ _ _) = Nothing
-splitLLVMBlockPerm _ (llvmBlockShape -> PExpr_EqShape _ _) = Nothing
-splitLLVMBlockPerm _ (llvmBlockShape -> PExpr_PtrShape _ _ _) = Nothing
-splitLLVMBlockPerm _ (llvmBlockShape -> PExpr_FieldShape _) = Nothing
-splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_ArrayShape len stride sh)
+    splitLLVMBlockPerm blsubst off (bp { llvmBlockShape = sh' })
+splitLLVMBlockPerm _ _ (llvmBlockShape -> PExpr_NamedShape _ _ _ _) = Nothing
+splitLLVMBlockPerm blsubst off bp@(llvmBlockShape ->
+                                   PExpr_EqShape _len (PExpr_Var b))
+  -- FIXME: make sure the returned shape fits into len bytes!
+  | Just sh <- blsubst b
+  = splitLLVMBlockPerm blsubst off (bp { llvmBlockShape = sh })
+splitLLVMBlockPerm _ _ (llvmBlockShape -> PExpr_EqShape _ _) = Nothing
+splitLLVMBlockPerm _ _ (llvmBlockShape -> PExpr_PtrShape _ _ _) = Nothing
+splitLLVMBlockPerm _ _ (llvmBlockShape -> PExpr_FieldShape _) = Nothing
+splitLLVMBlockPerm _ off bp@(llvmBlockShape -> PExpr_ArrayShape len stride sh)
   | Just (ix, BV.BV 0) <-
       bvMatchFactorPlusConst (bytesToInteger stride) (bvSub off $
                                                       llvmBlockOffset bp)
@@ -4788,35 +4797,35 @@ splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_ArrayShape len stride sh)
           bp { llvmBlockOffset = off,
                llvmBlockLen = bvSub (llvmBlockLen bp) off_diff,
                llvmBlockShape = PExpr_ArrayShape (bvSub len ix) stride sh })
-splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_SeqShape sh1 sh2)
+splitLLVMBlockPerm blsubst off bp@(llvmBlockShape -> PExpr_SeqShape sh1 sh2)
   | Just sh1_len <- llvmShapeLength sh1
   , off_diff <- bvSub off (llvmBlockOffset bp)
   , bvLt off_diff sh1_len
-  = splitLLVMBlockPerm off (bp { llvmBlockLen = sh1_len,
-                                 llvmBlockShape = sh1 }) >>= \(bp1,bp2) ->
+  = splitLLVMBlockPerm blsubst off (bp { llvmBlockLen = sh1_len,
+                                         llvmBlockShape = sh1 }) >>= \(bp1,bp2) ->
     Just (bp1,
           bp2 { llvmBlockLen = bvSub (llvmBlockLen bp) off_diff,
                 llvmBlockShape = PExpr_SeqShape (llvmBlockShape bp2) sh2 })
-splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_SeqShape sh1 sh2)
+splitLLVMBlockPerm blsubst off bp@(llvmBlockShape -> PExpr_SeqShape sh1 sh2)
   | Just sh1_len <- llvmShapeLength sh1
-  = splitLLVMBlockPerm off
+  = splitLLVMBlockPerm blsubst off
     (bp { llvmBlockOffset = bvAdd (llvmBlockOffset bp) sh1_len,
           llvmBlockLen = bvSub (llvmBlockLen bp) sh1_len,
           llvmBlockShape = sh2 }) >>= \(bp1,bp2) ->
     Just (bp1 { llvmBlockOffset = llvmBlockOffset bp,
                 llvmBlockLen = bvAdd (llvmBlockLen bp1) sh1_len,
                 llvmBlockShape = PExpr_SeqShape sh1 (llvmBlockShape bp1) },
           bp2)
-splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_OrShape sh1 sh2) =
-  do (bp1_L,bp1_R) <- splitLLVMBlockPerm off (bp { llvmBlockShape = sh1 })
-     (bp2_L,bp2_R) <- splitLLVMBlockPerm off (bp { llvmBlockShape = sh2 })
+splitLLVMBlockPerm blsubst off bp@(llvmBlockShape -> PExpr_OrShape sh1 sh2) =
+  do (bp1_L,bp1_R) <- splitLLVMBlockPerm blsubst off (bp { llvmBlockShape = sh1 })
+     (bp2_L,bp2_R) <- splitLLVMBlockPerm blsubst off (bp { llvmBlockShape = sh2 })
      let or_helper bp1 bp2 =
            bp1 { llvmBlockShape =
                    PExpr_OrShape (llvmBlockShape bp1) (llvmBlockShape bp2)}
      Just (or_helper bp1_L bp2_L, or_helper bp1_R bp2_R)
-splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_ExShape mb_sh) =
-  case mbMatch $ fmap (\sh -> splitLLVMBlockPerm off
-                                (bp { llvmBlockShape = sh })) mb_sh of
+splitLLVMBlockPerm blsubst off bp@(llvmBlockShape -> PExpr_ExShape mb_sh) =
+  case mbMatch $ fmap (\sh -> splitLLVMBlockPerm blsubst off
+                              (bp { llvmBlockShape = sh })) mb_sh of
     [nuMP| Just (mb_bp1,mb_bp2) |] ->
       let off_diff = bvSub off (llvmBlockOffset bp) in
       Just (bp { llvmBlockLen = off_diff,
@@ -4825,23 +4834,30 @@ splitLLVMBlockPerm off bp@(llvmBlockShape -> PExpr_ExShape mb_sh) =
                  llvmBlockLen = bvSub (llvmBlockLen bp) off_diff,
                  llvmBlockShape = PExpr_ExShape (fmap llvmBlockShape mb_bp2) })
     _ -> Nothing
-splitLLVMBlockPerm _ _ = Nothing
+splitLLVMBlockPerm _ _ _ = Nothing
 
 -- | Remove a range of offsets from a block permission, if possible, yielding a
 -- list of block permissions for the remaining offsets
-remLLVMBLockPermRange :: (1 <= w, KnownNat w) => BVRange w -> LLVMBlockPerm w ->
+remLLVMBlockPermRange :: (1 <= w, KnownNat w) => BVRange w -> LLVMBlockPerm w ->
                          Maybe [LLVMBlockPerm w]
-remLLVMBLockPermRange rng bp
+remLLVMBlockPermRange rng bp
   | bvRangeSubset (llvmBlockRange bp) rng = Just []
-remLLVMBLockPermRange rng bp =
+remLLVMBlockPermRange rng bp =
   do (bps_l, bp') <-
+       -- If the beginning of rng lies inside the range of bp, split bp into
+       -- block permissions before and after the beginning of rng; otherwise,
+       -- lump all of bp into the "after" bucket. The call to splitLLVMBlockPerm
+       -- uses an empty substitution because remLLVMBlockPermRange itself is
+       -- assuming an empty substitution
        if bvInRange (bvRangeOffset rng) (llvmBlockRange bp) then
-         do (bp_l,bp') <- splitLLVMBlockPerm (bvRangeOffset rng) bp
+         do (bp_l,bp') <- splitLLVMBlockPerm (const Nothing) (bvRangeOffset rng) bp
             return ([bp_l],bp')
        else return ([],bp)
      bp_r <-
+       -- Split bp', the permissions after the beginning of rng, into those
+       -- before and after the end of rng
        if bvInRange (bvRangeEnd rng) (llvmBlockRange bp) then
-         snd <$> splitLLVMBlockPerm (bvRangeEnd rng) bp
+         snd <$> splitLLVMBlockPerm (const Nothing) (bvRangeEnd rng) bp'
        else return bp'
      return (bps_l ++ [bp_r])
 
@@ -6240,6 +6256,20 @@ unfoldPerm :: NameSortCanFold ns ~ 'True => NamedPerm ns args a ->
 unfoldPerm (NamedPerm_Defined dp) = unfoldDefinedPerm dp
 unfoldPerm (NamedPerm_Rec rp) = unfoldRecPerm rp
 
+-- | Unfold a unfoldable conjunctive named permission to a list of conjuncts
+unfoldConjPerm :: NameSortIsConj ns ~ 'True => NameSortCanFold ns ~ 'True =>
+                  NamedPerm ns args a -> PermExprs args -> PermOffset a ->
+                  [AtomicPerm a]
+unfoldConjPerm npn args off
+  | ValPerm_Conj conjs <- unfoldPerm npn args off = conjs
+unfoldConjPerm npn args off
+  | ValPerm_Named npn' args' off' <- unfoldPerm npn args off
+  , TrueRepr <- nameIsConjRepr npn' =
+    [Perm_NamedConj npn' args' off']
+unfoldConjPerm _ _ _ =
+  -- NOTE: this should never happen
+  error "unfoldConjPerm"
+
 -- | Test if two expressions are definitely unequal
 exprsUnequal :: PermExpr a -> PermExpr a -> Bool
 exprsUnequal (PExpr_Var _) _ = False