Disallow enumerate equal expr between sub-exprs with different types.

Author: qinheping

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1433,10 +1433,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         " or --" FLAG_LOOP_CONTRACTS);
     }
 
-    log.warning() << "Loop invariant synthesizer is still work in progress. "
-                     "It only generates TRUE as invariants."
-                  << messaget::eom;
-
     // Synthesize loop invariants and annotate them into `goto_model`
     enumerative_loop_invariant_synthesizert synthesizer(goto_model, log);
     annotate_invariants(synthesizer.synthesize_all(), goto_model);

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.cpp

@@ -48,8 +48,14 @@ std::vector<exprt> construct_terminals(std::set<symbol_exprt> symbols)
       // For a variable v with primitive type, we add
       // v, __CPROVER_loop_entry(v)
       // into the result.
+      result.push_back(typecast_exprt(e, size_type()));
+      result.push_back(
+        typecast_exprt(unary_exprt(ID_loop_entry, e, e.type()), size_type()));
+    }
+    if((e.type().id() == ID_signedbv))
+    {
       result.push_back(e);
-      result.push_back(unary_exprt(ID_loop_entry, e, size_type()));
+      result.push_back(unary_exprt(ID_loop_entry, e, e.type()));
     }
     if((e.type().id() == ID_pointer))
     {
@@ -62,7 +68,8 @@ std::vector<exprt> construct_terminals(std::set<symbol_exprt> symbols)
         unary_exprt(ID_loop_entry, e, e.type()), size_type()));
     }
   }
-  result.push_back(from_integer(1, size_type()));
+  result.push_back(from_integer(1, unsigned_int_type()));
+  result.push_back(from_integer(1, unsigned_long_int_type()));
   return result;
 }
 

src/goto-instrument/synthesizer/expr_enumerator.cpp

@@ -316,7 +316,18 @@ exprt binary_functional_enumeratort::instantiate(const expr_listt &exprs) const
     exprs.size() == 2,
     "number of arguments should be 2: " + integer2string(exprs.size()));
   if(op_id == ID_equal)
+  {
+    if(exprs.front().type() != exprs.back().type())
+      return true_exprt();
+
     return equal_exprt(exprs.front(), exprs.back());
+  }
+  if(op_id == ID_notequal)
+  {
+    if(exprs.front().type() != exprs.back().type())
+      return true_exprt();
+    return notequal_exprt(exprs.front(), exprs.back());
+  }
   if(op_id == ID_le)
     return less_than_or_equal_exprt(exprs.front(), exprs.back());
   if(op_id == ID_lt)
@@ -333,8 +344,6 @@ exprt binary_functional_enumeratort::instantiate(const expr_listt &exprs) const
     return plus_exprt(exprs.front(), exprs.back());
   if(op_id == ID_minus)
     return minus_exprt(exprs.front(), exprs.back());
-  if(op_id == ID_notequal)
-    return notequal_exprt(exprs.front(), exprs.back());
   return binary_exprt(exprs.front(), op_id, exprs.back());
 }
 

src/goto-programs/CMakeLists.txt

@@ -3,4 +3,4 @@ add_library(goto-programs ${sources})
 
 generic_includes(goto-programs)
 
-target_link_libraries(goto-programs util assembler langapi analyses linking ansi-c)
+target_link_libraries(goto-programs util assembler langapi analyses linking ansi-c json)