Better output of arrays in json #922

romainbrenguier · 2017-05-15T09:33:19Z

This improves the output for arrays by simplifying some expressions, such as &array[0] and array0[pointer_offset[array0]].
This is related to issue diffblue/test-gen#293 ~~and is based on PR #889~~ (merged)

mgudemann · 2017-06-12T15:25:25Z

src/goto-programs/json_goto_trace.cpp

+
+\*******************************************************************/
+
+void remove_pointer_offsets(exprt &src, symbol_exprt array_symbol)


can array_symbol be passed as a reference

mgudemann · 2017-06-12T15:26:09Z

src/goto-programs/json_goto_trace.cpp

+          simplified into a unsigned constant value.
+
+ Purpose: Simplify the expression in index as much as possible to try
+          to get a unsigned constannt.


constannt->constant

a unsigned -> an unsigned

mgudemann · 2017-06-12T15:27:08Z

src/goto-programs/json_goto_trace.cpp

+{
+  if(idx.id()==ID_constant)
+  {
+    std::string value_str=id2string(to_constant_expr(idx).get_value());


value_str(id2string(...))

mgudemann · 2017-06-12T15:28:50Z

src/goto-programs/json_goto_trace.cpp

+  {
+    std::string value_str=id2string(to_constant_expr(idx).get_value());
+    mp_integer int_value=binary2integer(value_str, false);
+    out=int_value.to_long();


it is sure that there will never be an overflow?

allredj · 2017-06-12T15:55:54Z

src/goto-programs/json_goto_trace.cpp

+          simplified into a unsigned constant value.
+
+ Purpose: Simplify the expression in index as much as possible to try
+          to get a unsigned constannt.


a unsigned -> an unsigned

allredj · 2017-06-12T15:59:45Z

src/goto-programs/json_goto_trace.cpp

+
+  Inputs:
+    idx - an expression representing an index in an array
+    out - a reference to an unsigned value


I know the name of the variable speaks for itself, but could we be clearer about the fact that we write the result to out?
e.g. out - the result of the simplification?

allredj · 2017-06-12T16:06:56Z

src/goto-programs/json_goto_trace.cpp

+    out=int_value.to_long();
+    return false;
+  }
+  else if(idx.id()==ID_plus)


Doesn't ID_minus case occur?

All examples I have seen are of the form a pointer offset address plus some constant index, but I admit I don't know whether that really covers all the possibilities.

allredj · 2017-06-12T16:14:34Z

src/goto-programs/json_goto_trace.cpp

+  if(src.id()==ID_index && to_index_expr(src).array().id()==ID_symbol)
+  {
+    // Case where the array is a symbol.
+    symbol_exprt array_symbol=to_symbol_expr(to_index_expr(src).array());


const symbol_exprt &array_symbol?

allredj · 2017-06-12T16:17:24Z

src/util/json_expr.cpp

+          to_constant_expr(
+            to_index_expr(src.op0()).index()).value_is_zero_string())
+  {
+    // simplify things of the form  &array[0]


extra space in the comment

allredj · 2017-06-12T16:23:14Z

src/goto-programs/json_goto_trace.cpp

+
+\*******************************************************************/
+
+exprt simplify_array_access(const exprt &src, const namespacet &ns)


ns is unused

allredj

Looks good!

allredj · 2017-06-13T09:19:26Z

Can we have some regression tests for that?

romainbrenguier · 2017-06-13T14:48:10Z

@allredj actually I cannot find an example where the original problem still occurs. Maybe something as been fixed in CBMC that prevent the problem we are trying to solve from happening. I will check whether this is still needed and if not we can drop this pull request.

romainbrenguier · 2017-06-13T16:24:57Z

Actually I did found examples where we have an improvement, I made a commit to add this as a regression test.
Note that I also included the PR #1006 without which the test would fail when CBMC is compiled with sanitize option because of a memory leak solved by that PR.

allredj

LGTM

mgudemann · 2017-06-15T09:09:16Z

@romainbrenguier could you rebase before re-review, please?

romainbrenguier · 2017-06-19T15:29:19Z

@allredj @mgudemann this is now rebased

allredj

Still looks good.

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

romainbrenguier force-pushed the pull-request/arrays-in-trace branch 2 times, most recently from 743ce25 to d0bfb41 Compare June 12, 2017 07:53

forejtv requested review from mgudemann and allredj June 12, 2017 14:03

mgudemann suggested changes Jun 12, 2017

View reviewed changes

allredj approved these changes Jun 12, 2017

View reviewed changes

allredj suggested changes Jun 12, 2017

View reviewed changes

allredj previously approved these changes Jun 13, 2017

View reviewed changes

mgudemann previously approved these changes Jun 13, 2017

View reviewed changes

romainbrenguier dismissed mgudemann’s stale review via b23da64 June 13, 2017 16:22

romainbrenguier force-pushed the pull-request/arrays-in-trace branch from 83f9a3c to b23da64 Compare June 13, 2017 16:22

forejtv force-pushed the test-gen-support branch from c7b1fce to a308fb5 Compare June 13, 2017 21:04

romainbrenguier dismissed allredj’s stale review via 74b9d95 June 14, 2017 15:23

romainbrenguier force-pushed the pull-request/arrays-in-trace branch from b23da64 to 74b9d95 Compare June 14, 2017 15:23

forejtv requested review from allredj and mgudemann June 15, 2017 07:57

allredj previously approved these changes Jun 15, 2017

View reviewed changes

romainbrenguier dismissed allredj’s stale review via 8f192ae June 15, 2017 11:56

romainbrenguier force-pushed the pull-request/arrays-in-trace branch from 74b9d95 to 8f192ae Compare June 15, 2017 11:56

romainbrenguier requested review from mgudemann and removed request for mgudemann June 20, 2017 08:18

allredj previously approved these changes Jun 20, 2017

View reviewed changes

romainbrenguier requested review from mgudemann and removed request for mgudemann June 21, 2017 14:13

mgudemann previously approved these changes Jun 21, 2017

View reviewed changes

romainbrenguier added 4 commits June 21, 2017 20:40

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

02b7942

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

5cfa413

Documentation for json_goto_trace in doxygen format

f950ffc

romainbrenguier dismissed stale reviews from mgudemann and allredj via f950ffc June 21, 2017 19:40

romainbrenguier force-pushed the pull-request/arrays-in-trace branch from 8f192ae to f950ffc Compare June 21, 2017 19:40

romainbrenguier requested review from mgudemann and allredj June 21, 2017 21:39

mgudemann approved these changes Jun 22, 2017

View reviewed changes

allredj approved these changes Jun 22, 2017

View reviewed changes

romainbrenguier merged commit 05875e1 into diffblue:test-gen-support Jun 22, 2017

romainbrenguier deleted the pull-request/arrays-in-trace branch June 22, 2017 16:28

tautschnig mentioned this pull request Jul 13, 2017

Port improvements from test-gen-support to master #1121

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Better output of arrays in json #922

Better output of arrays in json #922

romainbrenguier commented May 15, 2017 •

edited

Loading

mgudemann Jun 12, 2017

mgudemann Jun 12, 2017

allredj Jun 12, 2017

mgudemann Jun 12, 2017

mgudemann Jun 12, 2017

allredj Jun 12, 2017

allredj Jun 12, 2017

allredj Jun 12, 2017

romainbrenguier Jun 13, 2017

allredj Jun 12, 2017

allredj Jun 12, 2017

allredj Jun 12, 2017

allredj left a comment

allredj commented Jun 13, 2017

romainbrenguier commented Jun 13, 2017

romainbrenguier commented Jun 13, 2017

allredj left a comment

mgudemann commented Jun 15, 2017

romainbrenguier commented Jun 19, 2017

allredj left a comment


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

		void remove_pointer_offsets(exprt &src, symbol_exprt array_symbol)


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

		exprt simplify_array_access(const exprt &src, const namespacet &ns)

Better output of arrays in json #922

Better output of arrays in json #922

Conversation

romainbrenguier commented May 15, 2017 • edited Loading

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

allredj left a comment

Choose a reason for hiding this comment

allredj commented Jun 13, 2017

romainbrenguier commented Jun 13, 2017

romainbrenguier commented Jun 13, 2017

allredj left a comment

Choose a reason for hiding this comment

mgudemann commented Jun 15, 2017

romainbrenguier commented Jun 19, 2017

allredj left a comment

Choose a reason for hiding this comment

romainbrenguier commented May 15, 2017 •

edited

Loading