New flag for only processing loop contracts

SaswatPadhi · SaswatPadhi · commit 9cdca480ed91 · 2021-06-22T17:36:01.000Z
Added `--apply-loop-contracts` to check and use loop contracts
(invariants and variants) independent of function contracts.
diff --git a/regression/contracts/invar_check_break_fail/test.desc b/regression/contracts/invar_check_break_fail/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_break_pass/test.desc b/regression/contracts/invar_check_break_pass/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_continue/test.desc b/regression/contracts/invar_check_continue/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_large/test.desc b/regression/contracts/invar_check_large/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_multiple_loops/test.desc b/regression/contracts/invar_check_multiple_loops/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_pointer_modifies-01/test.desc b/regression/contracts/invar_check_pointer_modifies-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts --pointer-check
+--apply-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_pointer_modifies-02/test.desc b/regression/contracts/invar_check_pointer_modifies-02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts --pointer-check
+--apply-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_check_sufficiency/test.desc b/regression/contracts/invar_check_sufficiency/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_dynamic_struct_member/test.desc b/regression/contracts/invar_dynamic_struct_member/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_array/test.desc b/regression/contracts/invar_havoc_dynamic_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_array/test.desc b/regression/contracts/invar_havoc_static_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_array_const_idx/test.desc b/regression/contracts/invar_havoc_static_array_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_loop_constant_fail/test.desc b/regression/contracts/invar_loop_constant_fail/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_loop_constant_no_modify/test.desc b/regression/contracts/invar_loop_constant_no_modify/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_loop_constant_pass/test.desc b/regression/contracts/invar_loop_constant_pass/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invar_struct_member/test.desc b/regression/contracts/invar_struct_member/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/invariant_side_effects/test.desc b/regression/contracts/invariant_side_effects/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
diff --git a/regression/contracts/quantifiers-loop-01/test.desc b/regression/contracts/quantifiers-loop-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] line .* Check loop invariant before entry: SUCCESS
diff --git a/regression/contracts/quantifiers-loop-02/test.desc b/regression/contracts/quantifiers-loop-02/test.desc
@@ -1,6 +1,6 @@
-CORE
+CORE smt-backend
 main.c
---enforce-all-contracts _ --z3
+--apply-loop-contracts _ --z3
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS
diff --git a/regression/contracts/quantifiers-loop-03/test.desc b/regression/contracts/quantifiers-loop-03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] line .* Check loop invariant before entry: SUCCESS
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
@@ -1186,6 +1186,12 @@ bool code_contractst::replace_calls(
   return false;
 }
 
+void code_contractst::apply_loop_contracts()
+{
+  for(auto &goto_function : goto_functions.function_map)
+    apply_loop_contract(goto_function.first, goto_function.second);
+}
+
 bool code_contractst::replace_calls()
 {
   std::set<std::string> funs_to_replace;
@@ -1204,8 +1210,6 @@ bool code_contractst::enforce_contracts()
   {
     if(has_contract(goto_function.first))
       funs_to_enforce.insert(id2string(goto_function.first));
-    else
-      apply_loop_contract(goto_function.first, goto_function.second);
   }
   return enforce_contracts(funs_to_enforce);
 }
@@ -1225,7 +1229,6 @@ bool code_contractst::enforce_contracts(
                   << messaget::eom;
       continue;
     }
-    apply_loop_contract(goto_function->first, goto_function->second);
 
     if(!has_contract(fun))
     {
diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h
@@ -90,6 +90,8 @@ class code_contractst
   /// \return `true` on failure, `false` otherwise
   bool replace_calls();
 
+  void apply_loop_contracts();
+
   const symbolt &new_tmp_symbol(
     const typet &type,
     const source_locationt &source_location,
@@ -216,6 +218,11 @@ class code_contractst
     const irep_idt &mode);
 };
 
+#define FLAG_LOOP_CONTRACTS "apply-loop-contracts"
+#define HELP_LOOP_CONTRACTS                                                    \
+  " --apply-loop-contracts\n"                                                  \
+  "                              check and use loop contracts when provided\n"
+
 #define FLAG_REPLACE_CALL "replace-call-with-contract"
 #define HELP_REPLACE_CALL                                                      \
   " --replace-call-with-contract <fun>\n"                                      \
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1149,7 +1149,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   }
 
   if(
-    cmdline.isset(FLAG_REPLACE_CALL) || cmdline.isset(FLAG_REPLACE_ALL_CALLS) ||
+    cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) ||
+    cmdline.isset(FLAG_REPLACE_ALL_CALLS) ||
     cmdline.isset(FLAG_ENFORCE_CONTRACT) ||
     cmdline.isset(FLAG_ENFORCE_ALL_CONTRACTS))
   {
@@ -1180,6 +1181,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     if(cmdline.isset(FLAG_ENFORCE_ALL_CONTRACTS))
       if(cont.enforce_contracts())
         exit(CPROVER_EXIT_USAGE_ERROR);
+
+    if(cmdline.isset(FLAG_LOOP_CONTRACTS))
+      cont.apply_loop_contracts();
   }
 
   if(cmdline.isset("value-set-fi-fp-removal"))
@@ -1868,7 +1872,8 @@ void goto_instrument_parse_optionst::help()
     " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
     HELP_REPLACE_CALLS
     "\n"
-    "Function contracts and invariants:\n"
+    "Code contracts:\n"
+    HELP_LOOP_CONTRACTS
     HELP_REPLACE_CALL
     HELP_REPLACE_ALL_CALLS
     HELP_ENFORCE_CONTRACT
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
@@ -99,6 +99,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
   "(horn)(skip-loops):(model-argc-argv):" \
+  "(" FLAG_LOOP_CONTRACTS ")" \
   "(" FLAG_REPLACE_CALL "):" \
   "(" FLAG_REPLACE_ALL_CALLS ")" \
   "(" FLAG_ENFORCE_CONTRACT "):" \
