Merge pull request #139 from viktormalik/svcomp20

Improvements for SV-COMP 2020

src/2ls/2ls_parse_options.cpp

@@ -393,6 +393,7 @@ int twols_parse_optionst::doit()
     irep_idt function=cmdline.get_value("function");
     show_ssa(
       goto_model,
+      options,
       heap_analysis,
       function,
       simplify,
@@ -404,14 +405,15 @@ int twols_parse_optionst::doit()
   if(cmdline.isset("show-defs"))
   {
     irep_idt function=cmdline.get_value("function");
-    show_defs(goto_model, function, std::cout, ui_message_handler);
+    show_defs(goto_model, function, options, std::cout, ui_message_handler);
     return 7;
   }
 
   if(cmdline.isset("show-assignments"))
   {
     irep_idt function=cmdline.get_value("function");
-    show_assignments(goto_model, function, std::cout, ui_message_handler);
+    show_assignments(
+      goto_model, function, options, std::cout, ui_message_handler);
     return 7;
   }
 
@@ -425,7 +427,8 @@ int twols_parse_optionst::doit()
   if(cmdline.isset("show-value-sets"))
   {
     irep_idt function=cmdline.get_value("function");
-    show_value_sets(goto_model, function, std::cout, ui_message_handler);
+    show_value_sets(
+      goto_model, function, options, std::cout, ui_message_handler);
     return 7;
   }
 
@@ -574,7 +577,7 @@ int twols_parse_optionst::doit()
 
       if(out_file=="-")
       {
-        horn_encoding(goto_model, std::cout);
+        horn_encoding(goto_model, options, std::cout);
       }
       else
       {
@@ -591,7 +594,7 @@ int twols_parse_optionst::doit()
           return 1;
         }
 
-        horn_encoding(goto_model, out);
+        horn_encoding(goto_model, options, out);
       }
 
       return 0;
@@ -1060,6 +1063,9 @@ bool twols_parse_optionst::process_goto_program(
 #endif
     }
 
+    if(options.get_bool_option("competition-mode"))
+      assert_no_builtin_functions(goto_model);
+
 #if REMOVE_MULTIPLE_DEREFERENCES
     remove_multiple_dereferences(goto_model);
 #endif
@@ -1127,6 +1133,7 @@ bool twols_parse_optionst::process_goto_program(
     if(options.get_bool_option("pointer-check"))
     {
       allow_record_malloc(goto_model);
+      handle_freed_ptr_compare(goto_model);
     }
     if(options.get_bool_option("memory-leak-check"))
       allow_record_memleak(goto_model);
@@ -1142,7 +1149,7 @@ bool twols_parse_optionst::process_goto_program(
       inline_main(goto_model);
     }
 
-    auto dynobj_instances=split_dynamic_objects(goto_model);
+    auto dynobj_instances=split_dynamic_objects(goto_model, options);
 
     if(!cmdline.isset("independent-properties"))
     {

src/2ls/2ls_parse_options.h

@@ -206,9 +206,13 @@ class twols_parse_optionst:
     goto_programt &goto_program,
     const std::map<symbol_exprt, size_t> &instance_counts,
     symbol_tablet &symbol_table);
-  std::map<symbol_exprt, size_t> split_dynamic_objects(goto_modelt &goto_model);
+  std::map<symbol_exprt, size_t> split_dynamic_objects(
+    goto_modelt &goto_model,
+    const optionst &options);
   void limit_array_bounds(goto_modelt &goto_model);
   void memory_assert_info(goto_modelt &goto_model);
+  void handle_freed_ptr_compare(goto_modelt &goto_model);
+  void assert_no_builtin_functions(goto_modelt &goto_model);
 };
 
 #endif

src/2ls/horn_encoding.cpp

@@ -22,9 +22,11 @@ class horn_encodingt
 public:
   horn_encodingt(
     const goto_modelt &_goto_model,
+    const optionst &_options,
     std::ostream &_out):
     goto_functions(_goto_model.goto_functions),
     ns(_goto_model.symbol_table),
+    options(_options),
     out(_out),
     smt2_conv(ns, "", "Horn-clause encoding", "", smt2_convt::Z3, _out)
   {
@@ -35,6 +37,7 @@ class horn_encodingt
 protected:
   const goto_functionst &goto_functions;
   const namespacet ns;
+  const optionst &options;
   std::ostream &out;
 
   smt2_convt smt2_conv;
@@ -61,7 +64,7 @@ void horn_encodingt::translate(
 
   // compute SSA
   ssa_heap_analysist heap_analysis(ns);
-  local_SSAt local_SSA(f_it->second, ns, heap_analysis, "");
+  local_SSAt local_SSA(f_it->second, ns, options, heap_analysis, "");
 
   const goto_programt &body=f_it->second.body;
 
@@ -209,7 +212,8 @@ void horn_encodingt::translate(
 
 void horn_encoding(
   const goto_modelt &goto_model,
+  const optionst &options,
   std::ostream &out)
 {
-  horn_encodingt(goto_model, out)();
+  horn_encodingt(goto_model, options, out)();
 }

src/2ls/horn_encoding.h

@@ -18,6 +18,7 @@ Module: Horn-clause Encoding
 
 void horn_encoding(
   const goto_modelt &,
+  const optionst &options,
   std::ostream &out);
 
 #endif

src/2ls/preprocessing_util.cpp

@@ -15,6 +15,7 @@ Author: Peter Schrammel
 
 #include <analyses/constant_propagator.h>
 #include <goto-instrument/unwind.h>
+#include <goto-instrument/function.h>
 #include <ssa/dynobj_instance_analysis.h>
 
 #include "2ls_parse_options.h"
@@ -611,7 +612,7 @@ void twols_parse_optionst::create_dynobj_instances(
 
         const std::string name=id2string(obj_symbol.name);
         const std::string base_name=id2string(obj_symbol.base_name);
-        std::string suffix="#"+std::to_string(0);
+        std::string suffix="$"+std::to_string(0);
 
         obj_symbol.name=name+suffix;
         obj_symbol.base_name=base_name+suffix;
@@ -632,7 +633,7 @@ void twols_parse_optionst::create_dynobj_instances(
           nondet.pretty_name=nondet.name;
           symbol_table.add(nondet);
 
-          suffix="#"+std::to_string(i);
+          suffix="$"+std::to_string(i);
           obj_symbol.name=name+suffix;
           obj_symbol.base_name=base_name+suffix;
 
@@ -652,16 +653,19 @@ void twols_parse_optionst::create_dynobj_instances(
 }
 
 std::map<symbol_exprt, size_t> twols_parse_optionst::split_dynamic_objects(
-  goto_modelt &goto_model)
+  goto_modelt &goto_model,
+  const optionst &options)
 {
   std::map<symbol_exprt, size_t> dynobj_instances;
   Forall_goto_functions(f_it, goto_model.goto_functions)
   {
     if(!f_it->second.body_available())
       continue;
     namespacet ns(goto_model.symbol_table);
-    ssa_value_ait value_analysis(f_it->second, ns, ssa_heap_analysist(ns));
-    dynobj_instance_analysist do_inst(f_it->second, ns, value_analysis);
+    ssa_value_ait value_analysis(
+      f_it->second, ns, options, ssa_heap_analysist(ns));
+    dynobj_instance_analysist do_inst(
+      f_it->second, ns, options, value_analysis);
 
     compute_dynobj_instances(
       f_it->second.body, do_inst, dynobj_instances, ns);
@@ -737,3 +741,112 @@ void twols_parse_optionst::memory_assert_info(goto_modelt &goto_model)
     }
   }
 }
+
+/// Transform comparison of pointers to be non-deterministic if the pointers
+/// were freed.
+/// This is done by transforming (x op y) into:
+///     (x op y) XOR ((freed(x) || nondet) && (freed(y) && nondet))
+void make_freed_ptr_comparison_nondet(
+  goto_modelt &goto_model,
+  goto_functionst::goto_functiont &fun,
+  goto_programt::instructionst::iterator loc,
+  exprt &cond,
+  const std::set<irep_idt> &typecasted_pointers)
+{
+  if(cond.id()==ID_equal || cond.id()==ID_notequal || cond.id()==ID_le ||
+     cond.id()==ID_lt || cond.id()==ID_ge || cond.id()==ID_gt)
+  {
+    // Check if both operands are either pointers or type-casted pointers
+    if(cond.op0().id()==ID_symbol && cond.op1().id()==ID_symbol &&
+       !is_cprover_symbol(cond.op0()) && !is_cprover_symbol(cond.op1()) &&
+       (cond.op0().type().id()==ID_pointer ||
+        typecasted_pointers.find(to_symbol_expr(cond.op0()).get_identifier())!=
+        typecasted_pointers.end()) &&
+       (cond.op1().type().id()==ID_pointer ||
+        typecasted_pointers.find(to_symbol_expr(cond.op1()).get_identifier())!=
+        typecasted_pointers.end()))
+    {
+      const symbolt &freed=goto_model.symbol_table.lookup(
+        "__CPROVER_deallocated");
+
+      // LHS != __CPROVER_deallocated
+      auto lhs_not_freed_cond=notequal_exprt(
+        typecast_exprt(cond.op0(), freed.type), freed.symbol_expr());
+
+      // RHS != __CPROVER_deallocated
+      auto rhs_not_freed_cond=notequal_exprt(
+        typecast_exprt(cond.op1(), freed.type), freed.symbol_expr());
+
+      // XOR is implemented as ==
+      cond=equal_exprt(
+        cond,
+        and_exprt(
+          or_exprt(
+            lhs_not_freed_cond,
+            side_effect_expr_nondett(bool_typet())),
+          or_exprt(
+            rhs_not_freed_cond,
+            side_effect_expr_nondett(bool_typet()))));
+    }
+  }
+  else if(cond.id()==ID_not)
+    make_freed_ptr_comparison_nondet(
+      goto_model, fun, loc, to_not_expr(cond).op(), typecasted_pointers);
+}
+
+/// Transform each comparison of pointers so that it has a non-deterministic
+/// result if the pointers were freed, since comparison of freed pointers is
+/// an undefined behavior.
+void twols_parse_optionst::handle_freed_ptr_compare(goto_modelt &goto_model)
+{
+  std::set<irep_idt> typecasted_pointers;
+  Forall_goto_functions(f_it, goto_model.goto_functions)
+  {
+    Forall_goto_program_instructions(i_it, f_it->second.body)
+    {
+      if(i_it->is_goto())
+      {
+        auto &guard=i_it->guard;
+        make_freed_ptr_comparison_nondet(
+          goto_model, f_it->second, i_it, guard, typecasted_pointers);
+      }
+      else if(i_it->is_assign())
+      {
+        auto &assign=to_code_assign(i_it->code);
+        // If a pointer is casted to a non-pointer type (probably an integer),
+        // save the destination variable into typecasted_pointers
+        if(assign.lhs().id()==ID_symbol &&
+           ((assign.rhs().id()==ID_typecast &&
+             to_typecast_expr(assign.rhs()).op().type().id()==ID_pointer &&
+             assign.lhs().type().id()!=ID_pointer) ||
+            typecasted_pointers.find(
+              to_symbol_expr(assign.lhs()).get_identifier())!=
+            typecasted_pointers.end()))
+        {
+          typecasted_pointers.insert(
+            to_symbol_expr(assign.lhs()).get_identifier());
+        }
+      }
+    }
+  }
+}
+
+/// Add assertions preventing analysis of programs using GCC builtin functions
+/// that are not supported and can cause false results.
+void twols_parse_optionst::assert_no_builtin_functions(goto_modelt &goto_model)
+{
+  forall_goto_program_instructions(
+    i_it,
+    goto_model.goto_functions.function_map.find("_start")->second.body)
+  {
+    std::string name=id2string(i_it->source_location.get_function());
+    assert(
+      name.find("__builtin_")==std::string::npos &&
+      name.find("__CPROVER_overflow")==std::string::npos);
+
+    if(i_it->is_assign())
+    {
+      assert(i_it->code.op1().id()!=ID_popcount);
+    }
+  }
+}