Merge pull request #1650 from GaloisInc/heapster/arrays-unify

WIP: Heapster/try unifying arrays

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)))
+
+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) ->
   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 $ str3Block 0 ===> charArray 0 3
     ]
 
   , testGroup "mix of permission types"

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,<len1,*stride,sh,bs1)
-  -- > -o x:[2]memblock(rw,off1,<len1,*stride,sh,bs1) *  x:[l]array(rw,off,<len,*stride,sh,bs)
+  -- > x:[l2]memblock(rw,off1,<len1,*stride,sh)
+  -- > -o x:[2]memblock(rw,off1,<len1,*stride,sh)
+  -- >    * x:[l]array(rw,off,<len,*stride,sh,bs)
   SImpl_LLVMArrayBorrowed ::
     (1 <= w, KnownNat w) =>
     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)
@@ -6706,6 +6706,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
@@ -6789,22 +6825,38 @@ 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).
+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
   -- 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?

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
 {-
@@ -243,9 +245,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

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

@@ -4078,6 +4078,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) ->

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