Merge pull request #141 from viktormalik/generic-solvers

Generic abstract domains and strategy solvers
diffblue · Jul 27, 2020 · b856541 · b856541
2 parents 615a853 + 90c3c63
commit b856541
Show file tree

Hide file tree

Showing 114 changed files with 2,667 additions and 5,655 deletions.
diff --git a/regression/book-examples/sll_min/assertions.desc b/regression/book-examples/sll_min/assertions.desc
@@ -1,6 +1,6 @@
 CORE
 sll_min.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/calendar/test.desc b/regression/heap-data/calendar/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/cart/test.desc b/regression/heap-data/cart/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/hash_fun/test.desc b/regression/heap-data/hash_fun/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/min_max/test.desc b/regression/heap-data/min_max/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/packet_filter/test.desc b/regression/heap-data/packet_filter/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/process_queue/test.desc b/regression/heap-data/process_queue/test.desc
@@ -1,6 +1,6 @@
 THOROUGH
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/quick_sort_split/test.desc b/regression/heap-data/quick_sort_split/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/running_example/test.desc b/regression/heap-data/running_example/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/running_example_assume/test.desc b/regression/heap-data/running_example_assume/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/shared_mem1/test.desc b/regression/heap-data/shared_mem1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap-data/shared_mem2/test.desc b/regression/heap-data/shared_mem2/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-values-refine
+--heap --values-refine
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap/built_from_end/test.desc b/regression/heap/built_from_end/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-interval --no-propagation
+--heap --intervals --no-propagation
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/heap/list_false/test.desc b/regression/heap/list_false/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-interval --no-propagation
+--heap --intervals --no-propagation
 ^EXIT=5$
 ^SIGNAL=0$
 ^VERIFICATION INCONCLUSIVE$

diff --git a/regression/heap/list_false_kind/test.desc b/regression/heap/list_false_kind/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-interval --no-propagation --k-induction
+--heap --intervals --no-propagation --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

diff --git a/regression/heap/simple_false/test.desc b/regression/heap/simple_false/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-interval --no-propagation
+--heap --intervals --no-propagation
 ^EXIT=5$
 ^SIGNAL=0$
 ^VERIFICATION INCONCLUSIVE$

diff --git a/regression/heap/simple_false_kind/test.desc b/regression/heap/simple_false_kind/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-interval --no-propagation --k-induction
+--heap --intervals --no-propagation --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

diff --git a/regression/heap/sll_simple/test.desc b/regression/heap/sll_simple/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap --no-propagation --heap-interval
+--heap --no-propagation --intervals
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/memsafety/built_from_end/test.desc b/regression/memsafety/built_from_end/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-interval --pointer-check --no-assertions
+--heap --intervals --pointer-check --no-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/memsafety/built_from_end_false/test.desc b/regression/memsafety/built_from_end_false/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-interval --pointer-check --no-assertions --k-induction
+--heap --intervals --pointer-check --no-assertions --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

diff --git a/regression/memsafety/simple_false/test.desc b/regression/memsafety/simple_false/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-interval --pointer-check --k-induction
+--heap --intervals --pointer-check --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

diff --git a/regression/memsafety/simple_true/test.desc b/regression/memsafety/simple_true/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---heap-interval --pointer-check --no-assertions
+--heap --intervals --pointer-check --no-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp
@@ -162,55 +162,78 @@ void twols_parse_optionst::get_command_line_options(optionst &options)
 
   if(cmdline.isset("havoc"))
     options.set_option("havoc", true);
-  else if(cmdline.isset("equalities"))
-  {
-    options.set_option("equalities", true);
-    options.set_option("std-invariants", true);
-  }
-  else if(cmdline.isset("heap"))
-  {
-    options.set_option("heap", true);
-  }
-  else if(cmdline.isset("heap-interval"))
-  {
-    options.set_option("heap-interval", true);
-    if(cmdline.isset("sympath"))
-      options.set_option("sympath", true);
-  }
-  else if(cmdline.isset("heap-zones"))
-  {
-    options.set_option("heap-zones", true);
-    if(cmdline.isset("sympath"))
-      options.set_option("sympath", true);
-  }
-  else if(cmdline.isset("heap-values-refine"))
-  {
-    options.set_option("heap-values-refine", true);
-    options.set_option("heap-interval", true);
-    if(cmdline.isset("sympath"))
-      options.set_option("sympath", true);
-  }
   else
   {
-    if(cmdline.isset("zones"))
+    // Options for using simple domains
+    optionst::value_listt simple_domains;
+    if(cmdline.isset("equalities"))
+    {
+      options.set_option("equalities", true);
+      options.set_option("std-invariants", true);
+      simple_domains.push_back("equalities");
+    }
+    if(cmdline.isset("heap"))
+    {
+      options.set_option("heap", true);
+      simple_domains.push_back("heap");
+    }
+
+    // Choose only a single value domain
+    if(cmdline.isset("values-refine"))
+    {
+      options.set_option("values-refine", true);
+      options.set_option("intervals", true);
+      simple_domains.push_back("intervals");
+    }
+    else if(cmdline.isset("zones"))
+    {
       options.set_option("zones", true);
+      simple_domains.push_back("zones");
+    }
     else if(cmdline.isset("qzones"))
+    {
       options.set_option("qzones", true);
+      simple_domains.push_back("qzones");
+    }
     else if(cmdline.isset("octagons"))
+    {
       options.set_option("octagons", true);
-    else // if(cmdline.isset("intervals")) // default
+      simple_domains.push_back("octagons");
+    }
+    else if(cmdline.isset("intervals"))
+    {
+      options.set_option("intervals", true);
+      simple_domains.push_back("intervals");
+    }
+
+    // If no simple domains are specified, use intervals
+    if(simple_domains.empty())
+    {
       options.set_option("intervals", true);
+      simple_domains.push_back("intervals");
+    }
+
+    // TODO: due to various modifications of options during verification
+    //  (e.g. in summary_checker_ait or in handle_special_functions), it is not
+    //  possible to rely on the content of this option.
+    options.set_option("simple-domains", simple_domains);
 
-    if(cmdline.isset("enum-solver"))
-      options.set_option("enum-solver", true);
-    else // if(cmdline.isset("binsearch-solver")) // default
-      options.set_option("binsearch-solver", true);
+    if(options.get_bool_option("values-refine") ||
+       options.get_bool_option("zones") ||
+       options.get_bool_option("qzones") ||
+       options.get_bool_option("octagons") ||
+       options.get_bool_option("intervals"))
+    {
+      // Choose solver for numerical domains
+      if(cmdline.isset("enum-solver"))
+        options.set_option("enum-solver", true);
+      else // if(cmdline.isset("binsearch-solver")) // default
+        options.set_option("binsearch-solver", true);
+    }
   }
 
-  if(cmdline.isset("heap") ||
-     cmdline.isset("heap-interval") ||
-     cmdline.isset("heap-zones") ||
-     cmdline.isset("heap-values-refine"))
+  // Heap domain requires full program inlining and usage of symbolic paths
+  if(cmdline.isset("heap"))
   {
     options.set_option("inline", true);
     options.set_option("sympath", true);
@@ -379,14 +402,6 @@ int twols_parse_optionst::doit()
     return 6;
 
   const namespacet ns(goto_model.symbol_table);
-  ssa_heap_analysist heap_analysis(ns);
-  if((options.get_bool_option("heap") ||
-      options.get_bool_option("heap-interval")) &&
-     !options.get_bool_option("inline"))
-  {
-    heap_analysis(goto_model.goto_functions);
-    add_dynamic_object_symbols(heap_analysis, goto_model);
-  }
 
   if(cmdline.isset("show-stats"))
   {
@@ -403,7 +418,6 @@ int twols_parse_optionst::doit()
     show_ssa(
       goto_model,
       options,
-      heap_analysis,
       function,
       simplify,
       std::cout,
@@ -551,18 +565,18 @@ int twols_parse_optionst::doit()
     if(!options.get_bool_option("k-induction") &&
        !options.get_bool_option("incremental-bmc"))
       checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_ait(options, heap_analysis));
+        new summary_checker_ait(options));
     if(options.get_bool_option("k-induction") &&
        !options.get_bool_option("incremental-bmc"))
       checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_kindt(options, heap_analysis));
+        new summary_checker_kindt(options));
     if(!options.get_bool_option("k-induction") &&
        options.get_bool_option("incremental-bmc"))
       checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_bmct(options, heap_analysis));
+        new summary_checker_bmct(options));
     if(options.get_bool_option("nontermination"))
       checker=std::unique_ptr<summary_checker_baset>(
-        new summary_checker_nontermt(options, heap_analysis));
+        new summary_checker_nontermt(options));
 
     checker->set_message_handler(get_message_handler());
     checker->simplify=!cmdline.isset("no-simplify");
@@ -1561,11 +1575,7 @@ void twols_parse_optionst::help()
     " --heap                       use heap domain\n"
     " --zones                      use zone domain\n"
     " --octagons                   use octagon domain\n"
-    " --heap-interval              use heap domain with interval domain for\n"
-    "                              values\n"
-    " --heap-zones                 use heap domain with zones domain for values\n" // NOLINT(*)
-    " --heap-values-refine         use heap domain with a dynamic refinement\n"
-    "                              of strength of the value domain\n"
+    " --values-refine              use dynamic refinement of strength of the value domain\n" // NOLINT(*)
     " --sympath                    compute invariant for each symbolic path\n"
     "                              (only usable with --heap-* switches)\n"
     " --enum-solver                use solver based on model enumeration\n"

diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h
@@ -47,9 +47,7 @@ class optionst;
   "(octagons)" \
   "(equalities)" \
   "(heap)" \
-  "(heap-interval)" \
-  "(heap-zones)" \
-  "(heap-values-refine)" \
+  "(values-refine)" \
   "(sympath)" \
   "(enum-solver)(binsearch-solver)(arrays)"\
   "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \
@@ -192,9 +190,6 @@ class twols_parse_optionst:
   void remove_loops_in_entry(goto_modelt &goto_model);
   void create_dynamic_objects(goto_modelt &goto_model);
   void add_dynamic_object_rec(exprt &expr, symbol_tablet &symbol_table);
-  void add_dynamic_object_symbols(
-    const ssa_heap_analysist &heap_analysis,
-    goto_modelt &goto_model);
   void split_same_symbolic_object_assignments(goto_modelt &goto_model);
   void remove_dead_goto(goto_modelt &goto_model);
   void compute_dynobj_instances(

diff --git a/src/2ls/dynamic_cfg.h b/src/2ls/dynamic_cfg.h
@@ -14,6 +14,7 @@ Author: Peter Schrammel
 
 #include <util/std_expr.h>
 #include <util/graph.h>
+#include <util/i2string.h>
 #include <goto-programs/goto_program.h>
 
 #include <ssa/ssa_unwinder.h>

diff --git a/src/2ls/horn_encoding.cpp b/src/2ls/horn_encoding.cpp
@@ -63,8 +63,7 @@ void horn_encodingt::translate(
          ";\n";
 
   // compute SSA
-  ssa_heap_analysist heap_analysis(ns);
-  local_SSAt local_SSA(f_it->second, ns, options, heap_analysis, "");
+  local_SSAt local_SSA(f_it->second, ns, options, "");
 
   const goto_programt &body=f_it->second.body;