Several fixes for SV-COMP

regression/heap-data/shared_mem1_false/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---heap --values-refine --k-induction
+--heap --intervals --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/kiki/hard2_unwindbound5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---heap --values-refine --k-induction --competition-mode
+--heap --intervals --k-induction --competition-mode
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*FAILURE$

regression/kiki/induction5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---k-induction
+--k-induction --std-invariants
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*FAILURE$

regression/kiki/induction7/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---k-induction
+--k-induction --std-invariants
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*FAILURE$

regression/kiki/nested12/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---k-induction
+--k-induction --std-invariants
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*FAILURE$

regression/overflows/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+FLAGS = --verbosity 10
+
+test:
+	@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)"
+
+tests.log: ../test.pl
+	@../test.pl -p -c "../../../src/2ls/2ls $(FLAGS)"
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@rm -f *.log
+	@for dir in *; do rm -f $$dir/*.out; done;

regression/overflows/scanf-overflow-bad/main.c

@@ -0,0 +1,28 @@
+// Inspired by SV-comp:
+// https://sv-comp.sosy-lab.org/2023/results/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int64_t_fscanf_add_01_bad.i
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
+void printLine(const char * line);
+void printLongLine(long longNumber);
+
+void CWE190_Integer_Overflow__int64_t_fscanf_add_01_bad()
+{
+    int64_t data;
+    data = 0LL;
+    fscanf (stdin, "%" "l" "d", &data);
+    {
+        int64_t result = data + 1;
+        printLongLongLine(result);
+    }
+}
+int main(int argc, char * argv[])
+{
+    srand( (unsigned)time(((void *)0)) );
+    printLine("Calling bad()...");
+    CWE190_Integer_Overflow__int64_t_fscanf_add_01_bad();
+    printLine("Finished bad()");
+    return 0;
+}

regression/overflows/scanf-overflow-bad/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--signed-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/overflows/scanf-overflow-good/main.c

@@ -0,0 +1,49 @@
+// Inspired by SV-comp:
+// https://sv-comp.sosy-lab.org/2023/results/sv-benchmarks/c/Juliet_Test/CWE190_Integer_Overflow__int64_t_fscanf_add_01_good.i
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <time.h>
+
+void printLine(const char * line);
+void printLongLine(long longNumber);
+void printLongLongLine(int64_t longLongIntNumber);
+
+static void goodG2B()
+{
+    int64_t data;
+    data = 0LL;
+    data = 2;
+    {
+        int64_t result = data + 1;
+        printLongLongLine(result);
+    }
+}
+static void goodB2G()
+{
+    int64_t data;
+    data = 0LL;
+    fscanf (stdin, "%" "l" "d", &data);
+    if (data < 0x7fffffffffffffffLL)
+    {
+        int64_t result = data + 1;
+        printLongLongLine(result);
+    }
+    else
+    {
+        printLine("data value is too large to perform arithmetic safely.");
+    }
+}
+void CWE190_Integer_Overflow__int64_t_fscanf_add_01_good()
+{
+    goodG2B();
+    goodB2G();
+}
+int main(int argc, char * argv[])
+{
+    srand( (unsigned)time(((void *)0)) );
+    printLine("Calling good()...");
+    CWE190_Integer_Overflow__int64_t_fscanf_add_01_good();
+    printLine("Finished good()");
+    return 0;
+}

regression/overflows/scanf-overflow-good/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--signed-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

src/2ls/2ls_parse_options.cpp

@@ -296,7 +296,6 @@ void twols_parse_optionst::get_command_line_options(optionst &options)
   // do k-induction refinement
   if(cmdline.isset("k-induction"))
   {
-    options.set_option("std-invariants", true);
     options.set_option("k-induction", true);
     options.set_option("inline", true);
     if(!cmdline.isset("unwind"))
@@ -1048,6 +1047,8 @@ bool twols_parse_optionst::process_goto_program(
     if(options.get_bool_option("competition-mode"))
       assert_no_builtin_functions(goto_model);
 
+    make_scanf_nondet(goto_model);
+
 #if REMOVE_MULTIPLE_DEREFERENCES
     remove_multiple_dereferences(goto_model);
 #endif
@@ -1114,6 +1115,7 @@ bool twols_parse_optionst::process_goto_program(
     // Replace malloc
     dynamic_objects=util_make_unique<dynamic_objectst>(goto_model);
     dynamic_objects->replace_malloc(options.get_bool_option("pointer-check"));
+    dynamic_objects->generate_instances(options);
 
     // Allow recording of mallocs and memory leaks
     if(options.get_bool_option("pointer-check"))
@@ -1138,8 +1140,6 @@ bool twols_parse_optionst::process_goto_program(
       inline_main(goto_model);
     }
 
-    dynamic_objects->generate_instances(options);
-
     if(!cmdline.isset("independent-properties"))
     {
       add_assumptions_after_assertions(goto_model);

src/2ls/2ls_parse_options.h

@@ -190,6 +190,7 @@ class twols_parse_optionst:
   void fix_goto_targets(goto_modelt &goto_model);
   void make_assertions_false(goto_modelt &goto_model);
   void make_symbolic_array_indices(goto_modelt &goto_model);
+  void make_scanf_nondet(goto_modelt &goto_model);
 };
 
 #endif

src/2ls/preprocessing_util.cpp

@@ -849,3 +849,43 @@ void twols_parse_optionst::make_symbolic_array_indices(goto_modelt &goto_model)
   }
   goto_model.goto_functions.update();
 }
+
+/// Makes user input nondeterministic, i.e. arguments of fscanf starting
+/// from the second one are assigned a nondeterministic value.
+void twols_parse_optionst::make_scanf_nondet(goto_modelt &goto_model)
+{
+  for(auto &f_it : goto_model.goto_functions.function_map)
+  {
+    Forall_goto_program_instructions(i_it, f_it.second.body)
+    {
+      if(!i_it->is_function_call())
+        continue;
+      auto name = to_symbol_expr(i_it->call_function()).get_identifier();
+      // FIXME: this is a bit hacky and should probably be handled better in
+      //        coordination with CBMC.
+      int start;
+      if(name == "__isoc99_fscanf" || name == "fscanf")
+        start = 2;
+      else if(name == "__isoc99_scanf" || name == "scanf")
+        start = 1;
+      else
+        continue;
+      int i = 0;
+      for(const auto &arg : i_it->call_arguments())
+      {
+        if(i >= start)
+        {
+          if(arg.id() == ID_address_of)
+          {
+            auto lhs = dereference_exprt(arg);
+            side_effect_expr_nondett rhs(
+              to_address_of_expr(arg).object().type(), i_it->source_location());
+            f_it.second.body.insert_after(
+              i_it, goto_programt::make_assignment(lhs, rhs));
+          }
+        }
+        i++;
+      }
+    }
+  }
+}

src/2ls/summary_checker_kind.cpp

@@ -44,6 +44,21 @@ resultt summary_checker_kindt::operator()()
     {
       summarize(goto_model);
       result=check_properties();
+
+      if(result == resultt::UNKNOWN &&
+         options.get_bool_option("values-refine") &&
+         options.get_bool_option("intervals"))
+      {
+        // Now try with zones
+        summary_db.mark_recompute_all();
+        options.set_option("intervals", false);
+        options.set_option("zones", true);
+        summarize(goto_model);
+        result = check_properties();
+        // Reset back to intervals (for the next unwinding)
+        options.set_option("intervals", true);
+        options.set_option("zones", false);
+      }
     }
 
     if(result==resultt::PASS)

src/domains/array_domain.cpp

@@ -144,7 +144,7 @@ void array_domaint::make_segments(const var_specst &var_specs,
   }
   // renaming_map contains some extra mappings that we used to determine index
   // ordering but now we have to remove them
-  clear_non_lb_renamings();
+  clear_array_renamings(renaming_map);
 }
 
 /// Add a single segment to the template.
@@ -810,7 +810,7 @@ void array_domaint::extend_indices_by_loop_inits(var_listt &indices)
 /// Remove all renamings that do not rename loop-back variables
 /// These are necessary for array domain initialization but can spoil
 /// the invariant inference process.
-void array_domaint::clear_non_lb_renamings()
+void array_domaint::clear_array_renamings(replace_mapt &renaming_map)
 {
   for(auto it = renaming_map.begin(); it != renaming_map.end();)
   {

src/domains/array_domain.h

@@ -184,6 +184,8 @@ class array_domaint : public domaint
                       const local_SSAt &SSA,
                       message_handlert &message_handler) override;
 
+  static void clear_array_renamings(replace_mapt &renaming_map);
+
 protected:
   void make_segments(const var_specst &var_specs, const namespacet &ns);
   array_segmentt *add_segment(const var_spect &var_spec,
@@ -203,7 +205,6 @@ class array_domaint : public domaint
                      const exprt &array_size);
 
   void extend_indices_by_loop_inits(var_listt &indices);
-  void clear_non_lb_renamings();
 
   void add_array_difference_template(tpolyhedra_domaint *domain,
                                      const var_specst &segment_var_specs,

src/domains/template_generator_base.cpp

@@ -628,6 +628,8 @@ std::unique_ptr<domaint> template_generator_baset::instantiate_standard_domains(
                                              SSA,
                                              solver,
                                              *this));
+    else
+      array_domaint::clear_array_renamings(post_renaming_map);
   }
 
   if(options.get_bool_option("intervals"))

src/ssa/local_ssa.cpp

@@ -1578,6 +1578,9 @@ local_SSAt::locationt
 local_SSAt::get_loc_with_symbol_def(const symbol_exprt &symbol) const
 {
   std::string id = id2string(symbol.get_identifier());
+  auto percent = id.find("%");
+  if(percent != std::string::npos)
+    id = id.substr(0, percent);
   auto loc_suffix = id.substr(id.find_last_not_of("0123456789") + 1);
   return get_location(std::stoi(loc_suffix));
 }