validForDeref_ptrval w/o provenance

rems-project · Jul 20, 2023 · 8be9579 · 8be9579
1 parent 64bcb78
commit 8be9579
Showing 1 changed file with 17 additions and 7 deletions.
diff --git a/coq/CheriMemory/CheriMemory.v b/coq/CheriMemory/CheriMemory.v
@@ -2814,13 +2814,12 @@ Module CheriMemory
     match ptrval with
     | PV _ (PVfunction _) => ret false
     | (PV Prov_device (PVconcrete c_value)) as ptrval =>
-        if cap_is_null c_value then
-          ret false
-        else
-          isWellAligned_ptrval ref_ty ptrval
+        if cap_is_null c_value
+        then ret false
+        else isWellAligned_ptrval ref_ty ptrval
     | PV (Prov_symbolic iota) (PVconcrete c_value) =>
-        if cap_is_null c_value then
-          ret false
+        if cap_is_null c_value
+        then ret false
         else
           lookup_iota iota >>=
             (fun x =>
@@ -2837,7 +2836,18 @@ Module CheriMemory
         if cap_is_null c_value
         then ret false
         else do_test alloc_id
-    | PV Prov_none _ => ret false
+    | PV Prov_none (PVconcrete c_value) =>
+        if CoqSwitches.is_PNVI (SW.get_switches tt)
+        then ret false
+        else if cap_is_null c_value
+             then ret false
+             else
+               find_overlaping (cap_to_Z c_value) >>= fun x =>
+                   match x with
+                   | NoAlloc => fail Loc_unknown (MerrAccess LoadAccess OutOfBoundPtr)
+                   | DoubleAlloc _ _ => fail Loc_unknown (MerrInternal "DoubleAlloc without PNVI")
+                   | SingleAlloc alloc_id => isWellAligned_ptrval ref_ty ptrval
+                   end
     end.
 
   Definition add_iota