Check side effect of loop contracts during instrumentation

doc/man/goto-instrument.1

@@ -1015,7 +1015,13 @@ force aggressive slicer to preserve all direct paths
 .SS "Code contracts:"
 .TP
 \fB\-\-apply\-loop\-contracts\fR
-check and use loop contracts when provided
+.TP
+\fB\-disable\-loop\-contracts\-side\-effect\-check\fR
+UNSOUND OPTION. Disable checking the absence of side effects in loop
+contract clauses. In absence of such checking, loop contracts clauses will
+accept more expressions, such as pure functions and statement expressions.
+But user have to make sure the loop contracts are side-effect free by them self
+to get a sound result.
 .TP
 \fB\-loop\-contracts\-no\-unwind\fR
 do not unwind transformed loops

regression/contracts-dfcc/loop_contracts_statement_expression/main.c

@@ -0,0 +1,16 @@
+int main()
+{
+  unsigned i;
+
+  while(i > 1)
+    __CPROVER_loop_invariant(({
+      unsigned b = i >= 1;
+      goto label;
+      b = i < 1;
+    label:
+      b;
+    }))
+    {
+      i--;
+    }
+}

regression/contracts-dfcc/loop_contracts_statement_expression/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --apply-loop-contracts --disable-side-effect-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test demonstrates a case where the loop invariant
+is a side-effect free statement expression.

regression/contracts/loop_contracts_statement_expression/main.c

@@ -0,0 +1,16 @@
+int main()
+{
+  unsigned i;
+
+  while(i > 1)
+    __CPROVER_loop_invariant(({
+      unsigned b = i >= 1;
+      goto label;
+      b = i < 1;
+    label:
+      b;
+    }))
+    {
+      i--;
+    }
+}

regression/contracts/loop_contracts_statement_expression/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--apply-loop-contracts --disable-side-effect-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test demonstrates a case where the loop invariant
+is a side-effect free statement expression.

src/ansi-c/goto-conversion/goto_convert.cpp

@@ -1036,12 +1036,6 @@ void goto_convertt::convert_loop_contracts(
     static_cast<const exprt &>(code.find(ID_C_spec_loop_invariant));
   if(!invariant.is_nil())
   {
-    if(has_subexpr(invariant, ID_side_effect))
-    {
-      throw incorrect_goto_program_exceptiont(
-        "Loop invariant is not side-effect free.", code.find_source_location());
-    }
-
     PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
     loop->condition_nonconst().add(ID_C_spec_loop_invariant).swap(invariant);
   }
@@ -1050,13 +1044,6 @@ void goto_convertt::convert_loop_contracts(
     static_cast<const exprt &>(code.find(ID_C_spec_decreases));
   if(!decreases_clause.is_nil())
   {
-    if(has_subexpr(decreases_clause, ID_side_effect))
-    {
-      throw incorrect_goto_program_exceptiont(
-        "Decreases clause is not side-effect free.",
-        code.find_source_location());
-    }
-
     PRECONDITION(loop->is_goto() || loop->is_incomplete_goto());
     loop->condition_nonconst().add(ID_C_spec_decreases).swap(decreases_clause);
   }

src/cprover/instrument_given_invariants.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "instrument_given_invariants.h"
 
+#include <util/expr_util.h>
+
 #include <goto-programs/goto_model.h>
 
 void instrument_given_invariants(goto_functionst::function_mapt::value_type &f)
@@ -25,6 +27,15 @@ void instrument_given_invariants(goto_functionst::function_mapt::value_type &f)
     {
       const auto &invariants = static_cast<const exprt &>(
         it->condition().find(ID_C_spec_loop_invariant));
+      if(!invariants.is_nil())
+      {
+        if(has_subexpr(invariants, ID_side_effect))
+        {
+          throw incorrect_goto_program_exceptiont(
+            "Loop invariant is not side-effect free.",
+            it->condition().find_source_location());
+        }
+      }
 
       for(const auto &invariant : invariants.operands())
       {

src/goto-instrument/contracts/contracts.cpp

@@ -983,12 +983,11 @@ void code_contractst::apply_loop_contract(
       goto_function.body, loop_head, goto_programt::make_skip());
     loop_end->set_target(loop_head);
 
-    exprt assigns_clause =
-      static_cast<const exprt &>(loop_end->condition().find(ID_C_spec_assigns));
-    exprt invariant = static_cast<const exprt &>(
-      loop_end->condition().find(ID_C_spec_loop_invariant));
-    exprt decreases_clause = static_cast<const exprt &>(
-      loop_end->condition().find(ID_C_spec_decreases));
+    exprt assigns_clause = get_loop_assigns(loop_end);
+    exprt invariant =
+      get_loop_invariants(loop_end, loop_contract_config.check_side_effect);
+    exprt decreases_clause =
+      get_loop_decreases(loop_end, loop_contract_config.check_side_effect);
 
     if(invariant.is_nil())
     {

src/goto-instrument/contracts/contracts.h

@@ -33,6 +33,10 @@ Date: February 2016
 #define HELP_LOOP_CONTRACTS                                                    \
   " {y--apply-loop-contracts} \t check and use loop contracts when provided\n"
 
+#define FLAG_DISABLE_SIDE_EFFECT_CHECK "disable-loop-contracts-side-effect-check"
+#define HELP_DISABLE_SIDE_EFFECT_CHECK                                         \
+  " {y--disable-loop-contracts-side-effect-check} \t UNSOUND OPTION.\t "       \
+  " do not check side-effect of loop contracts\n"
 #define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind"
 #define HELP_LOOP_CONTRACTS_NO_UNWIND                                          \
   " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n"

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

@@ -29,40 +29,15 @@ Date: March 2023
 #include "dfcc_root_object.h"
 #include "dfcc_utils.h"
 
-/// Extracts the assigns clause expression from the latch condition
-static const exprt::operandst &
-get_assigns(const goto_programt::const_targett &latch_target)
-{
-  return static_cast<const exprt &>(
-           latch_target->condition().find(ID_C_spec_assigns))
-    .operands();
-}
-
-/// Extracts the invariant clause expression from the latch condition
-static const exprt::operandst &
-get_invariants(const goto_programt::const_targett &latch_target)
-{
-  return static_cast<const exprt &>(
-           latch_target->condition().find(ID_C_spec_loop_invariant))
-    .operands();
-}
-
-/// Extracts the decreases clause expression from the latch condition
-static const exprt::operandst &
-get_decreases(const goto_programt::const_targett &latch_target)
-{
-  return static_cast<const exprt &>(
-           latch_target->condition().find(ID_C_spec_decreases))
-    .operands();
-}
-
 /// Returns true iff some contract clause expression is attached
 /// to the latch condition of this loop
-static bool has_contract(const goto_programt::const_targett &latch_target)
+static bool has_contract(
+  const goto_programt::const_targett &latch_target,
+  const bool check_side_effect)
 {
-  return !get_assigns(latch_target).empty() ||
-         !get_invariants(latch_target).empty() ||
-         !get_decreases(latch_target).empty();
+  return get_loop_assigns(latch_target).is_not_nil() ||
+         get_loop_invariants(latch_target, check_side_effect).is_not_nil() ||
+         get_loop_decreases(latch_target, check_side_effect).is_not_nil();
 }
 
 void dfcc_loop_infot::output(std::ostream &out) const
@@ -155,16 +130,20 @@ dfcc_loop_infot::find_latch(goto_programt &goto_program) const
 static std::optional<goto_programt::targett> check_has_contract_rec(
   const dfcc_loop_nesting_grapht &loop_nesting_graph,
   const std::size_t loop_idx,
-  const bool must_have_contract)
+  const bool must_have_contract,
+  const bool check_side_effect)
 {
   const auto &node = loop_nesting_graph[loop_idx];
-  if(must_have_contract && !has_contract(node.latch))
+  if(must_have_contract && !has_contract(node.latch, check_side_effect))
     return node.head;
 
   for(const auto pred_idx : loop_nesting_graph.get_predecessors(loop_idx))
   {
     auto result = check_has_contract_rec(
-      loop_nesting_graph, pred_idx, has_contract(node.latch));
+      loop_nesting_graph,
+      pred_idx,
+      has_contract(node.latch, check_side_effect),
+      check_side_effect);
     if(result.has_value())
       return result;
   }
@@ -175,13 +154,15 @@ static std::optional<goto_programt::targett> check_has_contract_rec(
 /// loops nested in loops that have contracts also have contracts.
 /// Return the head of the first offending loop if it exists, nothing otherwise.
 static std::optional<goto_programt::targett> check_inner_loops_have_contracts(
-  const dfcc_loop_nesting_grapht &loop_nesting_graph)
+  const dfcc_loop_nesting_grapht &loop_nesting_graph,
+  const bool check_side_effect)
 {
   for(std::size_t idx = 0; idx < loop_nesting_graph.size(); idx++)
   {
     if(loop_nesting_graph.get_successors(idx).empty())
     {
-      auto result = check_has_contract_rec(loop_nesting_graph, idx, false);
+      auto result = check_has_contract_rec(
+        loop_nesting_graph, idx, false, check_side_effect);
       if(result.has_value())
         return result;
     }
@@ -349,18 +330,21 @@ static struct contract_clausest default_loop_contract_clauses(
   const std::size_t loop_id,
   const irep_idt &function_id,
   local_may_aliast &local_may_alias,
+  const bool check_side_effect,
   message_handlert &message_handler,
   const namespacet &ns)
 {
   messaget log(message_handler);
   const auto &loop = loop_nesting_graph[loop_id];
 
   // Process loop contract clauses
-  exprt::operandst invariant_clauses = get_invariants(loop.latch);
-  exprt::operandst assigns_clauses = get_assigns(loop.latch);
+  exprt::operandst invariant_clauses =
+    get_loop_invariants(loop.latch, check_side_effect).operands();
+  exprt::operandst assigns_clauses = get_loop_assigns(loop.latch).operands();
 
   // Initialise defaults
-  struct contract_clausest result(get_decreases(loop.latch));
+  struct contract_clausest result(
+    get_loop_decreases(loop.latch, check_side_effect).operands());
 
   // Generate defaults for all clauses if at least one type of clause is defined
   if(
@@ -435,6 +419,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
   const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
   dirtyt &dirty,
   local_may_aliast &local_may_alias,
+  const bool check_side_effect,
   message_handlert &message_handler,
   dfcc_libraryt &library,
   symbol_table_baset &symbol_table)
@@ -454,6 +439,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
     loop_id,
     function_id,
     local_may_alias,
+    check_side_effect,
     message_handler,
     ns);
 
@@ -523,7 +509,8 @@ dfcc_cfg_infot::dfcc_cfg_infot(
     dfcc_check_loop_normal_form(goto_program, log);
     loop_nesting_graph = build_loop_nesting_graph(goto_program);
 
-    const auto head = check_inner_loops_have_contracts(loop_nesting_graph);
+    const auto head = check_inner_loops_have_contracts(
+      loop_nesting_graph, loop_contract_config.check_side_effect);
     if(head.has_value())
     {
       throw invalid_source_file_exceptiont(
@@ -571,6 +558,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
          loop_info_map,
          dirty,
          local_may_alias,
+         loop_contract_config.check_side_effect,
          message_handler,
          library,
          symbol_table)});

src/goto-instrument/contracts/utils.cpp

@@ -682,6 +682,66 @@ get_loop_head(const unsigned int target_loop_number, goto_functiont &function)
   return get_loop_head_or_end(target_loop_number, function, true);
 }
 
+/// Extract loop invariants from loop end without any checks.
+static exprt
+extract_loop_invariants(const goto_programt::const_targett &loop_end)
+{
+  return static_cast<const exprt &>(
+    loop_end->condition().find(ID_C_spec_loop_invariant));
+}
+
+static exprt extract_loop_assigns(const goto_programt::const_targett &loop_end)
+{
+  return static_cast<const exprt &>(
+    loop_end->condition().find(ID_C_spec_assigns));
+}
+
+static exprt
+extract_loop_decreases(const goto_programt::const_targett &loop_end)
+{
+  return static_cast<const exprt &>(
+    loop_end->condition().find(ID_C_spec_decreases));
+}
+
+exprt get_loop_invariants(
+  const goto_programt::const_targett &loop_end,
+  const bool check_side_effect)
+{
+  auto invariant = extract_loop_invariants(loop_end);
+  if(!invariant.is_nil() && check_side_effect)
+  {
+    if(has_subexpr(invariant, ID_side_effect))
+    {
+      throw incorrect_goto_program_exceptiont(
+        "Loop invariant is not side-effect free.",
+        loop_end->condition().find_source_location());
+    }
+  }
+  return invariant;
+}
+
+exprt get_loop_assigns(const goto_programt::const_targett &loop_end)
+{
+  return extract_loop_assigns(loop_end);
+}
+
+exprt get_loop_decreases(
+  const goto_programt::const_targett &loop_end,
+  const bool check_side_effect)
+{
+  auto decreases_clause = extract_loop_decreases(loop_end);
+  if(!decreases_clause.is_nil() && check_side_effect)
+  {
+    if(has_subexpr(decreases_clause, ID_side_effect))
+    {
+      throw incorrect_goto_program_exceptiont(
+        "Decreases clause is not side-effect free.",
+        loop_end->condition().find_source_location());
+    }
+  }
+  return decreases_clause;
+}
+
 void annotate_invariants(
   const invariant_mapt &invariant_map,
   goto_modelt &goto_model)

src/goto-instrument/contracts/utils.h

@@ -313,6 +313,23 @@ get_loop_end(const unsigned int loop_number, goto_functiont &function);
 goto_programt::targett
 get_loop_head(const unsigned int loop_number, goto_functiont &function);
 
+/// Extract loop invariants from annotated loop end.
+/// Will check if the loop invariant is side-effect free if
+/// \p check_side_effect` is set.
+exprt get_loop_invariants(
+  const goto_programt::const_targett &loop_end,
+  const bool check_side_effect = true);
+
+/// Extract loop assigns from annotated loop end.
+exprt get_loop_assigns(const goto_programt::const_targett &loop_end);
+
+/// Extract loop decreases from annotated loop end.
+/// Will check if the loop decreases is side-effect free if
+/// \p check_side_effect` is set.
+exprt get_loop_decreases(
+  const goto_programt::const_targett &loop_end,
+  const bool check_side_effect = true);
+
 /// Annotate the invariants in `invariant_map` to their corresponding
 /// loops. Corresponding loops are specified by keys of `invariant_map`
 void annotate_invariants(