Heapster substitution improvements (#1437)

* a new approach to genSubstMb to try to preserve the fresh pair representation * changed the Substable instances for tuples to expect fresh pair form * Update to a new version of Hobbits * added translateSimplImplOut and translateSimplImplOutHead to prevent switching back and forth to and from fresh pair form * added new Rust examples for enums with large numbers of constructors * whoops, uncommented the examples in rust_data.saw * updated freeze files
GaloisInc · Aug 31, 2021 · 354cda0 · 354cda0
1 parent 6f70a53
commit 354cda0
Show file tree

Hide file tree

Showing 9 changed files with 247 additions and 68 deletions.
diff --git a/cabal.GHC-8.10.3.config b/cabal.GHC-8.10.3.config
@@ -298,7 +298,7 @@ constraints: any.Cabal ==3.2.1.0,
              any.text-short ==0.1.3,
              text-short -asserts,
              any.tf-random ==0.5,
-             any.th-abstraction ==0.3.2.0,
+             any.th-abstraction ==0.4.2.0,
              any.th-compat ==0.1.1,
              any.th-expand-syns ==0.4.6.0,
              any.th-lift ==0.8.2,

diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config
@@ -300,7 +300,7 @@ constraints: any.Cabal ==3.0.1.0,
              any.text-short ==0.1.3,
              text-short -asserts,
              any.tf-random ==0.5,
-             any.th-abstraction ==0.3.2.0,
+             any.th-abstraction ==0.4.2.0,
              any.th-compat ==0.1.1,
              any.th-expand-syns ==0.4.6.0,
              any.th-lift ==0.8.2,

diff --git a/cabal.project b/cabal.project
@@ -43,4 +43,4 @@ packages:
 source-repository-package
     type: git
     location: https://github.com/eddywestbrook/hobbits.git
-    tag: e5918895396b6bcee2fc39f6bd0d77a90a52ba5f
+    tag: 20b6d18758312deaf6a544d474483e537d5f018f
diff --git a/heapster-saw/examples/rust_data.bc b/heapster-saw/examples/rust_data.bc
diff --git a/heapster-saw/examples/rust_data.rs b/heapster-saw/examples/rust_data.rs
@@ -315,3 +315,138 @@ pub fn tree_sum (t: &Tree<u64>) -> u64 {
     }
 }
 */
+
+/* A 20-element enum that just wraps around type X */
+#[repr(u64)]
+pub enum Enum20<X> {
+  Enum20_0(X),
+  Enum20_1(X),
+  Enum20_2(X),
+  Enum20_3(X),
+  Enum20_4(X),
+  Enum20_5(X),
+  Enum20_6(X),
+  Enum20_7(X),
+  Enum20_8(X),
+  Enum20_9(X),
+  Enum20_10(X),
+  Enum20_11(X),
+  Enum20_12(X),
+  Enum20_13(X),
+  Enum20_14(X),
+  Enum20_15(X),
+  Enum20_16(X),
+  Enum20_17(X),
+  Enum20_18(X),
+  Enum20_19(X),
+}
+
+pub fn enum20_list_proj<'a> (x:&'a Enum20<List<u64>>) -> &'a List<u64> {
+  match x {
+      Enum20::Enum20_0(l) => l,
+      Enum20::Enum20_1(l) => l,
+      Enum20::Enum20_2(l) => l,
+      Enum20::Enum20_3(l) => l,
+      Enum20::Enum20_4(l) => l,
+      Enum20::Enum20_5(l) => l,
+      Enum20::Enum20_6(l) => l,
+      Enum20::Enum20_7(l) => l,
+      Enum20::Enum20_8(l) => l,
+      Enum20::Enum20_9(l) => l,
+      Enum20::Enum20_10(l) => l,
+      Enum20::Enum20_11(l) => l,
+      Enum20::Enum20_12(l) => l,
+      Enum20::Enum20_13(l) => l,
+      Enum20::Enum20_14(l) => l,
+      Enum20::Enum20_15(l) => l,
+      Enum20::Enum20_16(l) => l,
+      Enum20::Enum20_17(l) => l,
+      Enum20::Enum20_18(l) => l,
+      Enum20::Enum20_19(l) => l,
+  }
+}
+
+/* A non-empty list type with 20 separate constructors */
+#[repr(u64)]
+pub enum List10<X> {
+  List10Head(X),
+  List10_0(X,Box<List10<X>>),
+  List10_1(X,Box<List10<X>>),
+  List10_2(X,Box<List10<X>>),
+  List10_3(X,Box<List10<X>>),
+  List10_4(X,Box<List10<X>>),
+  List10_5(X,Box<List10<X>>),
+  List10_6(X,Box<List10<X>>),
+  List10_7(X,Box<List10<X>>),
+  List10_8(X,Box<List10<X>>),
+  List10_9(X,Box<List10<X>>),
+}
+
+pub fn list10_head<'a> (x:&'a List10<List<u64>>) -> &'a List<u64> {
+  match x {
+      List10::List10Head(l) => l,
+      List10::List10_0(l,_) => l,
+      List10::List10_1(l,_) => l,
+      List10::List10_2(l,_) => l,
+      List10::List10_3(l,_) => l,
+      List10::List10_4(l,_) => l,
+      List10::List10_5(l,_) => l,
+      List10::List10_6(l,_) => l,
+      List10::List10_7(l,_) => l,
+      List10::List10_8(l,_) => l,
+      List10::List10_9(l,_) => l,
+  }
+}
+
+
+/* A non-empty list type with 20 separate constructors */
+#[repr(u64)]
+pub enum List20<X> {
+  List20Head(X),
+  List20_0(X,Box<List20<X>>),
+  List20_1(X,Box<List20<X>>),
+  List20_2(X,Box<List20<X>>),
+  List20_3(X,Box<List20<X>>),
+  List20_4(X,Box<List20<X>>),
+  List20_5(X,Box<List20<X>>),
+  List20_6(X,Box<List20<X>>),
+  List20_7(X,Box<List20<X>>),
+  List20_8(X,Box<List20<X>>),
+  List20_9(X,Box<List20<X>>),
+  List20_10(X,Box<List20<X>>),
+  List20_11(X,Box<List20<X>>),
+  List20_12(X,Box<List20<X>>),
+  List20_13(X,Box<List20<X>>),
+  List20_14(X,Box<List20<X>>),
+  List20_15(X,Box<List20<X>>),
+  List20_16(X,Box<List20<X>>),
+  List20_17(X,Box<List20<X>>),
+  List20_18(X,Box<List20<X>>),
+  List20_19(X,Box<List20<X>>),
+}
+
+pub fn list20_head<'a> (x:&'a List20<List<u64>>) -> &'a List<u64> {
+  match x {
+      List20::List20Head(l) => l,
+      List20::List20_0(l,_) => l,
+      List20::List20_1(l,_) => l,
+      List20::List20_2(l,_) => l,
+      List20::List20_3(l,_) => l,
+      List20::List20_4(l,_) => l,
+      List20::List20_5(l,_) => l,
+      List20::List20_6(l,_) => l,
+      List20::List20_7(l,_) => l,
+      List20::List20_8(l,_) => l,
+      List20::List20_9(l,_) => l,
+      List20::List20_10(l,_) => l,
+      List20::List20_11(l,_) => l,
+      List20::List20_12(l,_) => l,
+      List20::List20_13(l,_) => l,
+      List20::List20_14(l,_) => l,
+      List20::List20_15(l,_) => l,
+      List20::List20_16(l,_) => l,
+      List20::List20_17(l,_) => l,
+      List20::List20_18(l,_) => l,
+      List20::List20_19(l,_) => l,
+  }
+}
diff --git a/heapster-saw/examples/rust_data.saw b/heapster-saw/examples/rust_data.saw
@@ -61,6 +61,14 @@ heapster_define_opaque_llvmshape env "HashMap" 64 "T:llvmshape 64, U:llvmshape 6
 // 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>>) }";
 
+// Enum20 type
+heapster_define_rust_type env "pub enum Enum20<X> { Enum20_0(X), Enum20_1(X), Enum20_2(X), Enum20_3(X), Enum20_4(X), Enum20_5(X), Enum20_6(X), Enum20_7(X), Enum20_8(X), Enum20_9(X), Enum20_10(X), Enum20_11(X), Enum20_12(X), Enum20_13(X), Enum20_14(X), Enum20_15(X), Enum20_16(X), Enum20_17(X), Enum20_18(X), Enum20_19(X), }";
+
+// List10 type
+heapster_define_rust_type env "pub enum List10<X> { List10_Head(X,Box<List10<X>>), List10_0(X,Box<List10<X>>), List10_1(X,Box<List10<X>>), List10_2(X,Box<List10<X>>), List10_3(X,Box<List10<X>>), List10_4(X,Box<List10<X>>), List10_5(X,Box<List10<X>>), List10_6(X,Box<List10<X>>), List10_7(X,Box<List10<X>>), List10_8(X,Box<List10<X>>), List10_9(X,Box<List10<X>>), }";
+
+// List20 type
+heapster_define_rust_type env "pub enum List20<X> { List20_Head(X,Box<List20<X>>), List20_0(X,Box<List20<X>>), List20_1(X,Box<List20<X>>), List20_2(X,Box<List20<X>>), List20_3(X,Box<List20<X>>), List20_4(X,Box<List20<X>>), List20_5(X,Box<List20<X>>), List20_6(X,Box<List20<X>>), List20_7(X,Box<List20<X>>), List20_8(X,Box<List20<X>>), List20_9(X,Box<List20<X>>), List20_10(X,Box<List20<X>>), List20_11(X,Box<List20<X>>), List20_12(X,Box<List20<X>>), List20_13(X,Box<List20<X>>), List20_14(X,Box<List20<X>>), List20_15(X,Box<List20<X>>), List20_16(X,Box<List20<X>>), List20_17(X,Box<List20<X>>), List20_18(X,Box<List20<X>>), List20_19(X,Box<List20<X>>), }";
 
 
 /***
@@ -158,6 +166,15 @@ str_struct_new <- heapster_find_symbol env "9StrStruct3new";
 // FIXME: this is the correct version, with the String shape
 heapster_typecheck_fun_rename env str_struct_new "str_struct_new" "(len:bv 64).arg0:memblock(W,0,24,emptysh), arg1:array(0,<len,*1,[(R,0,8) |-> int8<>]), arg2:eq(llvmword(len)) -o arg0:memblock(W,0,24,String<>)";
 
+enum20_list_proj_sym <- heapster_find_symbol env "16enum20_list_proj";
+//heapster_typecheck_fun_rename env enum20_list_proj_sym "enum20_list_proj" "<'a> fn (x:&'a Enum20<List<u64>>) -> &'a List<u64>";
+
+list10_head_sym <- heapster_find_symbol env "11list10_head";
+//heapster_typecheck_fun_rename env list10_head_sym "list10_head" "<'a> fn (x:&'a List10<List<u64>>) -> &'a List<u64>";
+
+list20_head_sym <- heapster_find_symbol env "11list20_head";
+heapster_typecheck_fun_rename env list20_head_sym "list20_head" "<'a> fn (x:&'a List20<List<u64>>) -> &'a List<u64>";
+
 
 /***
  *** Export to Coq

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -2165,6 +2165,9 @@ simplImplOut (SImpl_NamedArgRead x npn args off memb) =
 simplImplOut (SImpl_ReachabilityTrans x rp args off _ e) =
   distPerms1 x (ValPerm_Named (recPermName rp) (PExprs_Cons args e) off)
 
+-- | Compute the output permissions of a 'SimplImpl' implication in a binding
+mbSimplImplOut :: Mb ctx (SimplImpl ps_in ps_out) -> Mb ctx (DistPerms ps_out)
+mbSimplImplOut = mbMapCl $(mkClosed [| simplImplOut |])
 
 -- | Apply a 'SimplImpl' implication to the permissions on the top of a
 -- permission set stack, checking that they equal the 'simplImplIn' of the

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -4864,7 +4864,7 @@ noExprsInTypeCtx (Member_Step ctx) = noExprsInTypeCtx ctx
 -- | Defines a substitution type @s@ that supports substituting into expression
 -- and permission variables in a given monad @m@
 class MonadBind m => SubstVar s m | s -> m where
-  -- extSubst :: s ctx -> ExprVar a -> s (ctx :> a)
+  extSubst :: s ctx -> ExprVar a -> s (ctx :> a)
   substExprVar :: s ctx -> Mb ctx (ExprVar a) -> m (PermExpr a)
 
 substPermVar :: SubstVar s m => s ctx -> Mb ctx (PermVar a) -> m (ValuePerm a)
@@ -4874,8 +4874,17 @@ substPermVar s mb_x =
     PExpr_Var x -> return $ ValPerm_Var x NoPermOffset
     PExpr_ValPerm p -> return p
 
+-- | Extend a substitution with 0 or more variables
+extSubstMulti :: SubstVar s m => s ctx -> RAssign ExprVar ctx' ->
+                 s (ctx :++: ctx')
+extSubstMulti s MNil = s
+extSubstMulti s (xs :>: x) = extSubst (extSubstMulti s xs) x
+
 -- | Generalized notion of substitution, which says that substitution type @s@
 -- supports substituting into type @a@ in monad @m@
+--
+-- FIXME: the 'Mb' argument should really be a 'MatchedMb', to emphasize that we
+-- expect it to be in fresh pair form
 class SubstVar s m => Substable s a m where
   genSubst :: s ctx -> Mb ctx a -> m a
 
@@ -4893,44 +4902,47 @@ instance (NuMatching a, Substable s a m) => Substable s (NonEmpty a) m where
   genSubst s (mbMatch -> [nuMP| x :| xs |]) =
     (:|) <$> genSubst s x <*> genSubst s xs
 
-instance (Substable s a m, Substable s b m) => Substable s (a,b) m where
-  genSubst s ab = (,) <$> genSubst s (fmap fst ab) <*> genSubst s (fmap snd ab)
+instance (NuMatching a, NuMatching b,
+          Substable s a m, Substable s b m) => Substable s (a,b) m where
+  genSubst s [nuP| (a,b) |] = (,) <$> genSubst s a <*> genSubst s b
 
-instance (Substable s a m,
+instance (NuMatching a, NuMatching b, NuMatching c, Substable s a m,
           Substable s b m, Substable s c m) => Substable s (a,b,c) m where
-  genSubst s abc =
-    (,,) <$> genSubst s (fmap (\(a,_,_) -> a) abc)
-    <*> genSubst s (fmap (\(_,b,_) -> b) abc)
-    <*> genSubst s (fmap (\(_,_,c) -> c) abc)
+  genSubst s [nuP| (a,b,c) |] =
+    (,,) <$> genSubst s a <*> genSubst s b <*> genSubst s c
 
-instance (Substable s a m, Substable s b m,
+instance (NuMatching a, NuMatching b, NuMatching c, NuMatching d,
+          Substable s a m, Substable s b m,
           Substable s c m, Substable s d m) => Substable s (a,b,c,d) m where
-  genSubst s abcd =
-    (,,,) <$> genSubst s (fmap (\(a,_,_,_) -> a) abcd)
-          <*> genSubst s (fmap (\(_,b,_,_) -> b) abcd)
-          <*> genSubst s (fmap (\(_,_,c,_) -> c) abcd)
-          <*> genSubst s (fmap (\(_,_,_,d) -> d) abcd)
+  genSubst s [nuP| (a,b,c,d) |] =
+    (,,,) <$> genSubst s a <*> genSubst s b <*> genSubst s c <*> genSubst s d
 
 instance (NuMatching a, Substable s a m) => Substable s (Maybe a) m where
   genSubst s mb_x = case mbMatch mb_x of
     [nuMP| Just a |] -> Just <$> genSubst s a
     [nuMP| Nothing |] -> return Nothing
 
-instance {-# INCOHERENT #-} (Given (RAssign Proxy ctx), Substable s a m, NuMatching a) => Substable s (Mb ctx a) m where
-   genSubst = genSubstMb given
+instance {-# INCOHERENT #-} (Given (RAssign Proxy (ctx :: RList CrucibleType)),
+                             Substable s a m, NuMatching a) =>
+                            Substable s (Mb ctx a) m where
+  genSubst = genSubstMb given
 
-instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Mb RNil a) m where
-   genSubst = genSubstMb RL.typeCtxProxies
+instance {-# INCOHERENT #-}
+  (Substable s a m, NuMatching a) =>
+  Substable s (Mb (RNil :: RList CrucibleType) a) m where
+  genSubst = genSubstMb RL.typeCtxProxies
 
-instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Binding c a) m where
-   genSubst = genSubstMb RL.typeCtxProxies
+instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) =>
+                            Substable s (Binding (c :: CrucibleType) a) m where
+  genSubst = genSubstMb RL.typeCtxProxies
 
 genSubstMb ::
   Substable s a m =>
   NuMatching a =>
-  RAssign Proxy ctx ->
+  RAssign Proxy (ctx :: RList CrucibleType) ->
   s ctx' -> Mb ctx' (Mb ctx a) -> m (Mb ctx a)
-genSubstMb p s mbmb = mbM (fmap (genSubst s) (mbSwap p mbmb))
+genSubstMb p s mbmb =
+  mbM $ nuMulti p $ \ns -> genSubst (extSubstMulti s ns) (mbCombine p mbmb)
 
 instance SubstVar s m => Substable s (Member ctx a) m where
   genSubst _ mb_memb = return $ mbLift mb_memb
@@ -5278,7 +5290,7 @@ noPermsInCruCtx (Member_Step ctx) = noPermsInCruCtx ctx
 -- No case for Member_Base
 
 instance SubstVar PermSubst Identity where
-  -- extSubst (PermSubst elems) x = PermSubst $ elems :>: PExpr_Var x
+  extSubst (PermSubst elems) x = PermSubst $ elems :>: PExpr_Var x
   substExprVar s x =
     case mbNameBoundP x of
       Left memb -> return $ substLookup s memb
@@ -5352,7 +5364,7 @@ varSubstVar s mb_x =
     Right x -> x
 
 instance SubstVar PermVarSubst Identity where
-  -- extSubst (PermVarSubst elems) x = PermVarSubst $ elems :>: x
+  extSubst s x = PermVarSubst_Cons s x
   substExprVar s x =
     case mbNameBoundP x of
       Left memb -> return $ PExpr_Var $ varSubstLookup s memb
@@ -5467,9 +5479,8 @@ psubstAppend (PartialSubst elems1) (PartialSubst elems2) =
   PartialSubst $ RL.append elems1 elems2
 
 instance SubstVar PartialSubst Maybe where
-  {-
   extSubst (PartialSubst elems) x =
-    PartialSubst $ elems :>: PSubstElem (Just $ PExpr_Var x) -}
+    PartialSubst $ elems :>: PSubstElem (Just $ PExpr_Var x)
   substExprVar s x =
     case mbNameBoundP x of
       Left memb -> psubstLookup s memb