Improvements to the shape abstract domain and to memory safety analysis #120

viktormalik · 2018-07-20T06:18:47Z

Multiple improvements and bug fixes mainly related to dynamic memory analysis. Changes are mostly related to the paper submitted to FMCAD'18.
Main contributions are:

Analysis of pointer and free safety for abstract dynamic objects.
Splitting abstract dynamic objects into multiple when it is needed for a sound analysis.
Added examples that need combined reasoning about shape and value properties.

This is useful when analysing pointer and memory safety, respectively.

If there is and incompatibility between the type of the template row expression and the address of pointed object, use typecast. This is currently used when dealing with CPROVER-specific pointer variables, which are of (void *) type. Hence, we allow incompatible type returned by the solver for these variables only.

When adding paths from other row, remove the other row as a destination if it has been added to another path. When clearing pointed rows, do not clear itself and remove poining row from the pointed_by set.

This information is used to prevent creation of PHI nodes for dynamic objects for 'if' branches in case where the object allocation occurs in one incoming branch only.

… condition This prevents from getting non-deterministic values of dynamic object fields incoming from other branches (where the dynamic object was not allocated) during analysis.

…ignment This is needed for correct RHS concretisation.

This test demonstrates the power of the combination of pointer and interval domains.

…object The concrete object has "$co" suffix and there is always only one allocated. It is created non-deterministically, but with the condition that no other pointer in the loop points to this object (i.e. it has not been allocated before).

…n template These guards are used in the post-condition of template rows of the heap domain that contain members of dynamic objects in the same loop where the object was allocated. This is required to make sure that the object is analysed only when it is created.

Modify assertions for dereferencing deallocated objects to perform checks on concrete objects only. Since a concrete object allocated within a loop has a non-deterministic position within the abstract object, this approach is sound.

…ression A pair is stored as an "and" expression. This is used to track dependency between a pair of pointer variables.

… pointers This is useful to prove that a deallocated object is never dereferenced. Since the assertions checks for this property are done on conrete objects only, we need to prove that once a concrete object was deallocated, it cannot be reached in the next iteration.

It shows that tracking the points-to relation is enough since we use abstract objects and a path is expressed by field of an abstract object pointing to the same object.

Tests check pointer safety for linked lists.

… sides.

This version of the test did not previously work because of a bug related to symbolic dereference objects occuring on both sides of an assignment.

…ides The bug was related to finding the symbol at LHS (since there may be multiple chained members and we need to get to the root object).

…s reachable Loop guards collected in the SSA form are pairs (loop-select and loop head guards). When checking the solver for symbolic path, both guards must be true to set the appropriate loop-select guard in the sympath.

GOTO instructions having "false" as guard are removed since some of them were backwards jumps treated as loops.

Previously, we set free::record to true, which in case of multiple frees in a loop caused just the last free to be recorded into the invariant. Now, we let free::record to be undefined, but instead update template rows for __CPROVER_deallocated only if one of free::record in the loop is true.

Currently, this is a part of heap-interval domain. This should be refactored to heap-polyhedra domain in future.

Disabling 'packet_filter' since it takes more than 500 seconds. Moving failing version of running example from 'heap' to 'heap-data'.

Now, the format is: malloc_value = cond1 ? (void *)&dyn_obj1 : (cond2 ? (void *)&dyn_obj2 ....) Also use read_rhs when collecting allocation guards to obtain correct versions of variables occuring in guards (this is needed when dealing with #co objects since their guards contain other pointers).

Multiple tests end inconclusive due to dynamic object splitting.

For more detail see 6f8efca. This strenghtens the condition for not creating a PHI node for a dynamic object field when merging branches of a conditional in case the object was allocated in one branch only.

We cannot iterate container while changing it.

The renaming commit probably forgot to delete the fmcad18 directory.

peterschrammel · 2018-07-21T15:17:46Z

regression/heap/dll1_simple/test.desc

@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG


Why do these fail now? Please create an issue for them so that the bug can be fixed.

These fail because we split abstract dynamic objects into multiple and such abstraction is not strong enough to reason about these programs. Should I create an issue for a stronger shape domain?

peterschrammel · 2018-07-21T15:18:11Z

regression/memsafety/built_from_end/main.c

+  }
+
+}
+


spurious newline (several occurrences)

peterschrammel · 2018-07-21T15:20:54Z

src/2ls/2ls_parse_options.cpp

@@ -1745,6 +1804,8 @@ void twols_parse_optionst::help()
    " --zones                      use zone domain\n"
    " --octagons                   use octagon domain\n"
    " --heap-interval              use heap domain with interval domain for values\n" // NOLINT(*)
+    " --heap-zones                 use heap domain with zones domain for values\n" // NOLINT(*)
+    " --heap-zones                 use heap domain with dynamically incrementing stregth of value domain\n" // NOLINT(*)


--heap-values-incremental?
stregth -> strength

peterschrammel · 2018-07-21T15:21:31Z

src/2ls/2ls_parse_options.h

@@ -37,7 +38,8 @@ class optionst;
  "(version)" \
  "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
  "(ppc-macos)(unsigned-char)" \
-  "(havoc)(intervals)(zones)(octagons)(equalities)(heap)(heap-interval)"\
+  "(havoc)(intervals)(zones)(octagons)(equalities)"\


put each option on a separate line to simplify merging in future

peterschrammel · 2018-07-21T15:23:54Z

src/domains/strategy_solver_heap.cpp

+bool strategy_solver_heapt::is_cprover_symbol(const exprt &expr)
+{
+  return expr.id()==ID_symbol &&
+         id2string(to_symbol_expr(expr).get_identifier()).find("__CPROVER_")==0;


Use has_prefix() and CPROVER_PREFIX

peterschrammel · 2018-07-21T15:25:08Z

src/ssa/dynobj_instance_analysis.cpp

+
+    // Do not include CPROVER symbols
+    if(lhs.id()==ID_symbol &&
+       id2string(to_symbol_expr(lhs).get_identifier()).find("__CPROVER")!=


peterschrammel · 2018-07-21T15:26:26Z

src/ssa/dynobj_instance_analysis.cpp

@@ -0,0 +1,318 @@
+/*******************************************************************\
+
+Module: Analysis of a number of instances of abstract dynamic objects.


the number ?

peterschrammel · 2018-07-21T15:27:13Z

src/ssa/dynobj_instance_analysis.h

@@ -0,0 +1,192 @@
+/*******************************************************************\
+
+Module: Analysis of a number of instances of abstract dynamic objects.


…R-specific.

peterschrammel · 2018-07-30T17:38:52Z

regression/Makefile

@@ -1,5 +1,6 @@
-DIRS = heap nontermination termination kiki \
-       preconditions interprocedural invariants
+DIRS = nontermination termination kiki \


Put every directory on a separate line

peterschrammel · 2018-07-30T17:40:04Z

regression/heap-data/calendar/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--heap-values-incremental --sympath --inline


I'm not sure -incremental is a good name, maybe better -refine? (or add a --refine-domains option -- see below)

I changed the name to -refine. I suggest we leave implementation of a more generic solution with --refine-domains switch to Matej as a part of his work on generic domain combinations. This is closely related to it and I think it should be designed all together.

peterschrammel · 2018-07-30T17:44:39Z

src/2ls/2ls_parse_options.cpp

-    }
-
-    if(cmdline.isset("horn-encoding"))
+    while(!finished)


This must not be implemented here, but inside summary_checker_ait. I'd generalise this right away by adding a --refine-domains option.

peterschrammel · 2018-07-30T17:46:04Z

src/2ls/2ls_parse_options.cpp

+    if(options.get_bool_option("pointer-check"))
+    {
+      allow_record_malloc(goto_model);
+//      allow_record_free(goto_model);


Why is this commented out? Use #if 0 plus a comment to justify the deactivation or remove this line.

peterschrammel · 2018-07-30T17:47:33Z

src/2ls/2ls_parse_options.cpp

@@ -1243,6 +1286,21 @@ bool twols_parse_optionst::process_goto_program(
      inline_main(goto_model);


Weird indent in the lines above

I don't see any bad indentation

peterschrammel · 2018-07-30T17:57:52Z

src/ssa/dynobj_instance_analysis.cpp

+        bool found=false;
+        for(const auto &i : must_alias_relations)
+        {
+          unsigned long n;


size_t? (further instances below)

peterschrammel · 2018-07-30T17:59:32Z

src/ssa/dynobj_instance_analysis.h

+\*******************************************************************/
+class must_alias_setst:public union_find<exprt>
+{
+protected:


I prefer the public section to come first.

peterschrammel · 2018-07-30T18:00:13Z

src/ssa/dynobj_instance_analysis.h

+  friend class dynobj_instance_domaint;
+};
+
+


superfluous blank line

peterschrammel · 2018-07-30T18:02:44Z

src/ssa/malloc_ssa.cpp

+
+void set_var_always_to_true(
+  goto_modelt &goto_model,
+  bool (*name_cond)(std::string &))


std::function preferred

peterschrammel · 2018-07-30T18:03:42Z

src/ssa/ssa_value_set.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_2LS_SSA_SSA_VALUE_SET_H

 #include <analyses/ai.h>
+#include <iostream>


seems unused, please remove

…d classes.

… domains. Rename --heap-values-incremental to --heap-values-refine. Move refinement into summary_checker_ai.

1. Move long and utility functions into dedicated modules 2. Add braces for multi-line statements and multi-line conditionals 3. Remove commented code 4. Use better types (size_t instead of unsigned) 5. Replace function pointer by std::function

peterschrammel

a few nitpicks

peterschrammel · 2018-08-04T10:41:25Z

src/2ls/2ls_parse_options.cpp

-    " --heap-interval              use heap domain with interval domain for values\n" // NOLINT(*)
-    " --sympath                    compute invariant for each symbolic path (only usable with --heap-interval switch)" // NOLINT(*)
+    " --heap-interval              use heap domain with interval domain for"
+      "values\n"


I'd align values with use in the output

peterschrammel · 2018-08-04T10:41:56Z

src/2ls/2ls_parse_options.cpp

@@ -1744,8 +1773,14 @@ 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 values\n" // NOLINT(*)
-    " --sympath                    compute invariant for each symbolic path (only usable with --heap-interval switch)" // NOLINT(*)
+    " --heap-interval              use heap domain with interval domain for"


\n at the end of the line

peterschrammel · 2018-08-04T10:42:09Z

src/2ls/2ls_parse_options.cpp

-    " --sympath                    compute invariant for each symbolic path (only usable with --heap-interval switch)" // NOLINT(*)
+    " --heap-interval              use heap domain with interval domain for"
+      "values\n"
+    " --heap-zones                 use heap domain with zones domain for values"


\n at the end of the line

peterschrammel · 2018-08-04T10:42:21Z

src/2ls/2ls_parse_options.cpp

+      "values\n"
+    " --heap-zones                 use heap domain with zones domain for values"
+      "\n"
+    " --heap-values-refine         use heap domain with a dynamically"


\n at the end of the line

peterschrammel · 2018-08-04T10:42:28Z

src/2ls/2ls_parse_options.cpp

+    " --heap-zones                 use heap domain with zones domain for values"
+      "\n"
+    " --heap-values-refine         use heap domain with a dynamically"
+      "refinement of the strength of the value domain\n"


align output

peterschrammel · 2018-08-04T10:42:34Z

src/2ls/2ls_parse_options.cpp

+      "\n"
+    " --heap-values-refine         use heap domain with a dynamically"
+      "refinement of the strength of the value domain\n"
+    " --sympath                    compute invariant for each symbolic path"


\n at the end of the line

peterschrammel · 2018-08-04T10:42:41Z

src/2ls/2ls_parse_options.cpp

+    " --heap-values-refine         use heap domain with a dynamically"
+      "refinement of the strength of the value domain\n"
+    " --sympath                    compute invariant for each symbolic path"
+      "(only usable with --heap-interval switch)"


align output

viktormalik added 30 commits July 20, 2018 07:53

Set "record_malloc" and "record_may_leak" variables to true

64daeeb

This is useful when analysing pointer and memory safety, respectively.

Heap domain: improve transitive row updating

424cf5e

When adding paths from other row, remove the other row as a destination if it has been added to another path. When clearing pointed rows, do not clear itself and remove poining row from the pointed_by set.

Track allocation sites of dynamic objects in assignmenst and SSA domain

b624ec9

This information is used to prevent creation of PHI nodes for dynamic objects for 'if' branches in case where the object allocation occurs in one incoming branch only.

For dynamic objects allocated in a loop, add allocation guard to post…

942511d

… condition This prevents from getting non-deterministic values of dynamic object fields incoming from other branches (where the dynamic object was not allocated) during analysis.

Add possibility to use object created in given SSA node at RHS of ass…

5e6503e

…ignment This is needed for correct RHS concretisation.

Copy pointed info to member expression on symbolic dereference

66a12ca

Add new test to heap directory

26684c8

This test demonstrates the power of the combination of pointer and interval domains.

Heap domain: allow template row to contain a pair of variables as exp…

b3eff2a

…ression A pair is stored as an "and" expression. This is used to track dependency between a pair of pointer variables.

Allow recording free

5ba86f4

Do not use pointer access paths in the heap domain

1a282c0

It shows that tracking the points-to relation is enough since we use abstract objects and a path is expressed by field of an abstract object pointing to the same object.

Make unwinder to handle "object-select" guard

7ade32c

Add tests for memory safety

8705014

Tests check pointer safety for linked lists.

Add another example to heap that uses domain combination

18b148b

Split assignments having the same symbolic dereference object on both…

0be684c

… sides.

Update process_queue test

06e0128

This version of the test did not previously work because of a bug related to symbolic dereference objects occuring on both sides of an assignment.

Fix bug in splitting assignments having same symbolic deref on both s…

0ce8606

…ides The bug was related to finding the symbol at LHS (since there may be multiple chained members and we need to get to the root object).

Remove dead GOTO instructions

ebb2d97

GOTO instructions having "false" as guard are removed since some of them were backwards jumps treated as loops.

Remove dead GOTO instruction only for backwards goto

56210f3

Create new regression directory with benchmark for SAS 2018 paper

d04098e

Add combination of heap and zones domain

d6428b5

Currently, this is a part of heap-interval domain. This should be refactored to heap-polyhedra domain in future.

Modify SAS 2018 tests to use __VERIFIER_error instead of assert

4cb88ab

Add 2 more tests to SAS'18 benchmark

ff40be0

Add new example to SAS'18 benchmark

2bfac82

viktormalik added 14 commits July 20, 2018 07:53

Add missing function comments.

16ffaa1

Adjust coding style.

6b67494

Heap-data tests: disable long test and move one from 'heap' directory

b414e3c

Disabling 'packet_filter' since it takes more than 500 seconds. Moving failing version of running example from 'heap' to 'heap-data'.

Remove debugging output

14bad7b

Add one test to memsafety and disable failing tests.

bc085cd

Multiple tests end inconclusive due to dynamic object splitting.

Splitting dynamic objects: do not fail on array-typed dynamic objects.

719684c

Add memsafety and heap-data to main regression Makefile

4fe5103

Fix bug in creating PHI nodes for dynamic objects in some 'if' branches

dd533c8

For more detail see 6f8efca. This strenghtens the condition for not creating a PHI node for a dynamic object field when merging branches of a conditional in case the object was allocated in one branch only.

Disable competition mode that kills programs with pointer arithmetic

54c9a2e

Fix bug in dynobj_instance_analysis.

d70047e

We cannot iterate container while changing it.

Fix bug in dynobj_instance_analysis.

40facd1

We cannot iterate container while changing it.

Adjust code style for latest fix.

9572ea2

Remove fmcad18 directory, it has already been replaced by heap-data.

c9a7d89

The renaming commit probably forgot to delete the fmcad18 directory.

peterschrammel reviewed Jul 21, 2018

View reviewed changes

peterschrammel assigned viktormalik Jul 21, 2018

viktormalik added 4 commits July 23, 2018 08:09

Remove spurious newlines from some tests in memory categories.

c71334c

Fix errors in command line options.

d022890

Use has_prefix and CPROVER_PREFIX to check whether a symbol is CPROVE…

ed80b24

…R-specific.

Remove debugging output.

556c9c7

peterschrammel reviewed Jul 30, 2018

View reviewed changes

peterschrammel assigned viktormalik and unassigned viktormalik Jul 30, 2018

viktormalik added 3 commits August 3, 2018 09:48

Rename heap-interval to heap-tpolyhedra including names of all relate…

9104bda

…d classes.

Refactor combination of heap domain with increasing strength of value…

cbb660c

… domains. Rename --heap-values-incremental to --heap-values-refine. Move refinement into summary_checker_ai.

Code cleanup

d938e3e

1. Move long and utility functions into dedicated modules 2. Add braces for multi-line statements and multi-line conditionals 3. Remove commented code 4. Use better types (size_t instead of unsigned) 5. Replace function pointer by std::function

peterschrammel reviewed Aug 4, 2018

View reviewed changes

Help formatting.

215ab5d

peterschrammel approved these changes Aug 13, 2018

View reviewed changes

peterschrammel merged commit 6aa1f00 into diffblue:master Aug 13, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Improvements to the shape abstract domain and to memory safety analysis #120

Improvements to the shape abstract domain and to memory safety analysis #120

viktormalik commented Jul 20, 2018

peterschrammel Jul 21, 2018

viktormalik Jul 23, 2018

peterschrammel Jul 21, 2018

peterschrammel Jul 21, 2018

peterschrammel Jul 21, 2018

peterschrammel Jul 21, 2018

peterschrammel Jul 21, 2018

peterschrammel Jul 21, 2018

peterschrammel Jul 21, 2018

peterschrammel Jul 30, 2018

peterschrammel Jul 30, 2018

viktormalik Aug 3, 2018

peterschrammel Jul 30, 2018

peterschrammel Jul 30, 2018

peterschrammel Jul 30, 2018

viktormalik Aug 3, 2018

peterschrammel Jul 30, 2018

peterschrammel Jul 30, 2018

peterschrammel Jul 30, 2018

peterschrammel Jul 30, 2018

peterschrammel Jul 30, 2018

peterschrammel left a comment

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

peterschrammel Aug 4, 2018

		@@ -0,0 +1,318 @@
		/*******************************************************************\

		Module: Analysis of a number of instances of abstract dynamic objects.

		@@ -0,0 +1,192 @@
		/*******************************************************************\

		Module: Analysis of a number of instances of abstract dynamic objects.

		@@ -1243,6 +1286,21 @@ bool twols_parse_optionst::process_goto_program(
		inline_main(goto_model);

		@@ -1,4 +1,4 @@
		CORE
		KNOWNBUG

Improvements to the shape abstract domain and to memory safety analysis #120

Improvements to the shape abstract domain and to memory safety analysis #120

Conversation

viktormalik commented Jul 20, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment