Heapster: existential function output perms

heapster-saw/examples/rust_data.saw

@@ -309,8 +309,8 @@ heapster_assume_fun_rename_prim env hashmap_u64_u64_insert_sym "hashmap_u64_u64_
 // String::deref
 string_deref <- heapster_find_trait_method_symbol env
   "core::ops::deref::Deref::deref<String>";
-//heapster_assume_fun_rename_prim env string_deref "string_deref"
-//  "<'a> fn (&'a String) -> &'a str";
+heapster_assume_fun_rename_prim env string_deref "string_deref"
+  "<'a> fn (&'a String) -> &'a str";
 
 // String::fmt
 string_fmt <- heapster_find_trait_method_symbol env

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

@@ -532,8 +532,8 @@ data SimplImpl ps_in ps_out where
   -- > x:eq(handle) -o x:fun_perm
   SImpl_ConstFunPerm ::
     args ~ CtxToRList cargs =>
-    ExprVar (FunctionHandleType cargs ret) ->
-    FnHandle cargs ret -> FunPerm ghosts (CtxToRList cargs) ret -> Ident ->
+    ExprVar (FunctionHandleType cargs ret) -> FnHandle cargs ret ->
+    FunPerm ghosts (CtxToRList cargs) gouts ret -> Ident ->
     SimplImpl (RNil :> FunctionHandleType cargs ret)
     (RNil :> FunctionHandleType cargs ret)
 
@@ -7397,7 +7397,7 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of
     foldr (\(i::Int,p) rest ->
             case p of
               Perm_Fun fun_perm
-                | Just (Refl,Refl,Refl) <- funPermEq3 fun_perm fun_perm' ->
+                | Just (Refl,Refl,Refl,Refl) <- funPermEq4 fun_perm fun_perm' ->
                   implCopyConjM x ps i >>> implPopM x (ValPerm_Conj ps)
               _ -> rest)
     (proveVarAtomicImplUnfoldOrFail x ps mb_p)
@@ -7712,8 +7712,8 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of
     use implStatePermEnv >>>= \env ->
     case lookupFunPerm env f of
       Just (SomeFunPerm fun_perm, ident)
-        | [nuMP| Just (Refl,Refl,Refl) |] <-
-            mbMatch $ fmap (funPermEq3 fun_perm) mb_fun_perm ->
+        | [nuMP| Just (Refl,Refl,Refl, Refl) |] <-
+            mbMatch $ fmap (funPermEq4 fun_perm) mb_fun_perm ->
           introEqCopyM x (PExpr_Fun f) >>>
           implPopM x p >>>
           implSimplM Proxy (SImpl_ConstFunPerm x f fun_perm ident)
@@ -7820,7 +7820,7 @@ distPermsToExDistPerms = emptyMb
 
 -- | Substitute arguments into a function permission to get the existentially
 -- quantified input permissions needed on the arguments
-funPermExDistIns :: FunPerm ghosts args ret -> RAssign Name args ->
+funPermExDistIns :: FunPerm ghosts args gouts ret -> RAssign Name args ->
                     ExDistPerms ghosts (ghosts :++: args)
 funPermExDistIns fun_perm args =
   fmap (varSubst (permVarSubstOfNames args)) $ mbSeparate args $
@@ -8072,6 +8072,16 @@ proveVarsImpl ps
   | Refl <- mbLift (fmap RL.prependRNilEq $ mbDistPermsToValuePerms ps) =
     proveVarsImplAppend ps
 
+-- | Prove a list of existentially-quantified distinguished permissions and put
+-- those proofs onto the stack, and then return the expressions assigned to the
+-- existential variables
+proveVarsImplEVarExprs :: NuMatchingAny1 r => ExDistPerms vars as ->
+                          ImplM vars s r as RNil (PermExprs vars)
+proveVarsImplEVarExprs ps =
+  proveVarsImpl ps >>>
+  use implStateVars >>>= \vars ->
+  fmap (exprsOfSubst . completePSubst vars) getPSubst
+
 -- | Prove a list of existentially-quantified permissions and put the proofs on
 -- the stack, similarly to 'proveVarsImpl', but ensure that the existential
 -- variables are themselves only instanitated with variables, not arbitrary

heapster-saw/src/Verifier/SAW/Heapster/Parser.y

@@ -205,7 +205,9 @@ permOffset ::                                   { Maybe AstExpr         }
 
 funPerm ::                                      { AstFunPerm }
   : '(' ctx ')' '.' funPermList '-o' funPermList
-                                                { AstFunPerm (pos $6) $2 $5 $7 }
+                                                { AstFunPerm (pos $6) $2 $5 [] $7 }
+  | '(' ctx ')' '.' funPermList '-o' '(' ctx ')' '.' funPermList
+                                                { AstFunPerm (pos $6) $2 $5 $8 $11 }
 
 funPermList ::                                  { [(Located String, AstExpr)] }
   : 'empty'                                     { []                    }