Merge pull request #1365 from GaloisInc/rust-heapster-translation

Improvements to the Heapster Rust translation

heapster-saw/examples/Makefile

@@ -5,7 +5,8 @@ Makefile.coq: _CoqProject
 
 include Makefile.coq
 
-SAW=saw
+# If the saw executable is available, use it, otherwise fall back on cabal run saw
+SAW=$(shell which saw || echo cabal run saw)
 
 %.bc: %.c
 	clang -emit-llvm -g -c $<

heapster-saw/examples/_CoqProject

@@ -22,3 +22,4 @@ rust_data.v
 rust_data_proofs.v
 rust_lifetimes.v
 rust_lifetimes_proofs.v
+arrays.v

heapster-saw/examples/rust_data.rs

@@ -287,3 +287,31 @@ pub fn hash_map_insert_gt_to_le (m: &mut HashMap<u64,u64>, x:u64, y:u64) -> () {
         m.insert (y, x);
     }
 }
+
+/* A tree whose internal nodes contain vectors of children */
+pub enum Tree<X> {
+    Leaf (X),
+    Node (Vec<Tree<X>>)
+}
+
+pub fn tree_is_leaf (t: &Tree<u64>) -> bool {
+    match *t {
+        Tree::Leaf (_) => true,
+        Tree::Node (_) => false
+    }
+}
+
+/* Sum all leaves in a tree */
+/*
+pub fn tree_sum (t: &Tree<u64>) -> u64 {
+    let mut acc = 0;
+    match *t {
+        Tree::Leaf (x) => x,
+        Tree::Node (children) =>
+            for u in children {
+                acc += tree_sum (u);
+            }
+            acc;
+    }
+}
+*/

heapster-saw/examples/rust_data.saw

@@ -51,11 +51,17 @@ heapster_define_rust_type env "pub struct MixedStruct { pub s: String, pub i1: u
 heapster_define_rust_type env "pub enum TrueEnum { Foo, Bar, Baz }";
 
 // Opaque type for Vec<T>
-//heapster_define_opaque_llvmshape env "Vec" 64 "T:llvmshape 64" "24" "\\ (T:sort 0) -> List T";
+heapster_define_opaque_llvmshape env "Vec" 64 "T:llvmshape 64" "24" "\\ (T:sort 0) -> List T";
 
 // Opaque type for HashMap<T,U>
 heapster_define_opaque_llvmshape env "HashMap" 64 "T:llvmshape 64, U:llvmshape 64" "56" "\\ (T:sort 0) (U:sort 0) -> List (T * U)";
 
+// Tree<X> type
+// FIXME: this does not work yet because Heapster cannot yet handle recursive types
+// where the type being defined is passed to an opaque or recursvie type
+//heapster_define_rust_type env "pub enum Tree<X> { Leaf (X), Node (Vec<Tree<X>>) }";
+
+
 
 /***
  *** Assumed Functions

heapster-saw/examples/rust_data.v

@@ -44,6 +44,9 @@ Definition foldList_IRT : forall (e0 : Type), forall (p0 : @SAWCorePrelude.Eithe
 Definition unfoldList_IRT : forall (e0 : Type), forall (p0 : @List_IRT e0), @SAWCorePrelude.Either (prod unit unit) (prod unit (prod e0 (prod (@List_IRT e0) unit))) :=
   fun (e0 : Type) => @SAWCorePrelude.unfoldIRT (@List_IRTTyVars e0) (@SAWCorePrelude.IRTs_Nil (@List_IRTTyVars e0)) (@List_IRTDesc e0).
 
+Definition Vec0 : forall (e0 : Type), Type :=
+  fun (T : Type) => @Datatypes.list T.
+
 Definition HashMap : forall (e0 : Type), forall (e1 : Type), Type :=
   fun (T : Type) (U : Type) => @Datatypes.list (prod T U).
 

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

@@ -82,6 +82,16 @@ traverseRAssign :: Applicative m => (forall x. f x -> m (g x)) ->
 traverseRAssign _ MNil = pure MNil
 traverseRAssign f (xs :>: x) = (:>:) <$> traverseRAssign f xs <*> f x
 
+-- FIXME HERE: this should move to Hobbits
+instance Closable a => Closable (Maybe a) where
+  toClosed Nothing = $(mkClosed [| Nothing |])
+  toClosed (Just a) = $(mkClosed [| Just |]) `clApply` toClosed a
+
+-- FIXME HERE: this should move to Hobbits
+instance (Closable a, Closable b) => Closable (a,b) where
+  toClosed (a,b) =
+    $(mkClosed [| (,) |]) `clApply` toClosed a `clApply` toClosed b
+
 
 ----------------------------------------------------------------------
 -- * Helper Functions for 'NatRepr' and 'KnownNat'

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

@@ -77,13 +77,100 @@ askExprCtxTerms = exprCtxToTerms <$> infoCtx <$> ask
 
 
 ----------------------------------------------------------------------
--- The monad for translating IRT type variables
+-- * Names of the recursive permission or shape being defined
 ----------------------------------------------------------------------
 
+-- | The name of the recursive permission or shape being defined
 data IRTRecName args where
   IRTRecPermName :: NamedPermName ns args tp -> IRTRecName args
   IRTRecShapeName :: NatRepr w -> NamedShape 'True args w -> IRTRecName args
 
+-- | Generic function to test if an object contains an 'IRTRecName'
+class ContainsIRTRecName a where
+  containsIRTRecName :: IRTRecName args -> a -> Bool
+
+instance ContainsIRTRecName a => ContainsIRTRecName [a] where
+  containsIRTRecName n = any (containsIRTRecName n)
+
+instance ContainsIRTRecName a => ContainsIRTRecName (Mb ctx a) where
+  containsIRTRecName n = mbLift . fmap (containsIRTRecName n)
+
+instance ContainsIRTRecName (PermExpr a) where
+  containsIRTRecName (IRTRecShapeName w nm_sh) (PExpr_NamedShape _ _ nm_sh' _)
+    | Just Refl <- testEquality w (natRepr nm_sh')
+    , Just _ <- namedShapeEq nm_sh nm_sh' = True
+  containsIRTRecName n (PExpr_NamedShape _ _ _ args) =
+    containsIRTRecName n args
+  containsIRTRecName n (PExpr_PtrShape _ _ sh) = containsIRTRecName n sh
+  containsIRTRecName n (PExpr_FieldShape fsh) = containsIRTRecName n fsh
+  containsIRTRecName n (PExpr_ArrayShape _ _ fshs) = containsIRTRecName n fshs
+  containsIRTRecName n (PExpr_SeqShape sh1 sh2) =
+    containsIRTRecName n sh1 || containsIRTRecName n sh2
+  containsIRTRecName n (PExpr_OrShape sh1 sh2) =
+    containsIRTRecName n sh1 || containsIRTRecName n sh2
+  containsIRTRecName n (PExpr_ExShape mb_sh) =
+    mbLift $ fmap (containsIRTRecName n) mb_sh
+  containsIRTRecName n (PExpr_ValPerm p) = containsIRTRecName n p
+  containsIRTRecName _ _ = False
+
+instance ContainsIRTRecName (RAssign PermExpr tps) where
+  containsIRTRecName _ MNil = False
+  containsIRTRecName n (es :>: e) =
+    containsIRTRecName n es || containsIRTRecName n e
+
+instance ContainsIRTRecName (LLVMFieldShape a) where
+  containsIRTRecName n (LLVMFieldShape p) = containsIRTRecName n p
+
+instance ContainsIRTRecName (ValuePerm a) where
+  containsIRTRecName n (ValPerm_Eq e) = containsIRTRecName n e
+  containsIRTRecName n (ValPerm_Or p1 p2) =
+    containsIRTRecName n p1 || containsIRTRecName n p2
+  containsIRTRecName n (ValPerm_Exists mb_p) =
+    mbLift $ fmap (containsIRTRecName n) mb_p
+  containsIRTRecName (IRTRecPermName npn) (ValPerm_Named npn' _ _)
+    | Just _ <- testNamedPermNameEq npn npn' = True
+  containsIRTRecName n (ValPerm_Named _ args _) =
+    containsIRTRecName n args
+  containsIRTRecName _ (ValPerm_Var _ _) = False
+  containsIRTRecName n (ValPerm_Conj ps) = containsIRTRecName n ps
+
+instance ContainsIRTRecName (RAssign ValuePerm tps) where
+  containsIRTRecName _ MNil = False
+  containsIRTRecName n (ps :>: p) =
+    containsIRTRecName n ps || containsIRTRecName n p
+
+instance ContainsIRTRecName (AtomicPerm a) where
+  containsIRTRecName n (Perm_LLVMField fp) = containsIRTRecName n fp
+  containsIRTRecName n (Perm_LLVMArray arrp) =
+    containsIRTRecName n (llvmArrayFields arrp)
+  containsIRTRecName n (Perm_LLVMBlock bp) =
+    containsIRTRecName n (llvmBlockShape bp)
+  containsIRTRecName _ (Perm_LLVMFree _) = False
+  containsIRTRecName _ (Perm_LLVMFunPtr _ _) = False
+  containsIRTRecName n (Perm_LLVMBlockShape sh) = containsIRTRecName n sh
+  containsIRTRecName _ Perm_IsLLVMPtr = False
+  containsIRTRecName (IRTRecPermName npn) (Perm_NamedConj npn' _ _)
+    | Just _ <- testNamedPermNameEq npn npn' = True
+  containsIRTRecName n (Perm_NamedConj _ args _) = containsIRTRecName n args
+  containsIRTRecName n (Perm_LLVMFrame fperm) =
+    containsIRTRecName n (map fst fperm)
+  containsIRTRecName _ (Perm_LOwned _ _) = False
+  containsIRTRecName _ (Perm_LCurrent _) = False
+  containsIRTRecName n (Perm_Struct ps) = containsIRTRecName n ps
+  containsIRTRecName _ (Perm_Fun _) = False
+  containsIRTRecName _ (Perm_BVProp _) = False
+
+instance ContainsIRTRecName (LLVMArrayField w) where
+  containsIRTRecName n (LLVMArrayField fp) = containsIRTRecName n fp
+
+instance ContainsIRTRecName (LLVMFieldPerm w sz) where
+  containsIRTRecName n fp = containsIRTRecName n $ llvmFieldContents fp
+
+
+----------------------------------------------------------------------
+-- * The monad for translating IRT type variables
+----------------------------------------------------------------------
+
 data IRTTyVarsTransCtx args ext =
   IRTTyVarsTransCtx
   {
@@ -150,7 +237,7 @@ irtTSubstExt x =
 
 
 ----------------------------------------------------------------------
--- Trees for keeping track of IRT variable indices
+-- * Trees for keeping track of IRT variable indices
 ----------------------------------------------------------------------
 
 data IRTVarTree a = IRTVarsNil
@@ -174,7 +261,7 @@ setIRTVarIdxs tree = evalState (mapM (\_ -> nextIdx) tree) 0
 
 
 ----------------------------------------------------------------------
--- Translating IRT type variables
+-- * Translating IRT type variables
 ----------------------------------------------------------------------
 
 -- | Given the name of a recursive permission being defined and its argument
@@ -364,6 +451,9 @@ instance IRTTyVars (PermExpr (LLVMShapeType w)) where
            _ -> case mbMatch $ namedShapeBody <$> nmsh of
                   [nuMP| DefinedShapeBody _ |] ->
                     irtTyVars (mbMap2 unfoldNamedShape nmsh args)
+                  _ | containsIRTRecName n_rec mb_sh ->
+                      throwError ("recursive shape passed to an opaque or"
+                                  ++ " recursive shape in its definition!")
                   _ -> do sh' <- irtTSubstExt mb_sh
                           let sh_trans = transTupleTerm <$> translate sh'
                           return ([sh_trans], IRTVar ())
@@ -396,7 +486,7 @@ instance IRTTyVars (RAssign ValuePerm ps) where
 
 
 ----------------------------------------------------------------------
--- The IRTDesc translation monad
+-- * The IRTDesc translation monad
 ----------------------------------------------------------------------
 
 -- | Contextual info for translating IRT type descriptions
@@ -462,7 +552,7 @@ irtCtor c all_args =
 
 
 ----------------------------------------------------------------------
--- Translating IRT type descriptions
+-- * Translating IRT type descriptions
 ----------------------------------------------------------------------
 
 -- | Given an identifier whose definition in the shared context is the first
@@ -636,7 +726,7 @@ instance IRTDescs (RAssign ValuePerm ps) where
 
 
 ----------------------------------------------------------------------
--- Translating IRT definitions
+-- * Translating IRT definitions
 ----------------------------------------------------------------------
 
 -- | Given identifiers whose definitions in the shared context are the results

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

@@ -1988,24 +1988,25 @@ data NamedShapeBody b args w where
   -- | A recursive shape body has a one-step unfolding to a shape, which can
   -- refer to the shape itself via the last bound variable; it also has
   -- identifiers for the type it is translated to, along with fold and unfold
-  -- functions for mapping to and from this type
+  -- functions for mapping to and from this type. The fold and unfold functions
+  -- can be undefined if we are in the process of defining this recusive shape.
   RecShapeBody :: Mb (args :> LLVMShapeType w) (PermExpr (LLVMShapeType w)) ->
-                  Ident -> Ident -> Ident ->
+                  Ident -> Maybe (Ident, Ident) ->
                   NamedShapeBody 'True args w
 
 deriving instance Eq (NamedShapeBody b args w)
 
 -- | Test if a 'NamedShape' is recursive
 namedShapeIsRecursive :: NamedShape b args w -> Bool
-namedShapeIsRecursive (NamedShape _ _ (RecShapeBody _ _ _ _)) = True
+namedShapeIsRecursive (NamedShape _ _ (RecShapeBody _ _ _)) = True
 namedShapeIsRecursive _ = False
 
 -- | Get a 'BoolRepr' for the Boolean flag for whether a named shape can be
 -- unfolded
 namedShapeCanUnfoldRepr :: NamedShape b args w -> BoolRepr b
 namedShapeCanUnfoldRepr (NamedShape _ _ (DefinedShapeBody _)) = TrueRepr
 namedShapeCanUnfoldRepr (NamedShape _ _ (OpaqueShapeBody _ _)) = FalseRepr
-namedShapeCanUnfoldRepr (NamedShape _ _ (RecShapeBody _ _ _ _)) = TrueRepr
+namedShapeCanUnfoldRepr (NamedShape _ _ (RecShapeBody _ _ _)) = TrueRepr
 
 -- | Whether a 'NamedShape' can be unfolded
 namedShapeCanUnfold :: NamedShape b args w -> Bool
@@ -3245,7 +3246,7 @@ llvmShapeLength (PExpr_NamedShape _ _ (NamedShape _ _
                                        (OpaqueShapeBody mb_len _)) args) =
   Just $ subst (substOfExprs args) mb_len
 llvmShapeLength (PExpr_NamedShape _ _ nmsh@(NamedShape _ _
-                                            (RecShapeBody _ _ _ _)) args) =
+                                            (RecShapeBody _ _ _)) args) =
   -- FIXME: if the recursive shape contains itself *not* under a pointer, then
   -- this could diverge
   llvmShapeLength (unfoldNamedShape nmsh args)
@@ -3395,7 +3396,7 @@ unfoldNamedShape :: KnownNat w => NamedShape 'True args w -> PermExprs args ->
                     PermExpr (LLVMShapeType w)
 unfoldNamedShape (NamedShape _ _ (DefinedShapeBody mb_sh)) args =
   subst (substOfExprs args) mb_sh
-unfoldNamedShape sh@(NamedShape _ _ (RecShapeBody mb_sh _ _ _)) args =
+unfoldNamedShape sh@(NamedShape _ _ (RecShapeBody mb_sh _ _)) args =
   subst (substOfExprs (args :>: PExpr_NamedShape Nothing Nothing sh args)) mb_sh
 
 -- | Unfold a named shape and apply 'modalizeShape' to the result
@@ -4354,7 +4355,7 @@ shapeIsCopyable rw (PExpr_NamedShape maybe_rw' _ nmsh args) =
     -- HACK: the real computation we want to perform is to assume nmsh is copyable
     -- and prove it is under that assumption; to accomplish this, we substitute
     -- the empty shape for the recursive shape
-    RecShapeBody mb_sh _ _ _ ->
+    RecShapeBody mb_sh _ _ ->
       shapeIsCopyable rw $ subst (substOfExprs (args :>: PExpr_EmptyShape)) mb_sh
 shapeIsCopyable _ (PExpr_EqShape _) = True
 shapeIsCopyable rw (PExpr_PtrShape maybe_rw' _ sh) =
@@ -4640,7 +4641,7 @@ instance FreeVars (NamedShape b args w) where
 instance FreeVars (NamedShapeBody b args w) where
   freeVars (DefinedShapeBody mb_sh) = freeVars mb_sh
   freeVars (OpaqueShapeBody mb_len _) = freeVars mb_len
-  freeVars (RecShapeBody mb_sh _ _ _) = freeVars mb_sh
+  freeVars (RecShapeBody mb_sh _ _) = freeVars mb_sh
 
 
 -- | Test if an expression @e@ is a /determining/ expression, meaning that
@@ -4971,11 +4972,10 @@ genSubstNSB px s mb_body = case mbMatch mb_body of
       DefinedShapeBody <$> genSubstMb px s mb_sh
     [nuMP| OpaqueShapeBody mb_len trans_id |] ->
       OpaqueShapeBody <$> genSubstMb px s mb_len <*> return (mbLift trans_id)
-    [nuMP| RecShapeBody mb_sh trans_id fold_id unfold_id |] ->
+    [nuMP| RecShapeBody mb_sh trans_id fold_ids |] ->
       RecShapeBody <$> genSubstMb (px :>: Proxy) s mb_sh
                    <*> return (mbLift trans_id)
-                   <*> return (mbLift fold_id)
-                   <*> return (mbLift unfold_id)
+                   <*> return (mbLift fold_ids)
 
 instance SubstVar s m => Substable s (NamedPermName ns args a) m where
   genSubst _ mb_rpn = return $ mbLift mb_rpn
@@ -5873,12 +5873,11 @@ instance AbstractVars (NamedShapeBody b args w) where
     absVarsReturnH ns1 ns2 ($(mkClosed [| \i l -> OpaqueShapeBody l i |])
                              `clApply` toClosed trans_id)
     `clMbMbApplyM` abstractPEVars ns1 ns2 mb_len
-  abstractPEVars ns1 ns2 (RecShapeBody mb_sh trans_id fold_id unfold_id) =
+  abstractPEVars ns1 ns2 (RecShapeBody mb_sh trans_id fold_ids) =
     absVarsReturnH ns1 ns2 ($(mkClosed
-                              [| \i1 i2 i3 l -> RecShapeBody l i1 i2 i3 |])
+                              [| \i1 i2 l -> RecShapeBody l i1 i2 |])
                              `clApply` toClosed trans_id
-                             `clApply` toClosed fold_id
-                             `clApply` toClosed unfold_id)
+                             `clApply` toClosed fold_ids)
     `clMbMbApplyM` abstractPEVars ns1 ns2 mb_sh
 
 instance AbstractVars (NamedPermName ns args a) where

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

@@ -270,14 +270,16 @@ namedTypeTable w =
 -- @Foo<X>::Bar<Y,Z>::Baz@ just becomes @[Foo,Bar,Baz]@
 newtype RustName = RustName [Ident] deriving (Eq)
 
+-- | Convert a 'RustName' to a string by interspersing "::"
+flattenRustName :: RustName -> String
+flattenRustName (RustName ids) = concat $ intersperse "::" $ map name ids
+
 instance Show RustName where
-  show (RustName ids) = concat $ intersperse "::" $ map show ids
+  show = show . flattenRustName
 
 instance RsConvert w RustName (SomeShapeFun w) where
-  rsConvert w (RustName elems) =
-    -- FIXME: figure out how to actually resolve names; for now we just look at
-    -- the last string component...
-    do let str = name $ last elems
+  rsConvert w nm =
+    do let str = flattenRustName nm
        env <- rciPermEnv <$> ask
        case lookupNamedShape env str of
          Just nmsh -> namedShapeShapeFun (natRepr w) nmsh