check borrow equality in suitableAP, update sha512_mr_solver.saw

Author: m-yac

heapster-saw/examples/sha512_mr_solver.saw

@@ -28,7 +28,7 @@ heapster_typecheck_fun env "round_16_80"
     \ arg2:int64_ptr<>, arg3:int64_ptr<>, arg4:int64_ptr<>, arg5:int64_ptr<>, \
     \ arg6:int64_ptr<>, arg7:int64_ptr<>, arg8:int64_ptr<>, arg9:int64_ptr<>, \
     \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \
-    \ arg11:int64_ptr<>, arg12:int64_ptr<>, arg13:int64_ptr<> -o \
+    \ arg11:ptr((W,0) |-> true), arg12:ptr((W,0) |-> true), arg13:int64_ptr<> -o \
     \ arg2:int64_ptr<>, arg3:int64_ptr<>, arg4:int64_ptr<>, arg5:int64_ptr<>, \
     \ arg6:int64_ptr<>, arg7:int64_ptr<>, arg8:int64_ptr<>, arg9:int64_ptr<>, \
     \ arg10:array(W,0,<16,*8,fieldsh(int64<>)), \
@@ -38,8 +38,6 @@ heapster_typecheck_fun env "return_X"
   "(). arg0:array(W,0,<16,*8,fieldsh(int64<>)) -o \
      \ arg0:array(W,0,<16,*8,fieldsh(int64<>))";
 
-heapster_set_debug_level env 1;
-
 heapster_set_translation_checks env false;
 heapster_typecheck_fun env "processBlock"
   "(num:bv 64). arg0:int64_ptr<>, arg1:int64_ptr<>, arg2:int64_ptr<>, \
@@ -51,9 +49,7 @@ heapster_typecheck_fun env "processBlock"
               \ arg6:int64_ptr<>, arg7:int64_ptr<>, \
               \ arg8:array(R,0,<16*num,*8,fieldsh(int64<>)), ret:true";
 
-heapster_export_coq env "sha512_mr_solver_gen.v";
-
-/*
+// FIXME: This translation contains errors
 heapster_set_translation_checks env false;
 heapster_typecheck_fun env "processBlocks"
   "(num:bv 64). arg0:array(W,0,<8,*8,fieldsh(int64<>)), \
@@ -63,6 +59,8 @@ heapster_typecheck_fun env "processBlocks"
               \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \
               \ arg2:true, ret:true";
 
+heapster_export_coq env "sha512_mr_solver_gen.v";
+
 // Mr. Solver
 
 let eq_bool b1 b2 =
@@ -81,13 +79,14 @@ let run_test name test expected =
 
 round_00_15 <- parse_core_mod "SHA512" "round_00_15";
 round_16_80 <- parse_core_mod "SHA512" "round_16_80";
-// processBlock <- parse_core_mod "SHA512" "processBlock";
-// processBlocks <- parse_core_mod "SHA512" "processBlocks";
+processBlock <- parse_core_mod "SHA512" "processBlock";
+processBlocks <- parse_core_mod "SHA512" "processBlocks";
 
 // Test that every function refines itself
-// run_test "processBlocks |= processBlocks" (mr_solver processBlocks processBlocks) true;
+run_test "processBlocks |= processBlocks" (mr_solver processBlocks processBlocks) true;
+// FIXME: Why does this hang?
 // run_test "processBlock |= processBlock" (mr_solver processBlock processBlock) true;
-// run_test "round_16_80 |= round_16_80" (mr_solver round_16_80 round_16_80) true;
+run_test "round_16_80 |= round_16_80" (mr_solver round_16_80 round_16_80) true;
 // run_test "round_00_15 |= round_00_15" (mr_solver round_00_15 round_00_15) true;
 
 import "sha512.cry";
@@ -105,5 +104,6 @@ monadify_term {{ Maj }};
 monadify_term {{ round_00_15_spec }};
 
 run_test "round_00_15 |= round_00_15_spec" (mr_solver round_00_15 {{ round_00_15_spec }}) true;
-run_test "round_16_80 |= round_16_80_spec" (mr_solver_debug 0 round_16_80 {{ round_16_80_spec }}) true;
-*/
+
+// FIXME: Need to add heterogenous equality on output types for this to work
+// run_test "round_16_80 |= round_16_80_spec" (mr_solver_debug 0 round_16_80 {{ round_16_80_spec }}) true;

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

@@ -6734,15 +6734,16 @@ proveVarLLVMArrayH x psubst ps mb_ap
   , Just len <- partialSubst psubst $ mbLLVMArrayLen mb_ap
   , Just lenBytes <- partialSubst psubst $ mbLLVMArrayLenBytes mb_ap
   , stride <- mbLLVMArrayStride mb_ap
-  , Just i   <- findIndex (suitableAP off lenBytes stride) ps
+  , Just bs  <- partialSubst psubst $ mbLLVMArrayBorrows mb_ap
+  , Just i   <- findIndex (suitableAP off lenBytes stride bs) ps
   , Perm_LLVMArray ap_lhs <- ps!!i =
     implVerbTraceM (\info -> pretty "proveVarLLVMArrayH case 1: using" <+>
                              permPretty info ap_lhs) >>>
     implGetConjM x ps i >>>= \ps' ->
     recombinePerm x (ValPerm_Conj ps') >>>
 
     partialSubstForceM (mbLLVMArrayBorrows mb_ap)
-    "proveVarLLVMArrayH: incomplete array borrows" >>>= \bs ->
+    "proveVarLLVMArrayH: incomplete array borrows" >>>
 
     if bvEq off (llvmArrayOffset ap_lhs) && bvEq len (llvmArrayLen ap_lhs) then
       proveVarLLVMArray_FromArray x ap_lhs len bs mb_ap
@@ -6752,22 +6753,26 @@ proveVarLLVMArrayH x psubst ps mb_ap
       proveVarLLVMArray_FromArray x (llvmMakeSubArray ap_lhs off len) len bs mb_ap
   where
     -- Test if an atomic permission is a "suitable" array permission for the
-    -- given offset, length, and stride, meaning that it has the required
-    -- stride, could contain the offset and length, and does not have all of the
-    -- offset and length borrowed
+    -- given offset, length, stride, and borrows, meaning that it has the
+    -- given stride, could contain the given offset and length, and either
+    -- has exactly the given borrows or at least does not have all of the
+    -- given offset and length borrowed
     suitableAP ::
       (1 <= w, KnownNat w) =>
       PermExpr (BVType w) -> PermExpr (BVType w) -> Bytes ->
-      AtomicPerm (LLVMPointerType w) -> Bool
-    suitableAP off len stride (Perm_LLVMArray ap) =
+      [LLVMArrayBorrow w] -> AtomicPerm (LLVMPointerType w) -> Bool
+    suitableAP off len stride bs (Perm_LLVMArray ap) =
       -- Test that the strides are equal
       llvmArrayStride ap == stride &&
-      -- Make sure the range [off,len) is not fully borrowed
-      not (llvmArrayRangeIsBorrowed ap (BVRange off len)) &&
       -- Test if this permission *could* cover the desired off/len
       all bvPropCouldHold (bvPropRangeSubset (BVRange off len)
-                                             (llvmArrayAbsOffsets ap))
-    suitableAP _ _ _ _ = False
+                                             (llvmArrayAbsOffsets ap)) &&
+      -- Test that either the sets of borrows are equal ...
+      (all (flip elem bs) (llvmArrayBorrows ap) &&
+       all (flip elem (llvmArrayBorrows ap)) bs) ||
+      -- ...or the range [off,len) is not fully borrowed
+      not (llvmArrayRangeIsBorrowed ap (BVRange off len))
+    suitableAP _ _ _ _ _ = False
 
 -- Check if there is a block that contains the required offset and length, in
 -- which case eliminate it, allowing us to either satisfy way 4 (eliminate a
@@ -6809,8 +6814,8 @@ proveVarLLVMArrayH x psubst ps mb_ap
   , len <- llvmArrayLen ap
   , lhs_cells@(lhs_cell_rng:_) <- concatMap (permCells ap) ps
   , rhs_cells <- map llvmArrayBorrowCells (llvmArrayBorrows ap)
-  , Just cells <- gatherCoveringRanges (llvmArrayCells ap) (lhs_cells ++
-                                                            rhs_cells)
+  , Just cells <- gatherCoveringRanges (llvmArrayCells ap) (rhs_cells ++
+                                                            lhs_cells)
   , bs <- map cellRangeToBorrow cells
   , ap_borrowed <- ap { llvmArrayBorrows = bs }
   , cell_bp <- blockForCell ap (bvRangeOffset lhs_cell_rng) =