get round round_16_80 typechecking

Author: m-yac

heapster-saw/examples/sha512_mr_solver.saw

@@ -23,7 +23,7 @@ heapster_typecheck_fun env "round_00_15"
     \ arg5:int64_ptr<>, arg6:int64_ptr<>, arg7:int64_ptr<>, arg8:int64_ptr<>, \
     \ arg9:int64_ptr<>, ret:true";
 
-heapster_set_debug_level env 1;
+// heapster_set_debug_level env 1;
 
 heapster_typecheck_fun env "round_16_80"
  "(). arg0:int64<>, arg1:int64<>, \
@@ -39,10 +39,14 @@ heapster_typecheck_fun env "round_16_80"
 /*
 heapster_set_translation_checks env false;
 heapster_typecheck_fun env "processBlock"
-  "(num:bv 64). arg0:array(W,0,<8,*8,fieldsh(int64<>)), \
-              \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)) -o \
-              \ arg0:array(W,0,<8,*8,fieldsh(int64<>)), \
-              \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), ret:true";
+  "(num:bv 64). arg0:int64_ptr<>, arg1:int64_ptr<>, arg2:int64_ptr<>, \
+              \ arg3:int64_ptr<>, arg4:int64_ptr<>, arg5:int64_ptr<>, \
+              \ arg6:int64_ptr<>, arg7:int64_ptr<>, \
+              \ arg8:array(R,0,<16*num,*8,fieldsh(int64<>)) -o \
+              \ arg0:int64_ptr<>, arg1:int64_ptr<>, arg2:int64_ptr<>, \
+              \ arg3:int64_ptr<>, arg4:int64_ptr<>, arg5:int64_ptr<>, \
+              \ arg6:int64_ptr<>, arg7:int64_ptr<>, \
+              \ arg8:array(R,0,<16*num,*8,fieldsh(int64<>)), ret:true";
 
 heapster_set_translation_checks env false;
 heapster_typecheck_fun env "processBlocks"
@@ -52,6 +56,7 @@ heapster_typecheck_fun env "processBlocks"
               \ arg0:array(W,0,<8,*8,fieldsh(int64<>)), \
               \ arg1:array(R,0,<16*num,*8,fieldsh(int64<>)), \
               \ arg2:true, ret:true";
+*/
 
 heapster_export_coq env "sha512_mr_solver_gen.v";
 
@@ -73,12 +78,12 @@ 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 "processBlock |= processBlock" (mr_solver processBlock processBlock) true;
+// run_test "processBlocks |= processBlocks" (mr_solver processBlocks processBlocks) true;
+// 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_00_15 |= round_00_15" (mr_solver round_00_15 round_00_15) true;
 
@@ -98,4 +103,3 @@ 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;
-*/

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

@@ -8040,10 +8040,14 @@ detVarsClauseAddLHSVar :: ExprVar a -> DetVarsClause -> DetVarsClause
 detVarsClauseAddLHSVar n (DetVarsClause lhs rhs) =
   DetVarsClause (NameSet.insert n lhs) rhs
 
+newtype SeenDetVarsClauses :: CrucibleType -> * where
+  SeenDetVarsClauses :: [DetVarsClause] -> SeenDetVarsClauses tp
+
 -- | Generic function to compute the 'DetVarsClause's for a permission
 class GetDetVarsClauses a where
   getDetVarsClauses ::
-    a -> ReaderT (PermSet ps) (State (NameSet CrucibleType)) [DetVarsClause]
+    a -> ReaderT (PermSet ps) (State (NameMap SeenDetVarsClauses))
+                              [DetVarsClause]
 
 instance GetDetVarsClauses a => GetDetVarsClauses [a] where
   getDetVarsClauses l = concat <$> mapM getDetVarsClauses l
@@ -8055,11 +8059,13 @@ instance GetDetVarsClauses (ExprVar a) where
   getDetVarsClauses x =
     do seen_vars <- get
        perms <- ask
-       if NameSet.member x seen_vars then return [] else
-         do modify (NameSet.insert x)
-            perm_clauses <- getDetVarsClauses (perms ^. varPerm x)
-            return (DetVarsClause NameSet.empty (SomeName x) :
-                    map (detVarsClauseAddLHSVar x) perm_clauses)
+       perm_clauses <- case NameMap.lookup x seen_vars of
+         Just (SeenDetVarsClauses perm_clauses) -> return perm_clauses
+         Nothing -> do perm_clauses <- getDetVarsClauses (perms ^. varPerm x)
+                       modify (NameMap.insert x (SeenDetVarsClauses perm_clauses))
+                       return perm_clauses
+       return (DetVarsClause NameSet.empty (SomeName x) :
+               map (detVarsClauseAddLHSVar x) perm_clauses)
 
 instance GetDetVarsClauses (PermExpr a) where
   getDetVarsClauses e
@@ -8131,7 +8137,7 @@ instance GetDetVarsClauses (LLVMFieldShape w) where
 -- | Compute the 'DetVarsClause's for a block permission with the given shape
 getShapeDetVarsClauses ::
   (1 <= w, KnownNat w) => PermExpr (LLVMShapeType w) ->
-  ReaderT (PermSet ps) (State (NameSet CrucibleType)) [DetVarsClause]
+  ReaderT (PermSet ps) (State (NameMap SeenDetVarsClauses)) [DetVarsClause]
 getShapeDetVarsClauses (PExpr_Var x) =
   getDetVarsClauses x
 getShapeDetVarsClauses (PExpr_NamedShape _ _ _ args) =
@@ -8157,20 +8163,23 @@ getShapeDetVarsClauses _ = return []
 -- is always a uniquely determined value of @y@ for any proof of @exists y.x:p@.
 determinedVars :: PermSet ps -> RAssign ExprVar ns -> [SomeName CrucibleType]
 determinedVars top_perms vars =
-  let vars_set = NameSet.fromList $ mapToList SomeName vars
+  let vars_map = NameMap.fromList $
+        mapToList (\v -> NameAndElem v (SeenDetVarsClauses [])) vars
+      vars_set = NameSet.fromList $ mapToList SomeName vars
       multigraph =
         evalState (runReaderT (getDetVarsClauses (distPermsToValuePerms $
                                                   varPermsMulti vars top_perms))
                    top_perms)
-        vars_set in
+        vars_map in
   evalState (determinedVarsForGraph multigraph) vars_set
   where
     -- Find all variables that are not already marked as determined in our
     -- NameSet state but that are determined given the current determined
-    -- variables, mark these variables as determiend, and then repeat, returning
+    -- variables, mark these variables as determined, and then repeat, returning
     -- all variables that are found in order
     determinedVarsForGraph :: [DetVarsClause] ->
-                              State (NameSet CrucibleType) [SomeName CrucibleType]
+                              State (NameSet CrucibleType)
+                                    [SomeName CrucibleType]
     determinedVarsForGraph graph =
       do det_vars <- concat <$> mapM determinedVarsForClause graph
          if det_vars == [] then return [] else
@@ -8179,7 +8188,8 @@ determinedVars top_perms vars =
     -- If the LHS of a clause has become determined but its RHS is not, return
     -- its RHS, otherwise return nothing
     determinedVarsForClause :: DetVarsClause ->
-                               State (NameSet CrucibleType) [SomeName CrucibleType]
+                               State (NameSet CrucibleType)
+                                     [SomeName CrucibleType]
     determinedVarsForClause (DetVarsClause lhs_vars (SomeName rhs_var)) =
       do det_vars <- get
          if not (NameSet.member rhs_var det_vars) &&