From 12e1d87954fb32130e766d7b29cb3390d06507a4 Mon Sep 17 00:00:00 2001
From: Alexander Bakst <abakst@galois.com>
Date: Fri, 29 Apr 2022 13:44:11 -0700
Subject: [PATCH] Try solving for array lifetime/rw modality.

---
 .../src/Verifier/SAW/Heapster/Implication.hs  | 42 +++++++++++++++++++
 .../src/Verifier/SAW/Heapster/Permissions.hs  |  7 ++++
 2 files changed, 49 insertions(+)

diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index c8d07edea6..acdb6a9df6 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -6606,6 +6606,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
@@ -6701,6 +6737,12 @@ proveVarLLVMArrayH x p psubst ps mb_ap
 -- 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
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index c60bb5cfdb..f4af7ac63a 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -4058,6 +4058,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) ->