New flag for only processing loop contracts

Author: SaswatPadhi

regression/contracts/invar_check_break_fail/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_break_pass/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_continue/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_large/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_multiple_loops/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_nested_loops/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_pointer_modifies-01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts --pointer-check
+--use-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_pointer_modifies-02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts --pointer-check
+--use-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_sufficiency/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_dynamic_struct_member/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_dynamic_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_static_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_static_array_const_idx/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_static_multi-dim_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_loop_constant_fail/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_loop_constant_no_modify/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_loop_constant_pass/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_struct_member/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invariant_side_effects/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/quantifiers-loop-01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] line .* Check loop invariant before entry: SUCCESS

regression/contracts/quantifiers-loop-02/test.desc

@@ -1,6 +1,6 @@
-CORE
+CORE smt-backend
 main.c
---enforce-all-contracts _ --z3
+--use-loop-contracts _ --z3
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS

regression/contracts/quantifiers-loop-03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-all-contracts
+--use-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.1\] line .* Check loop invariant before entry: SUCCESS

src/goto-instrument/code_contracts.cpp

@@ -549,22 +549,23 @@ bool code_contractst::apply_function_contract(
   return false;
 }
 
-void code_contractst::apply_loop_contract(
-  const irep_idt &function_name,
-  goto_functionst::goto_functiont &goto_function)
+void code_contractst::apply_loop_contracts()
 {
-  local_may_aliast local_may_alias(goto_function);
-  natural_loops_mutablet natural_loops(goto_function.body);
+  for(auto &goto_function : goto_functions.function_map)
+  {
+    local_may_aliast local_may_alias(goto_function.second);
+    natural_loops_mutablet natural_loops(goto_function.second.body);
 
-  // Iterate over the (natural) loops in the function,
-  // and apply any invariant annotations that we find.
-  for(const auto &loop : natural_loops.loop_map)
-    check_apply_invariants(
-      goto_function,
-      local_may_alias,
-      loop.first,
-      loop.second,
-      symbol_table.lookup_ref(function_name).mode);
+    // Iterate over the (natural) loops in the function,
+    // and apply any invariant annotations that we find.
+    for(const auto &loop : natural_loops.loop_map)
+      check_apply_invariants(
+        goto_function.second,
+        local_may_alias,
+        loop.first,
+        loop.second,
+        symbol_table.lookup_ref(goto_function.first).mode);
+  }
 }
 
 const symbolt &code_contractst::new_tmp_symbol(
@@ -1204,8 +1205,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 +1224,6 @@ bool code_contractst::enforce_contracts(
                   << messaget::eom;
       continue;
     }
-    apply_loop_contract(goto_function->first, goto_function->second);
 
     if(!has_contract(fun))
     {

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,
@@ -172,10 +174,6 @@ class code_contractst
     const exprt &lhs,
     std::vector<exprt> &aliasable_references);
 
-  void apply_loop_contract(
-    const irep_idt &function_name,
-    goto_functionst::goto_functiont &goto_function);
-
   /// \brief Does the named function have a contract?
   bool has_contract(const irep_idt);
 
@@ -216,6 +214,11 @@ class code_contractst
     const irep_idt &mode);
 };
 
+#define FLAG_LOOP_CONTRACTS "use-loop-contracts"
+#define HELP_LOOP_CONTRACTS                                                    \
+  " --use-loop-contracts\n"                                                    \
+  "                              simplify loops using loop contracts\n"
+
 #define FLAG_REPLACE_CALL "replace-call-with-contract"
 #define HELP_REPLACE_CALL                                                      \
   " --replace-call-with-contract <fun>\n"                                      \

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

src/goto-instrument/goto_instrument_parse_options.h

@@ -99,6 +99,7 @@ Author: Daniel Kroening, [email protected]
   "(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 "):" \