Siemens fix260 squashed (do not merge) #291

lucasccordeiro · 2016-11-02T03:47:22Z

No description provided.

Signed-off-by: Lucas Cordeiro <[email protected]>

…ing the dependence graph Signed-off-by: Lucas Cordeiro <[email protected]>

Signed-off-by: Lucas Cordeiro <[email protected]>

…tatements' Signed-off-by: Lucas Cordeiro <[email protected]>

Signed-off-by: Lucas Cordeiro <[email protected]>

tautschnig

The tests should definitively get merged (even though there's a design decision to be made whether they should genuinely be in a separate directory or just be part of the cbmc/ folder. For the code there are a couple of questions for discussion, and linting is necessary.

tautschnig · 2017-01-19T15:34:37Z

src/goto-instrument/full_slicer.cpp

@@ -400,6 +429,9 @@ void full_slicert::operator()(
  Forall_goto_functions(f_it, goto_functions)
    if(f_it->second.body_available())
    {
+   	  if(f_it->first=="pthread_create")
+   		throw "--full-slice does not support C/Pthreads yet";
+


The indent seems wrong here.

This was fixed in https://github.com/lucasccordeiro/cbmc/tree/dependence-graph-fix

tautschnig · 2017-01-19T15:35:20Z

src/goto-instrument/full_slicer.cpp

 {
  // some variables are used during symbolic execution only

+  const irep_idt &statement=target->code.get(ID_statement);
+  if (statement==ID_array_copy) return true;


Why does array_copy need to be singled out?

See #260. There are two test cases that expose this bug in the full slicer: realloc1 and realloc2. If we do not add that check, the full slicer incorrectly cuts all expressions related to array_copy.

tautschnig · 2017-01-19T15:36:44Z

src/goto-instrument/full_slicer.cpp

@@ -322,18 +329,38 @@ Function: implicit

 \*******************************************************************/

-static bool implicit(goto_programt::const_targett target)
+static bool implicit(const namespacet &ns, goto_programt::const_targett target)
 {
  // some variables are used during symbolic execution only


This function now seems to be doing a lot more than what it originally was intended for!

I have added an explanation in #260. As I reported in the issue, I'm not completely sure whether this is correct or not.

tautschnig · 2017-01-19T15:37:48Z

src/goto-instrument/full_slicer.cpp

+  const irep_idt &statement=target->code.get(ID_statement);
+  if (statement==ID_array_copy) return true;
+
+  if (target->is_assume()) return true;


Why is that the case? It should not be forced into the slice when there is a control dependency on the condition represented by the assume. Except for bugs, the control-dependency code should be handling this.

The control-flow dependency code is not handling this. Should we open a bug for this issue then?

tautschnig · 2017-01-19T15:38:35Z

src/goto-instrument/full_slicer.cpp

  if(!target->is_assign()) return false;

  const code_assignt &a=to_code_assign(target->code);
+  if(a.lhs().id()==ID_dereference) return true;


This seems excessive.

tautschnig · 2017-01-19T15:54:36Z

src/goto-instrument/full_slicer.cpp

  if(a.lhs().id()!=ID_symbol) return false;

  const symbol_exprt &s=to_symbol_expr(a.lhs());

-  return s.get_identifier()==CPROVER_PREFIX "rounding_mode";
+  if (s.source_location().get_function().empty())


Why is this restriction required?

We were incorrectly slicing all global variables inside the __CPROVER_initialize function. Specifically, the call to s.source_location().get_function().empty() returns true for __CPROVER_initialize function.

The fact that those variables have been wrongly sliced away is a bug, and I'm not sure it actually exists any longer - the bugfix should be via 50383ed. Can you confirm that this change is still necessary?

tautschnig · 2017-01-19T15:55:04Z

src/goto-instrument/full_slicer.cpp

+
+    // static lifetime?
+    if(ns.lookup(s.get_identifier()).is_static_lifetime)
+      return true;


Why can't those variables not be sliced away?

The problem is that we were slicing all global variables inside the __CPROVER_initialize function. This was causing a large number of incorrect results for the full-slice option.

See above - I think this has been fixed via 50383ed.

tautschnig · 2017-01-19T15:57:27Z

src/cbmc/cbmc_parse_options.cpp

+    // add generic checks
+    status() << "Generic Property Instrumentation" << eom;
+    goto_check(ns, options, goto_functions);
+


Why is this code new?

Here we have to ensure that we call the full-slice option just after instrumenting the code with goto_check; otherwise, we the full-slice cuts all assignments that are relevant to checking a given property.

tautschnig · 2017-01-19T15:58:22Z

src/goto-instrument/full_slicer.cpp

-      it!=d_node.in.end();
-      ++it)
-    add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
+  if (dep_graph.state_exist(node.PC))


Is it truly possible that a state doesn't exist?

I have removed this code in https://github.com/lucasccordeiro/cbmc/tree/dependence-graph-fix.

tautschnig · 2017-01-19T15:58:53Z

src/analyses/ai.h

@@ -274,6 +274,14 @@ class ait:public ai_baset
    ai_baset::clear();
  }

+  // this one just finds states
+  virtual const bool state_exist(locationt l) const


I think this should be state_exists (with an s)

This piece of code was already removed in https://github.com/lucasccordeiro/cbmc/tree/dependence-graph-fix

kroening · 2017-01-20T10:35:20Z

@lucasccordeiro perhaps as a first easy step, may I have a separate PR for the tests, please?

lucasccordeiro · 2017-01-27T14:02:03Z

@kroening and @tautschnig: I have just created PR #479 to add test cases to check the full-slice option. In particular, I have added all test cases into the cbmc regression suite to make sure that we always test the full-slice option.

forejtv · 2017-04-04T16:36:38Z

@lucasccordeiro can you rebase, please?

lucasccordeiro · 2017-04-05T08:05:49Z

@forejtv: I have created a set of small PRs related to this large PR. We had 5 small PRs ( 211cb90, 27227cc, e70aa7d, ad384f1, b4ae916) that were already merged about this large PR. I intend to go back to this work once I fix the issues assigned to me for the GS upgrade.

SEC-16: Preparation steps for load analysed web apps with libraries included.

hannes-steffenhagen-diffblue · 2021-02-25T13:23:32Z

Closing for now, the PR description doesn't make it clear what the added value for this and there's been no movement on this PR since 2017.

lucasccordeiro added 22 commits December 28, 2016 16:37

added ignore for input in value_set_fit::apply_code

97963ff

Signed-off-by: Lucas Cordeiro <[email protected]>

do not remove assignments related to __CPROVER_initialize

62b3cea

Signed-off-by: Lucas Cordeiro <[email protected]>

remove virtual functions, function pointers, and returns before build…

8076914

…ing the dependence graph Signed-off-by: Lucas Cordeiro <[email protected]>

add test cases to check the full-slice option

fa10441

Signed-off-by: Lucas Cordeiro <[email protected]>

add test case slice12

f826a4e

Signed-off-by: Lucas Cordeiro <[email protected]>

check whether symbol is a __CPROVER_rounding_mode

e126a1e

Signed-off-by: Lucas Cordeiro <[email protected]>

add test case slice13

b53ac91

Signed-off-by: Lucas Cordeiro <[email protected]>

remove unused files from slice13

bdc6b83

Signed-off-by: Lucas Cordeiro <[email protected]>

add makefile to cbmc-slice

226b3f9

Signed-off-by: Lucas Cordeiro <[email protected]>

do not remove assignments related to dereference

efb1fc4

Signed-off-by: Lucas Cordeiro <[email protected]>

add test case slice14

42af01e

Signed-off-by: Lucas Cordeiro <[email protected]>

add test case slice15

0f2ea7b

Signed-off-by: Lucas Cordeiro <[email protected]>

add test case slice16 from the paper 'On Slicing Programs with Jump S…

a77eb88

…tatements' Signed-off-by: Lucas Cordeiro <[email protected]>

add function calls to the queue before computing the dependency graph

a9c1ea7

Signed-off-by: Lucas Cordeiro <[email protected]>

update test desc for full-slice

83d5b2e

Signed-off-by: Lucas Cordeiro <[email protected]>

remove function pointers by adding the safety assertion

5a82815

Signed-off-by: Lucas Cordeiro <[email protected]>

add test case related to equality through union

d59dd58

Signed-off-by: Lucas Cordeiro <[email protected]>

consider assume statements during symbolic execution

be2709c

Signed-off-by: Lucas Cordeiro <[email protected]>

add test case related to the exit function

fada618

Signed-off-by: Lucas Cordeiro <[email protected]>

execute full-slice after goto_check

ed9b801

Signed-off-by: Lucas Cordeiro <[email protected]>

check whether a given state exists before adding dependencies

c57f663

Signed-off-by: Lucas Cordeiro <[email protected]>

fix merge conflict in cbmc_parse_options.cpp

517fbd2

Signed-off-by: Lucas Cordeiro <[email protected]>

lucasccordeiro force-pushed the siemens_fix260_squashed branch from 1da9076 to 517fbd2 Compare December 28, 2016 16:41

check for array_copy during the implicit call

3bbca7c

Signed-off-by: Lucas Cordeiro <[email protected]>

tautschnig requested changes Jan 19, 2017

View reviewed changes

tautschnig assigned lucasccordeiro Feb 1, 2017

lucasccordeiro changed the title ~~Siemens fix260 squashed~~ Siemens fix260 squashed (do not merge) Jul 4, 2017

tautschnig changed the base branch from master to develop August 22, 2017 12:35

smowton pushed a commit to smowton/cbmc that referenced this pull request May 9, 2018

Merge pull request diffblue#291 from diffblue/feature/include_libs

3196528

SEC-16: Preparation steps for load analysed web apps with libraries included.

hannes-steffenhagen-diffblue closed this Feb 25, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Siemens fix260 squashed (do not merge) #291

Siemens fix260 squashed (do not merge) #291

lucasccordeiro commented Nov 2, 2016

tautschnig left a comment

tautschnig Jan 19, 2017

lucasccordeiro Jan 30, 2017

tautschnig Jan 19, 2017

lucasccordeiro Jan 30, 2017

tautschnig Jan 19, 2017

lucasccordeiro Jan 30, 2017

tautschnig Jan 19, 2017

lucasccordeiro Jan 30, 2017

tautschnig Jan 19, 2017

tautschnig Jan 19, 2017

lucasccordeiro Jan 30, 2017

tautschnig Feb 1, 2017

tautschnig Jan 19, 2017

lucasccordeiro Jan 30, 2017

tautschnig Feb 1, 2017

tautschnig Jan 19, 2017

lucasccordeiro Jan 30, 2017

tautschnig Jan 19, 2017

lucasccordeiro Jan 30, 2017

tautschnig Jan 19, 2017

lucasccordeiro Jan 30, 2017

kroening commented Jan 20, 2017

lucasccordeiro commented Jan 27, 2017

forejtv commented Apr 4, 2017

lucasccordeiro commented Apr 5, 2017

hannes-steffenhagen-diffblue commented Feb 25, 2021

Siemens fix260 squashed (do not merge) #291

Siemens fix260 squashed (do not merge) #291

Conversation

lucasccordeiro commented Nov 2, 2016

tautschnig 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

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

kroening commented Jan 20, 2017

lucasccordeiro commented Jan 27, 2017

forejtv commented Apr 4, 2017

lucasccordeiro commented Apr 5, 2017

hannes-steffenhagen-diffblue commented Feb 25, 2021