[depends: #1161, #1272] JSON expr and JSON trace #1271

tautschnig · 2017-08-22T14:58:55Z

None of this is my work - these are commits already merged into develop (test-gen-support).

peterschrammel · 2017-08-22T15:14:58Z

src/goto-programs/json_goto_trace.cpp

+/// Replaces in src, expressions of the form pointer_offset(constant) by that
+/// constant.
+/// \param src: an expression
+void remove_pointer_offsets(exprt &src)


util/simplify_expr should be improved to do that.

peterschrammel · 2017-08-22T15:16:30Z

src/util/json_expr.h

@@ -21,11 +22,13 @@ class namespacet;

 json_objectt json(
  const exprt &,
-  const namespacet &);
+  const namespacet &,
+  const irep_idt &mode=ID_unknown);


Default arguments should be avoided.

Done in #1288.

peterschrammel · 2017-08-22T15:19:17Z

src/util/json_expr.cpp

+
+#include <langapi/mode.h>
+
+static exprt simplify_json_expr(


util/simplify_expr should be improved to do that.

Done in #1288.

tautschnig · 2017-08-23T12:58:40Z

src/goto-programs/json_goto_trace.cpp

+  if(src.id()==ID_pointer_offset &&
+     src.op0().id()==ID_constant &&
+     src.op0().op0().id()==ID_address_of &&
+     src.op0().op0().op0().id()==ID_index)


@romainbrenguier Would you happen to know where you had seen such expressions? (This originally was f4fa778.) As far as I am aware, an expression with id ID_constant should not have any operands.

These are symbolic pointer constants -- for example, constant(value -> 0x12345678, op0 -> &dynamic_object1), giving both the bitwise and the symbolic value. They only occur in traces AFAIK.

Also I'd be quite surprised by a case where this worked, but the above more general function didn't.

Thanks a lot, finally I do understand and should have done so all along as I happened to edit code recently... Quite possibly we should have a pointer_constant_exprt or the likes.

I think the constant operands does not only happen in traces but in other places as well, I will try to find some example...
I agree how expressions deal with pointers is a bit messy at the moment but I'm not sure about pointer_constant_exprt, why not having simply a constant of type pointer?

Actually it seems that constant operands is something coming from the solver: if I understand correctly calling get on an expression returns a constant with value corresponding to its actual value and an operand with the original expression.
One thing that confused me a bit is that expressions like &a[0] gets simplified by from_expr to a, but simplify_expr does not simplify it.

One thing that confused me a bit is that expressions like &a[0] gets simplified by from_expr to a, but simplify_expr does not simplify it.

That's because as much as they can be used interchangeably at source level, their types are different: with int a[1], a is of type int[1], while &a[0] is of type int*. Consequently the pretty printer can do this "simplification" at text level, but transforming expressions would not be valid.

ok thanks, it makes more sense to me now

mgudemann · 2017-08-23T12:13:22Z

regression/cbmc-java/exceptions20/test.java

+   }  
+ }
+}
+


is exceptions20 included deliberately?

No, this is a merge error, I will review how this crept in.

Hmm, no, not quite: this appears to be the regression test affiliated with d299ea2. Do you think this is not a good fit for this PR?

ok, I forgot about that and wondered what is has to do with JSON. ok for inclusion then.

tautschnig · 2017-08-23T14:01:10Z

I will need to debug why the "outputID" entry is missing from the test output (failing CI test).

smowton

Concerned about some of those simplifications. I expect some of them are deliberately unsound but look pretty, and therefore they should not go into simplify_expr.

smowton · 2017-08-23T14:19:43Z

src/goto-programs/json_goto_trace.cpp

+  if(src.id()==ID_pointer_offset &&
+     src.op0().id()==ID_constant &&
+     src.op0().op0().id()==ID_address_of &&
+     src.op0().op0().op0().id()==ID_index)


These are symbolic pointer constants -- for example, constant(value -> 0x12345678, op0 -> &dynamic_object1), giving both the bitwise and the symbolic value. They only occur in traces AFAIK.

smowton · 2017-08-23T14:22:08Z

src/goto-programs/json_goto_trace.cpp

+  if(src.id()==ID_pointer_offset &&
+     src.op0().id()==ID_constant &&
+     src.op0().op0().id()==ID_address_of &&
+     src.op0().op0().op0().id()==ID_index)


Also I'd be quite surprised by a case where this worked, but the above more general function didn't.

smowton · 2017-08-23T14:30:02Z

src/util/json_expr.cpp

+         src.operands().size()==1 &&
+         src.op0().id()!=ID_constant)
+        // try to simplify the constant pointer
+        return simplify_json_expr(src.op0(), ns);


Recommend improve this comment -- this is discarding the binary value of the pointer, keeping only the symbolic expression. It is not a simplification per se.

smowton · 2017-08-23T14:31:17Z

src/util/json_expr.cpp

+            src.op0()).get_component_name()).find("@")!=std::string::npos)
+  {
+    // simplify expressions of the form &member_expr(object, @class_identifier)
+    return simplify_json_expr(src.op0(), ns);


!!! This transforms ``&x.@xyzintox.@xyz`, changing its type!

smowton · 2017-08-23T14:32:14Z

src/util/json_expr.cpp

+            to_index_expr(src.op0()).index()).value_is_zero_string())
+  {
+    // simplify expressions of the form  &array[0]
+    return simplify_json_expr(to_index_expr(src.op0()).array(), ns);


! &arr[0] has type element* whereas arr has type element[...], might be important?

tautschnig · 2017-08-23T18:44:59Z

Concerned about some of those simplifications. I expect some of them are deliberately unsound but look pretty, and therefore they should not go into simplify_expr.

Are there tests or other bits of information that could be used for validation purposes? @romainbrenguier would you know more about this? You seem to have authored the original commits introducing those changes, unless I'm mistaken. If anyone else has input, please do contribute.

peterschrammel · 2017-08-23T19:01:25Z

The typical use case of these simplifications is regression/cbmc-java/json_trace3 where array access expressions that entirely consist of constants should be simplified to the value expression of the accessed array element, e.g. {10, 11, 12, 13}[(0+8)/4)]=12 for a 32-bit int array.

romainbrenguier · 2017-08-25T14:23:45Z

Actually there is a regression test which was supposed to check the original changes in regression/strings-smoke-tests/jsonArrays but it has been changed and it seems to be broken as we see some unknown values assigned:

         {
          "assignmentType": "variable",
          "hidden": true,
          "internal": false,
          "lhs": "tmp_object_factory$5",
          "mode": "java",
          "sourceLocation": {
            "file": "test.java",
            "function": "java::test.check:(Ljava/lang/String;)I",
            "line": "5"
          },
          "stepType": "assignment",
          "thread": 0,
          "value": {
            "name": "unknown"
          }
        },

It seems the value reported as unknown is a with_expr representing an array and not handled by json, it wouldn't be handled by the functions removed by this PR either, so it should not block this PR and we should create a new issue for that (TG-393) .

It's only called from within configt.

json() does not deal with nil expression and would just give "name" : "unknown". On the other hand nil expression should not make it to that stage so it would probably denotes an error.

This will delete language pointer created by get_language_from_mode when the object goes out of scope. This prevents memory leaks when using json output.

We simplifying these expression so that these pointers appear correctly in the trace in json. This is related to issue diffblue/test-gen#21 Includes improvements in json_expr.cpp following review of PR#922

We simplify expressions containing array accesses before producing a json representation of the trace. This commit also adds comments on the functions in the cpp files Includes improvements in json_goto_trace.cpp following review of PR#922

This previously stripped pointer_offset_exprt, which wasn't correct-- it should mask the pointer expression within it to give the offset between the operand address and the base of its allocation.

With the exception_value support, there is the possibility to have `nil` values assigned in the trace. These values are returned from `prop_conv.get(expr)`.

In particular, booleans are now printed as true/false instead of 0/1; NULL as null, and pointer types as their respective structs.

tautschnig · 2018-02-23T13:09:45Z

All the discussion items seem to have been merged into develop, closing this as a transition to master will likely happen differently.

tautschnig requested review from peterschrammel, smowton, thk123, mgudemann and romainbrenguier August 22, 2017 14:59

peterschrammel reviewed Aug 22, 2017

View reviewed changes

tautschnig self-assigned this Aug 23, 2017

tautschnig mentioned this pull request Aug 23, 2017

[depends: #1271] Test coverage commits #1278

Closed

tautschnig commented Aug 23, 2017

View reviewed changes

mgudemann reviewed Aug 23, 2017

View reviewed changes

tautschnig mentioned this pull request Aug 23, 2017

JSON code cleanup #1288

Merged

tautschnig changed the title ~~[develop->master] JSON expr and JSON trace~~ [depends: #1288, develop->master] JSON expr and JSON trace Aug 23, 2017

smowton reviewed Aug 23, 2017

View reviewed changes

romainbrenguier added the do not merge label Aug 25, 2017

tautschnig force-pushed the json-trace branch from a2de5e4 to 4d28bdd Compare September 1, 2017 20:20

tautschnig added the develop->master label Sep 2, 2017

tautschnig changed the title ~~[depends: #1288, develop->master] JSON expr and JSON trace~~ [depends: #1288] JSON expr and JSON trace Sep 2, 2017

tautschnig changed the title ~~[depends: #1288] JSON expr and JSON trace~~ JSON expr and JSON trace Sep 2, 2017

tautschnig changed the title ~~JSON expr and JSON trace~~ [depends: #1161] JSON expr and JSON trace Sep 2, 2017

peterschrammel added 7 commits September 2, 2017 10:30

Make configt::set_classpath private

e274395

It's only called from within configt.

Factorize setting config from symbol table when reading goto binaries

69bed5d

Replace BV_ADDR_BITS by config setting

5947035

Better error message when too many dynamic objects

be93dcc

Allow specifying object-bits via command line and language defaults

7944e21

Catch command line parsing exceptions

fc35b49

Add java address space limits tests

eed3925

romainbrenguier and others added 22 commits September 2, 2017 10:30

Call to lookup that does not throw when symbol is not found

7b27200

Use the from_type function to get string for the type

f7bd507

Adding assertion to make sure "type" field is always set

a8d0a00

Adding assertions to prevent the "data" field from not being set

5532660

Assertion to forbid calling json() with nil values

5c3e67c

json() does not deal with nil expression and would just give "name" : "unknown". On the other hand nil expression should not make it to that stage so it would probably denotes an error.

Using unique pointers to avoid memory leak in json for expressions

49bf719

This will delete language pointer created by get_language_from_mode when the object goes out of scope. This prevents memory leaks when using json output.

Simplifying expressions of the form &array[0] in json

ab93ab7

We simplifying these expression so that these pointers appear correctly in the trace in json. This is related to issue diffblue/test-gen#21 Includes improvements in json_expr.cpp following review of PR#922

Adding test to check that data field of strings are set in json

5aec3c8

Documentation for json_goto_trace in doxygen format

8e037aa

Fix remove_pointer_offsets

695e2a5

This previously stripped pointer_offset_exprt, which wasn't correct-- it should mask the pointer expression within it to give the offset between the operand address and the base of its allocation.

Allow "unknown" value assignments in JSON trace

c82da48

With the exception_value support, there is the possibility to have `nil` values assigned in the trace. These values are returned from `prop_conv.get(expr)`.

Add regression test for nil assigns in JSON trace

dbf699a

Fix language-specific constant printing in JSON

67482d7

Fix mode in input/output steps in JSON trace

f7bfd6b

Replace asserts

e85ecd8

Replace simplify_index by simplify_expr

7248d1b

Replace asserts

8a6b357

Test for java-specific output in JSON

1589bf1

In particular, booleans are now printed as true/false instead of 0/1; NULL as null, and pointer types as their respective structs.

Do not use default arguments for json(...)

bdf18be

Simplify pointer_offset(constant)

0f2fcc4

Use generic simplify_expr instead of local simplification rules

a6236ab

tautschnig force-pushed the json-trace branch from 4d28bdd to a6236ab Compare September 2, 2017 09:31

tautschnig changed the title ~~[depends: #1161] JSON expr and JSON trace~~ [depends: #1161, #1272] JSON expr and JSON trace Sep 2, 2017

romainbrenguier removed the do not merge label Sep 28, 2017

thk123 requested review from chrisr-diffblue and removed request for thk123 October 31, 2017 12:57

tautschnig closed this Feb 23, 2018

tautschnig deleted the json-trace branch February 23, 2018 13:09

[depends: #1161, #1272] JSON expr and JSON trace #1271

[depends: #1161, #1272] JSON expr and JSON trace #1271

Uh oh!

Conversation

tautschnig commented Aug 22, 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!

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!

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 Aug 23, 2017

Uh oh!

smowton left a comment

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 Aug 23, 2017

Uh oh!

peterschrammel commented Aug 23, 2017

Uh oh!

romainbrenguier commented Aug 25, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tautschnig commented Feb 23, 2018

Uh oh!

Uh oh!

romainbrenguier commented Aug 25, 2017 •

edited

Loading