Generalized Heapster lifetime ownership permissions

heapster-saw/examples/rust_data.rs

@@ -421,6 +421,14 @@ pub fn list64_sum(l:&List64) -> u64 {
     }
 }
 
+/* Return a mutable reference to the head of a list, or None if it is empty */
+pub fn list64_head_mut <'a> (l:&'a mut List64) -> Option<&'a mut u64> {
+    match l {
+        List64::Nil64 => None,
+        List64::Cons64 (h,_) => Some (h),
+    }
+}
+
 /* Find an element in a List64 and return a mutable reference to it */
 pub fn list64_find_mut <'a> (x:u64, l:&'a mut List64) -> Option<&'a mut u64> {
     match l {

heapster-saw/examples/rust_data.saw

@@ -596,6 +596,17 @@ list64_tail_sym <- heapster_find_symbol env "11list64_tail";
 heapster_typecheck_fun_rename env list64_tail_sym "list64_tail"
   "<> fn (l:List64) -> Option<List64>";
 
+// list64_head_mut
+list64_head_mut_sym <- heapster_find_symbol env "15list64_head_mut";
+heapster_typecheck_fun_rename env list64_head_mut_sym "list64_head_mut"
+  "<'a> fn (l:&'a mut List64) -> Option<&'a mut u64>";
+
+// list64_find_mut
+list64_find_mut_sym <- heapster_find_symbol env "15list64_find_mut";
+heapster_typecheck_fun_rename env list64_find_mut_sym "list64_find_mut"
+  "<'a> fn (x:u64, l:&'a mut List64) -> Option<&'a mut u64>";
+
+/*
 hash_map_insert_gt_to_le_sym <- heapster_find_symbol env "hash_map_insert_gt_to_le";
 heapster_typecheck_fun_rename
   env hash_map_insert_gt_to_le_sym
@@ -628,6 +639,7 @@ heapster_set_translation_checks env false;
 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>";
+*/
 
 
 /***

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

@@ -749,6 +749,19 @@ cruCtxReplicate n tp =
       | Some ctx <- cruCtxReplicate (predNat n) tp
       -> Some (CruCtxCons ctx tp)
 
+-- | A representation of a context of types as a sequence of 'KnownRepr'
+-- instances
+--
+-- FIXME: this can go away when existentials take explicit 'TypeRepr's instead
+-- of 'KnownRepr TypeRepr' instances, as per issue #79
+type KnownCruCtx = RAssign (KnownReprObj TypeRepr)
+
+-- | Convert a 'KnownCruCtx' to a 'CruCtx'
+knownCtxToCruCtx :: KnownCruCtx ctx -> CruCtx ctx
+knownCtxToCruCtx MNil = CruCtxNil
+knownCtxToCruCtx (ctx :>: KnownReprObj) =
+  CruCtxCons (knownCtxToCruCtx ctx) knownRepr
+
 
 ----------------------------------------------------------------------
 -- * Misc Operations on Crucible Objects

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

@@ -154,8 +154,8 @@ instance ContainsIRTRecName (AtomicPerm a) where
   containsIRTRecName n (Perm_NamedConj _ args _) = containsIRTRecName n args
   containsIRTRecName n (Perm_LLVMFrame fperm) =
     containsIRTRecName n (map fst fperm)
-  containsIRTRecName _ (Perm_LOwned _ _ _) = False
-  containsIRTRecName _ (Perm_LOwnedSimple _) = False
+  containsIRTRecName _ (Perm_LOwned _ _ _ _ _) = False
+  containsIRTRecName _ (Perm_LOwnedSimple _ _) = False
   containsIRTRecName _ (Perm_LCurrent _) = False
   containsIRTRecName _ Perm_LFinished = False
   containsIRTRecName n (Perm_Struct ps) = containsIRTRecName n ps
@@ -414,9 +414,9 @@ instance IRTTyVars (AtomicPerm a) where
     [nuMP| Perm_NamedConj npn args off |] ->
       namedPermIRTTyVars mb_p npn args off
     [nuMP| Perm_LLVMFrame _ |] -> return ([], IRTVarsNil)
-    [nuMP| Perm_LOwned _ _ _ |] ->
+    [nuMP| Perm_LOwned _ _ _ _ _ |] ->
       throwError "lowned permission in an IRT definition!"
-    [nuMP| Perm_LOwnedSimple _ |] ->
+    [nuMP| Perm_LOwnedSimple _ _ |] ->
       throwError "lowned permission in an IRT definition!"
     [nuMP| Perm_LCurrent _ |] -> return ([], IRTVarsNil)
     [nuMP| Perm_LFinished |] -> return ([], IRTVarsNil)
@@ -664,9 +664,9 @@ instance IRTDescs (AtomicPerm a) where
     ([nuMP| Perm_NamedConj npn args off |], _) ->
       namedPermIRTDescs npn args off ixs
     ([nuMP| Perm_LLVMFrame _ |], _) -> return []
-    ([nuMP| Perm_LOwned _ _ _ |], _) ->
+    ([nuMP| Perm_LOwned _ _ _ _ _ |], _) ->
       error "lowned permission made it to IRTDesc translation"
-    ([nuMP| Perm_LOwnedSimple _ |], _) ->
+    ([nuMP| Perm_LOwnedSimple _ _ |], _) ->
       error "lowned permission made it to IRTDesc translation"
     ([nuMP| Perm_LCurrent _ |], _) -> return []
     ([nuMP| Perm_LFinished |], _) -> return []