Allow to use any combination of simple domains

viktormalik · viktormalik · commit d6e7ad7c3d8c · 2020-03-30T17:49:43.000+02:00
The 2LS interface now allows to specify multiple simple domains to use.
These include --heap, --equalities, and all value domains. If mutliple
domains are specified, a product domain is created and invariants are
inferred in all domains in parallel.

Since the domains are created in template_generator_base while the
strategy solvers and abstract values are created in ssa_analyzer, it is
required that the order of simple domains/solvers/values within the
product domain/solver/value is always the same.

CLI options of all tests are ported to the new interface.
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);
@@ -1552,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)" \
diff --git a/src/2ls/summary_checker_ai.cpp b/src/2ls/summary_checker_ai.cpp
@@ -74,12 +74,12 @@ property_checkert::resultt summary_checker_ait::operator()(
     report_statistics();
 
     if(result==property_checkert::UNKNOWN &&
-       options.get_bool_option("heap-values-refine") &&
-       options.get_bool_option("heap-interval"))
+       options.get_bool_option("values-refine") &&
+       options.get_bool_option("intervals"))
     {
       summary_db.clear();
-      options.set_option("heap-interval", false);
-      options.set_option("heap-zones", true);
+      options.set_option("intervals", false);
+      options.set_option("zones", true);
     }
     else
     {
diff --git a/src/domains/product_domain.h b/src/domains/product_domain.h
@@ -39,7 +39,9 @@ class product_domaint:public domaint
   /// The order has to match the order of domains.
   struct valuet:domaint::valuet, std::vector<domaint::valuet *>
   {
-    using std::vector<domaint::valuet *>::vector;
+    valuet()=default;
+    explicit valuet(const std::vector<domaint::valuet *> &values):
+      vector(values) {}
 
     valuet *clone() override
     {
diff --git a/src/domains/ssa_analyzer.cpp b/src/domains/ssa_analyzer.cpp
diff --git a/src/domains/strategy_solver_simple.cpp b/src/domains/strategy_solver_simple.cpp
diff --git a/src/domains/template_generator_base.cpp b/src/domains/template_generator_base.cpp
diff --git a/src/domains/template_generator_base.h b/src/domains/template_generator_base.h
