hide specific variables in the counterexample trace for test-gen-support #605

lucasccordeiro · 2017-03-06T09:50:41Z

hide variable assignments related to dynamic_object[0-9],
dynamic_[0-9]_array, and CPROVER internal functions
(e.g., __CPROVER_initialize). This PR is related to
test-gen-support issue https://github.com/diffblue/test-gen/issues/20

peterschrammel · 2017-03-07T23:22:57Z

src/goto-symex/build_goto_trace.cpp

+  if (expr.id()==ID_symbol)
+  {
+    std::string identifier = expr.get(ID_identifier).c_str();
+    if (identifier.find("dynamic_")!=std::string::npos)


This looks like a hack...

Yes, I also agree that this looks like a hack. I was thinking about alternatives to get rid of this hack. What do you think if we create a new field called "dynamic_object" that is properly set during the convert method call in goto-programs? This might create some additional overhead when we build the respective goto-program.

Looking at the symbol behind that name, you should find #dynamic to be set in the type of the symbol. See goto-symex/symex_builtin_functions.cpp.

peterschrammel · 2017-03-07T23:23:10Z

src/goto-symex/build_goto_trace.cpp

+{
+  if (expr.id()==ID_symbol)
+  {
+    std::string identifier = expr.get(ID_identifier).c_str();


use id2string

Implemented as suggested.

peterschrammel · 2017-03-07T23:23:22Z

src/goto-symex/build_goto_trace.cpp

+  else
+  {
+    forall_operands(it, expr)
+      hide_dynamic_object(*it,goto_trace_step);


cpplint (more instances)

Implemented as suggested.

tautschnig · 2017-03-14T02:08:10Z

Why is this hiding actually necessary?

lucasccordeiro · 2017-03-14T09:21:59Z

@tautschnig: We would like to hide all variable assignments in the counterexample trace related to

dynamic_object[0-9]
dynamic_[0-9]_array

I have tried to implement your suggestion as follows:

....
bool is_dynamic_object=expr.type().get_bool("#dynamic");
goto_trace_step.hidden=is_dynamic_object;
....

However, it does not work if we have expressions that contain "dynamic_object[0-9]". For "dynamic_[0-9]_array", it seems to work well.

This is the test program that I'm using:

public class Test
{
   public static void foo(int x, int y)
   {
     int diffblue[] = {10, 20, 30, 40};

     assert(diffblue[x] + diffblue[y] != x + y);
  }

   public static void main(String[] args)
   {
     foo(40,30);
   }
}

I'm running CBMC as follows:

cbmc Test.class --trace --json-ui

tautschnig · 2017-03-14T09:36:09Z

I believe you will need to look up the symbol in the namespace and then look at the symbol's type. Comments like #dynamic need not be present in all expressions. Could you give that a try?

lucasccordeiro · 2017-03-14T09:37:30Z

Yes, sure. I'll take a look at it.

lucasccordeiro · 2017-03-17T10:28:02Z

@tautschnig: I have tried to look for examples in the source code, but I couldn't find what you have suggested (maybe I have misunderstood it). Is there some chance to point to some particular portion of the CBMC code, where I could look at your suggestion?

lucasccordeiro · 2017-03-17T17:14:12Z

@tautschnig: It seems that expressions like dynamic_object[0-9] and dynamic_[0-9]_array are not in the symbol table. If I understood your comment correctly, I have tried to look for the symbol in the namespace as follows:

...
  if(expr.id()==ID_symbol)
  {
    symbol_tablet symbol_table = ns.get_symbol_table();

    if (symbol_table.has_symbol(to_symbol_expr(expr).get_identifier()))
    {
      const symbolt &symbol=
        ns.lookup(to_symbol_expr(expr));
     }
   ...
   }
...

However, I'm unable to look further at the symbol's type since the second if-condition is always false.

I have also run CBMC with the option ''--show-symbol-table'', but I was unable to find expressions like dynamic_object[0-9] and dynamic_[0-9]_array in the symbol table.

tautschnig · 2017-03-20T10:43:53Z

src/goto-symex/build_goto_trace.cpp

-          s_it2=goto_trace.steps.erase(s_it2));
-
+          s_it2=goto_trace.steps.erase(s_it2))
+      { };


As you are touching this code: I believe this can be rewritten to goto_trace.steps.erase(s_it1, goto_trace.steps.end()); instead of this strange for loop.

Implemented as suggested.

tautschnig · 2017-03-20T10:47:02Z

Indeed you wouldn't find them using --show-symbol-table as they will only be generated during symbolic execution.
You will want to use to_ssa_expr(expr).get_object_name() as you are likely dealing with some SSA-renamed symbol. That resulting name, I believe, should be found in the symbol table. If you still can't find it, would you mind printing out the exact identifier and copying this into the conversation here?

lucasccordeiro · 2017-03-20T13:07:33Z

@tautschnig: I have tried to implement your suggestion as:

  if(expr.id()==ID_symbol)
  {
    symbol_tablet symbol_table = ns.get_symbol_table();
    if (symbol_table.has_symbol(to_ssa_expr(expr).get_object_name()))
    {
      const symbolt &symbol=
        ns.lookup(to_symbol_expr(expr));
      ...
     }
  }

However, we get this in the trace:

identifier __CPROVER_rounding_mode!0#1 not found

In json format:

{
  "messageText": "identifier __CPROVER_rounding_mode!0#1 not found",
  "messageType": "ERROR"
}

tautschnig · 2017-03-20T13:46:55Z

I am sorry, I had misguided you: you need get_original_name, not get_object_name.

lucasccordeiro · 2017-03-20T17:12:30Z

@tautschnig: I still get the same behavior as previously mentioned if I replace "get_object_name" by "get_original_name". Do you have another suggestion?

- strip <CR> from end of lines in test.pl - tests for test-script do not depend on gcc - Makefile in regression/goto-analyser has the same structure as other test Makefiles - remove tests for empty lines

tautschnig · 2017-03-20T17:38:42Z

Would you mind adding expr.pretty() for debugging purposes (and copy the final tree output in here)?

lucasccordeiro · 2017-03-21T08:31:19Z

@tautschnig: yes, sure. Find below the output of expr.pretty() method:

expr.pretty(): symbol
  * type: signedbv
      * width: 32
      * #c_type: signed_int
  * identifier: __CPROVER_rounding_mode!0#1
  * expression: symbol
      * type: signedbv
          * width: 32
          * #c_type: signed_int
      * identifier: __CPROVER_rounding_mode
  * L0: 0
  * L2: 1
  * L1_object_identifier: __CPROVER_rounding_mode!0
  * #SSA_symbol: 1
,
{
  "messageText": "identifier __CPROVER_rounding_mode!0#1 not found",
  "messageType": "ERROR"
}

tautschnig · 2017-03-21T10:07:33Z

Ok, this looks good - there might be a minor omission in your code; the following should work:

if(expr.id()==ID_symbol)
  {
    symbol_tablet symbol_table = ns.get_symbol_table();
    if (symbol_table.has_symbol(to_ssa_expr(expr).get_original_name()))
    {
      const symbolt &symbol=
        ns.lookup(to_ssa_expr(expr).get_original_name());  // <-- this had still been to_symbol_expr ...
      ...
     }
  }

lucasccordeiro · 2017-03-21T10:14:21Z

@tautschnig: I have used get_original_name() for both calls: has_symbol and lookup as follows:

  if(expr.id()==ID_symbol)
  {
    symbol_tablet symbol_table = ns.get_symbol_table();
    if (symbol_table.has_symbol(to_ssa_expr(expr).get_original_name()))
    {
      const symbolt &symbol=
        ns.lookup(to_ssa_expr(expr).get_original_name());
     }
  }
```

I'm now able to have access to the symbol's type, but it does not 
seem to show the dynamic object type. How can you detect whether 
a given symbol's type is dynamic?

Find attached the log file produced for the output of the goto trace 
using the expr.pretty() method.
 
[log.txt.zip](https://github.com/diffblue/cbmc/files/857729/log.txt.zip)

lucasccordeiro · 2017-03-21T12:55:01Z

@tautschnig: many thanks for your support to fix this issue.

@peterschrammel: Now I believe we have a proper fix for this issue.

Let me know if you have further comments.

Fix several test problems on Windows

Simply assigning to a temporary symbol of the correct type and amending the type passed to the elaboration of the sub-array seems to suffice to properly initialise a multi-dimensional array.

Correct pretty-printing of code_returnt

The default behaviour of CBMC for the options --show-goto-functions, --show-properties and --cover is to consider all functions. This is particularly annoying for --cover where coverage goals are reported from functions that are trivially unreachable from the entry point. Also, --show-reachable-properties has been introduced in the past to hide such properties. We could change the default behaviour to slicing away everything that is trivially unreachable from the entry point. However, this would require an extra option to be able to view all functions and properties. This commit preserves the default behaviour and enables focussing the output of --show-goto-functions --show-properties and --cover on functions that are not trivially unreachable using --drop-unused-functions.

The same effect can now be achieved by --show-properties --drop-unused-functions

…le-fun-only Cover (and others) for reachable functions only

This commit changes the behahaviour of --no-assertions so that only user assertions are ignored. Built-in assertions can be hidden by the new option --no-built-in-assertions.

skip_classid was always false, so there wasn't any point having it.

gen_nondet_init() is only used once, and is only two lines long, so get rid of it and just put those two lines. This also avoids confusion with java_object_factory::gen_nondet_init().

Do not slice away array_copy expressions during the implicit call in the full-slicert class. We do not process array_copy in value_set_fit.

…ay_copy added two test cases related to array copy in the goto-instrument regression suite to further test the full-slice option

consider array_copy expressions in the full-slice

Fix multinewarray

Updates to compiling instructions for GCC 6

Changelog

…-object-factory Cleanup/java object factory

…-user-only No-assertions should not affect assertions in built-ins

hide variable assignments related to dynamic_object[0-9], dynamic_[0-9]_array, and CPROVER internal functions (e.g., __CPROVER_initialize). This PR is related to test-gen-support issue diffblue#20

lucasccordeiro · 2017-03-28T15:19:26Z

Due to several merge conflicts, I have created a new PR to address this issue: #709

…-webgoat SEC-608: Add extra rule for StringBuilder::append(String)

peterschrammel requested changes Mar 7, 2017

View reviewed changes

lucasccordeiro force-pushed the fix-issue-20 branch from 0611b0e to 5ab0933 Compare March 10, 2017 19:35

tautschnig reviewed Mar 20, 2017

View reviewed changes

tautschnig assigned lucasccordeiro Mar 20, 2017

Fix several test problems on Windows

0662dd0

- strip <CR> from end of lines in test.pl - tests for test-script do not depend on gcc - Makefile in regression/goto-analyser has the same structure as other test Makefiles - remove tests for empty lines

lucasccordeiro force-pushed the fix-issue-20 branch from 015b1c2 to b29b80b Compare March 21, 2017 12:51

peterschrammel and others added 9 commits March 22, 2017 21:13

Auxiliary function to check whether source location is in built-in

72052c7

Replace built-in checks by is_built_in

32fcbbc

Merge pull request diffblue#622 from forejtv/master

ff9d833

Fix several test problems on Windows

update instructions for g++ 6

c21d3ed

Merge branch 'master' of github.com:diffblue/cbmc

2a95e59

Updates for GCC 6

903d243

Correct pretty-printing of code_returnt

e843b72

Fix Java multinewarray

4473f06

Simply assigning to a temporary symbol of the correct type and amending the type passed to the elaboration of the sub-array seems to suffice to properly initialise a multi-dimensional array.

Amend test-case to complete in acceptable time

0a53fbb

Daniel Kroening and others added 21 commits March 23, 2017 14:28

Merge pull request diffblue#658 from smowton/pretty_print_return

6550e2c

Correct pretty-printing of code_returnt

Remove -show-reachable-properties

a35731b

The same effect can now be achieved by --show-properties --drop-unused-functions

Correctly align description of option

5e5bbca

Merge pull request diffblue#671 from peterschrammel/cover-for-reachab…

5ecb15e

…le-fun-only Cover (and others) for reachable functions only

Option --no-built-in-assertions

85a7566

This commit changes the behahaviour of --no-assertions so that only user assertions are ignored. Built-in assertions can be hidden by the new option --no-built-in-assertions.

Remove unused variable and braces

2b09c0b

Move function comments to the right place

a3f49a3

Remove variable that is always false

4c4ccc0

skip_classid was always false, so there wasn't any point having it.

Remove function that's only used once

9a1dae0

gen_nondet_init() is only used once, and is only two lines long, so get rid of it and just put those two lines. This also avoids confusion with java_object_factory::gen_nondet_init().

added support for array_copy in the full-slice option

27227cc

Do not slice away array_copy expressions during the implicit call in the full-slicert class. We do not process array_copy in value_set_fit.

added two test cases into goto-instrument regression for checking arr…

e70aa7d

…ay_copy added two test cases related to array copy in the goto-instrument regression suite to further test the full-slice option

Merge pull request diffblue#694 from lucasccordeiro/fix-full-slice-03

727aea1

consider array_copy expressions in the full-slice

Merge pull request diffblue#686 from smowton/fix_multinewarray

96c9e65

Fix multinewarray

Merge pull request diffblue#682 from jgwilson42/compiling_update

7e406cd

Updates to compiling instructions for GCC 6

Release notes up to 5.6 from CProver Google group messages

83874c3

Initial version of release notes for 5.7

81470f4

Merge pull request diffblue#696 from tautschnig/user-visible-changes

4ea27a3

Changelog

Merge pull request diffblue#693 from owen-jones-diffblue/cleanup/java…

cf17239

…-object-factory Cleanup/java object factory

Merge pull request diffblue#681 from peterschrammel/no-assertions-for…

29af567

…-user-only No-assertions should not affect assertions in built-ins

hide specific variables in the counterexample trace for test-gen-support

0feaaef

hide variable assignments related to dynamic_object[0-9], dynamic_[0-9]_array, and CPROVER internal functions (e.g., __CPROVER_initialize). This PR is related to test-gen-support issue diffblue#20

lucasccordeiro force-pushed the fix-issue-20 branch from b29b80b to 0feaaef Compare March 28, 2017 10:08

lucasccordeiro closed this Mar 28, 2017

NathanJPhillips pushed a commit to NathanJPhillips/cbmc that referenced this pull request Sep 6, 2018

Merge pull request diffblue#605 from diffblue/owen-jones-diffblue/fix…

20c6bf1

…-webgoat SEC-608: Add extra rule for StringBuilder::append(String)

hide specific variables in the counterexample trace for test-gen-support #605

hide specific variables in the counterexample trace for test-gen-support #605

Uh oh!

Conversation

lucasccordeiro commented Mar 6, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 14, 2017

Uh oh!

lucasccordeiro commented Mar 14, 2017

Uh oh!

tautschnig commented Mar 14, 2017

Uh oh!

lucasccordeiro commented Mar 14, 2017

Uh oh!

lucasccordeiro commented Mar 17, 2017

Uh oh!

lucasccordeiro commented Mar 17, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lucasccordeiro Mar 20, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Mar 20, 2017

Uh oh!

lucasccordeiro commented Mar 20, 2017

Uh oh!

tautschnig commented Mar 20, 2017

Uh oh!

lucasccordeiro commented Mar 20, 2017

Uh oh!

tautschnig commented Mar 20, 2017

Uh oh!

lucasccordeiro commented Mar 21, 2017

Uh oh!

tautschnig commented Mar 21, 2017

Uh oh!

lucasccordeiro commented Mar 21, 2017

Uh oh!

lucasccordeiro commented Mar 21, 2017

Uh oh!

lucasccordeiro commented Mar 28, 2017

Uh oh!

Uh oh!

lucasccordeiro Mar 20, 2017 •

edited

Loading