consider array_set expressions in the full-slice (do not merge) #898

lucasccordeiro · 2017-05-09T15:40:00Z

handle array_set expressions during the function call
in the full-slicert class. Added one test case into
goto-instrument regression for checking array_set expressions
using the full-slice option.

tautschnig · 2017-05-09T16:40:35Z

src/goto-instrument/full_slicer.cpp

@@ -60,6 +60,10 @@ void full_slicert::add_function_calls(
  queuet &queue,
  const goto_functionst &goto_functions)
 {
+  // do not retain calls of empty functions
+  if(node.PC->function.empty())


I'm not sure whether the comment is misleading or the code might not do what you'd expect it to do? This tests whether the function name set for a particular instruction is empty, which is unrelated to the function being called not having a function body.

tautschnig · 2017-05-09T16:41:17Z

src/pointer-analysis/value_set_fi.cpp

@@ -1727,7 +1727,7 @@ void value_set_fit::apply_code(
  else if(statement==ID_fence)
  {
  }
-  else if(statement==ID_array_copy)
+  else if(statement==ID_array_copy || statement==ID_array_set)


This fix should be applied in value_set.cpp as well.

As just discussed on Skype, this is actually already the case.

tautschnig

This PR includes a binary blob without corresponding source. This is bound to cause license trouble.

lucasccordeiro · 2017-05-10T14:36:27Z

@tautschnig: I have replaced the goto binary by a Java program in the regression suite, which exposes the error. I have proposed a temporary fix to the problem so that we can evaluate the application of the slicer to the security benchmarks.

I need to talk to @peterschrammel to check about the Java library implementation. It seems that if we verify a Java program that does not contain the library implementation in CBMC, then we get nil expressions as:

node.PC->code.is_nil(): 1
node.PC->code.pretty(): nil

Since the full slicer does implicitly assume expression well-formedness, then we get some assertion violations in the code.

lucasccordeiro · 2017-05-11T09:24:56Z

@tautschnig: I have discussed this issue with our Java team (note that we have four or five teams at DiffBlue :-). The nil expressions are produced for those functions that do not contain a body. As @mgudemann has explained, those nil expressions are kept just to reproduce the trace of the Java program.

What we do now is to check for a nil expression in the add_function_calls as follows:

 if(node.PC->code.is_nil())
    return;

In some sense, it is similar to the way that add_decl_dead currently works:

  if(decl_dead.empty())
    return;

Let us know your thoughts and if you have a better solution in mind.

Many thanks for your support.

lucasccordeiro · 2017-05-11T09:43:07Z

@tautschnig: These are some questions that our team has about the dependence graph, which I'm unsure how to properly answer:

(1) What does the dependency analysis compute if a function has no body?
(2) Is it sound to consider functions without body?

lucasccordeiro · 2017-05-11T10:44:45Z

Here is a simple example of how the slicer in this PR works for functions of the Java library that are not implemented.

public class testSlice
{
  public static void main(String[] args)
  {
     char c = 0;
     if (Character.isDefined(c)==true)
       assert true;
     else
       assert false;
  }
}

Since there is no implementation for Character.isDefined, then the Java front-end instruments that method with nondet return value and side effects.

The slicer replaces Character.isDefined(c) by return_tmp0 = NONDET(boolean) and it keeps the dependence on the expression return_tmp0 = NONDET(boolean) since return_tmp0 is used to guard the if-else-statement.

tautschnig · 2017-05-11T10:56:17Z

The nil expressions are produced for those functions that do not contain a body. As @mgudemann has explained, those nil expressions are kept just to reproduce the trace of the Java program.

Interesting. Increases the urgency of #751.

(1) What does the dependency analysis compute if a function has no body?

As the dependency analysis is based on def-use, a function call to a function without body may introduce uses (all arguments) and a definition (the return value).

(2) Is it sound to consider functions without body?

Working with functions without body is never sound.

martin-cs · 2017-05-15T06:28:40Z

On Thu, 2017-05-11 at 02:43 -0700, Lucas Cordeiro wrote: @tautschnig: These are some questions that our team has about the dependence graph, which I'm unsure how to properly answer: (1) What does the dependency analysis compute if a function has no body?

You might want to chat with @danpoe about this as he fixed the same issue elsewhere.

(2) Is it sound to consider functions without body?

<pedantry> Personally I avoid using the words "sound" and "complete" as they have been hijacked and twisted (because everyone wants a technique that is "sound but not complete"). I'd suggest "over-approximate" or "under-approximate". Can you correctly handle functions without a body in over-approximate analysis -- yes but you have to assume that they could introduce dependencies between *anything*, so your results are likely to be ... less helpful than you wanted. </pedantry>

lucasccordeiro · 2017-05-15T07:50:02Z

@martin-cs and @tautschnig: many thanks for your reply.

Last Friday we had a meeting at DiffBlue together with @peterschrammel. We decided that our security scanner team is going to provide a summary for all those functions that do not have a body so that we can properly use the full-slicer for the taint analysis of Java programs.

Later on I'm going to update this PR to reflect the result of that meeting.

lucasccordeiro · 2017-05-15T16:30:15Z

@tautschnig: May I ask you to review this PR? Here is a summary of all changes:

(1) removed checks related to the empty function body (as discussed before in this issue);
(2) added function calls to the full-slicer working queue;
(3) combined the full-slice with reachability-slice;
(4) added new test cases and enabled existing test cases in the goto-instrument regression suite.

tautschnig · 2017-05-22T12:13:59Z

regression/cbmc-java/slice1/test.desc

@@ -0,0 +1,6 @@
+KNOWNBUG


It seems rather impossible to infer what the problem here is from the commit message. Please either make the commit message more verbose or add comments to test.desc.

tautschnig · 2017-05-22T12:15:30Z

src/cbmc/cbmc_parse_options.cpp

@@ -905,6 +906,12 @@ bool cbmc_parse_optionst::process_goto_program(
    {
      status() << "Performing a full slice" << eom;
      full_slicer(goto_functions, ns);
+
+      status() << "Performing a reachability slice" << eom;
+       if(cmdline.isset("property"))


I think this should be done before doing a full slice, and possibly should always be done (irrespective of whether full-slice is used or not).

The indent is weird.

tautschnig · 2017-05-22T12:16:05Z

src/goto-instrument/goto_instrument_parse_options.cpp

+    else
+      reachability_slicer(goto_functions);
+  }
+


Why has this been moved?

tautschnig · 2017-05-22T12:16:53Z

src/goto-instrument/full_slicer.cpp

@@ -399,6 +399,8 @@ void full_slicert::operator()(
      const exprt &s=to_code_dead(e_it->first->code).symbol();
      decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
    }
+    else if(e_it->first->is_function_call())
+      add_to_queue(queue, e_it->second, e_it->first);


Add a comment that this assumes that a rechability slice has been performed, for it would otherwise add way too much to the slice.

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

lucasccordeiro · 2017-07-04T10:28:11Z

The original intention of this PR was to consider array_set expressions to enable the full-slice option. This has already been merged into CBMC (https://github.com/diffblue/cbmc/blob/master/src/pointer-analysis/value_set_fi.cpp#L1507). We have now to investigate the combination of the reachability and full slicer, which I'll try to handle in a different PR.

tautschnig requested changes May 9, 2017

View reviewed changes

lucasccordeiro force-pushed the fix-full-slice-06 branch from 1c4561f to 7f74d7f Compare May 10, 2017 09:34

tautschnig requested changes May 10, 2017

View reviewed changes

lucasccordeiro force-pushed the fix-full-slice-06 branch from 7f74d7f to 6c3ff3c Compare May 10, 2017 14:25

lucasccordeiro force-pushed the fix-full-slice-06 branch 2 times, most recently from a98ed38 to 101c652 Compare May 11, 2017 09:13

lucasccordeiro force-pushed the fix-full-slice-06 branch from 101c652 to 899b56b Compare May 12, 2017 08:11

lucasccordeiro force-pushed the fix-full-slice-06 branch 3 times, most recently from 853ce4e to 8847542 Compare May 15, 2017 14:29

lucasccordeiro force-pushed the fix-full-slice-06 branch 3 times, most recently from 08db915 to 3d38441 Compare May 16, 2017 09:35

tautschnig requested changes May 22, 2017

View reviewed changes

peterschrammel assigned lucasccordeiro Jun 25, 2017

lucasccordeiro mentioned this pull request Jun 29, 2017

added function call to working queue in the full-slicer #702

Closed

lucasccordeiro added 3 commits July 4, 2017 10:16

added support for array_set in the full-slice option

9606967

added test case into goto-instrument regression for checking array_set

2fc22f4

added function call to working queue in the full-slicer

b823e0a

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

lucasccordeiro force-pushed the fix-full-slice-06 branch from 3d38441 to ac39dfb Compare July 4, 2017 09:20

lucasccordeiro changed the title ~~consider array_set expressions in the full-slice~~ consider array_set expressions in the full-slice (do not merge) Jul 4, 2017

added new test cases related to function call

09df414

combined full-slice with reachability-slice

4b1c20b

lucasccordeiro force-pushed the fix-full-slice-06 branch from ac39dfb to 4b1c20b Compare July 4, 2017 10:13

lucasccordeiro closed this Jul 4, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

consider array_set expressions in the full-slice (do not merge) #898

consider array_set expressions in the full-slice (do not merge) #898

lucasccordeiro commented May 9, 2017

tautschnig May 9, 2017

tautschnig May 9, 2017

tautschnig May 10, 2017

tautschnig left a comment

lucasccordeiro commented May 10, 2017

lucasccordeiro commented May 11, 2017

lucasccordeiro commented May 11, 2017

lucasccordeiro commented May 11, 2017

tautschnig commented May 11, 2017

martin-cs commented May 15, 2017 via email

lucasccordeiro commented May 15, 2017

lucasccordeiro commented May 15, 2017

tautschnig May 22, 2017

tautschnig May 22, 2017

tautschnig May 22, 2017

tautschnig May 22, 2017

lucasccordeiro commented Jul 4, 2017

consider array_set expressions in the full-slice (do not merge) #898

consider array_set expressions in the full-slice (do not merge) #898

Conversation

lucasccordeiro commented May 9, 2017

tautschnig May 9, 2017

Choose a reason for hiding this comment

tautschnig May 9, 2017

Choose a reason for hiding this comment

tautschnig May 10, 2017

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

lucasccordeiro commented May 10, 2017

lucasccordeiro commented May 11, 2017

lucasccordeiro commented May 11, 2017

lucasccordeiro commented May 11, 2017

tautschnig commented May 11, 2017

martin-cs commented May 15, 2017 via email

lucasccordeiro commented May 15, 2017

lucasccordeiro commented May 15, 2017

tautschnig May 22, 2017

Choose a reason for hiding this comment

tautschnig May 22, 2017

Choose a reason for hiding this comment

tautschnig May 22, 2017

Choose a reason for hiding this comment

tautschnig May 22, 2017

Choose a reason for hiding this comment

lucasccordeiro commented Jul 4, 2017