Handle the case of violation in loop guards in loop-invariant synthesis

In current loop-invariant synthesizer, we synthesize two kinds of clauses separately.
1. `in_clause` that should hold when we enter the loop body---when the loop guard holds, that is ```loop_guard -> in_clause```.
2. `pos_clause` that should hold when we leave the loop---when the loop guard doesn't hold, that is ```!loop_guard -> pos_clause```.

We synthesize `in_clause` when the violations happen in the loop body. We synthesize `pos_clause` when the violation happen after the loop.

This PR handles the case that the violations happen in the loop guard. In the case, the new clause we synthesize should hold for both of the cases that loop guard holds and loop guards doesn't hold.

We introduce a new variable `violation_location` to indicate whether the violation happen in the loop, after the loop, or in the loop guard, and add the new synthesized clause as `in_clause`, `pos_clause`, or both, respectively.

Author: qinheping

regression/goto-synthesizer/loop_contracts_synthesis_06/main.c

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 #define SIZE 80
 
 void main()

regression/goto-synthesizer/loop_contracts_synthesis_06/test.desc

@@ -9,5 +9,4 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This test is a variation of strlen. It checks that we can synthesize
-loop invariant for checks happen in the loop guard.
+Checks whether CBMC synthesizes loop invariants for checks in the loop guard.

regression/goto-synthesizer/loop_contracts_synthesis_06/test_dump.desc

@@ -6,4 +6,4 @@ main.c
 loop 1 invariant.*\_\_CPROVER\_POINTER\_OFFSET
 assigns i
 --
-This test case checks if synthesized contracts are correctly dumped.
+Checks if synthesized contracts are dumped correctly.

regression/goto-synthesizer/loop_contracts_synthesis_07/main.c

@@ -1,3 +1,4 @@
+#include <stdlib.h>
 #define SIZE 80
 
 void main()

regression/goto-synthesizer/loop_contracts_synthesis_07/test.desc

@@ -10,5 +10,4 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that we can synthesize loop invariant for violation happen
-after the loop body.
+Checks whether CBMC synthesizes loop invariants for checks located after the loop body.

regression/goto-synthesizer/loop_contracts_synthesis_07/test_dump.desc

@@ -6,4 +6,4 @@ main.c
 loop 1 assigns i
 loop 1 invariant.*\_\_CPROVER\_POINTER\_OFFSET
 --
-This test case checks if synthesized contracts are correctly dumped.
+Checks if synthesized contracts are dumped correctly.

src/goto-synthesizer/cegis_verifier.cpp

@@ -236,7 +236,7 @@ bool cegis_verifiert::is_instruction_in_transfomed_loop_condition(
   const goto_functiont &function,
   unsigned location_number_of_target)
 {
-  // The transformed loop condition are instructions from
+  // The transformed loop condition is a set of instructions from
   // loop havocing instructions
   // to
   // if(!guard) GOTO EXIT
@@ -245,7 +245,7 @@ bool cegis_verifiert::is_instruction_in_transfomed_loop_condition(
       it != function.body.instructions.end();
       ++it)
   {
-    // Record the location number of the begin of a transformed loop.
+    // Record the location number of the beginning of a transformed loop.
     if(
       loop_havoc_set.count(it) &&
       original_loop_number_map[it] == loop_id.loop_number)

src/goto-synthesizer/cegis_verifier.h

@@ -68,7 +68,7 @@ class cext
   exprt checked_pointer;
   exprt violated_predicate;
 
-  // Location where the violation happen.
+  // Location where the violation happens
   violation_locationt violation_location = violation_locationt::in_loop;
 
   // We collect havoced evaluations of havoced variables and their object sizes

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -408,7 +408,7 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
         return_cex->violation_location ==
         cext::violation_locationt::in_condition)
       {
-        // When the violation is happen in the loop guard, the new clause
+        // When the violation happens in the loop guard, the new clause
         // should hold for the both cases of
         // 1. loop guard holds        --- loop_guard -> in_invariant
         // 2. loop guard doesn't hold --- !loop_guard -> pos_invariant
@@ -420,15 +420,15 @@ invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
       else if(
         return_cex->violation_location == cext::violation_locationt::in_loop)
       {
-        // When the violation is happen in the loop body, the new clause
+        // When the violation happens in the loop body, the new clause
         // should hold for the case of
         // loop guard holds        --- loop_guard -> in_invariant
         in_invariant_clause_map[cause_loop_id] = and_exprt(
           in_invariant_clause_map[cause_loop_id], new_invariant_clause);
       }
       else
       {
-        // When the violation is happen after the loop body, the new clause
+        // When the violation happens after the loop body, the new clause
         // should hold for the case of
         // loop guard doesn't hold --- !loop_guard -> pos_invariant
         pos_invariant_clause_map[cause_loop_id] = and_exprt(