Add test verifying no invalid trace with dynamic array #4372

thk123 · 2019-03-12T14:34:46Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[n/a] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
[n/a] My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

In trying to produce a test for #4197 I've discovered the problem originally discussed in #4153 has been fixed. So I added the test and moved the invariant to a more defensive position.

tautschnig

I'm quite curious which change actually fixed this problem?

tautschnig · 2019-03-12T14:43:57Z

jbmc/regression/jbmc/nondet-array-size/test.desc

+--
+--
+Verify that the trace produced when creating an array whose size is determined
+by a an array input, the trace is valid.


tautschnig

I'm quite curious which change actually fixed the problem?

tautschnig · 2019-03-12T14:45:44Z

jbmc/regression/jbmc/nondet-array-size/test.desc

+--
+--
+Verify that the trace produced when creating an array whose size is determined
+by a an array input, the trace is valid.


smowton

Fix English, otherwise lgtm :)

smowton · 2019-03-12T15:04:34Z

jbmc/regression/jbmc/nondet-array-size/test.desc

+VERIFICATION FAILED
+--
+--
+Verify that the trace produced when creating an array whose size is determined


"Verify that when an array's size is determined by an array input, the resulting trace is valid"?

thk123 · 2019-03-12T16:57:09Z

So moving this invariant now causes some other failures so I will do the following:

try this branch on top of Do not generate nil_exprt in bv_get #4197 to see if that's now fixing that
move the invariant back and add a regex that the value is now not unknown
low priority: bisect between two versions to see what fixed it

thk123 · 2019-03-12T17:59:06Z

Note failure is cbmc-cprover-smt2-CORE not cbmc-CORE

tautschnig · 2019-03-12T18:37:47Z

@thk123 I suppose I should also put some effort into the work in #4197.

thk123 · 2019-03-13T09:36:56Z

@tautschnig I've not yet checked that fixes this, and so far not got a test that passes on your branch that fails on develop so I wouldn't rush. I'll let you know if the failures here are fixed by your branch.

thk123 · 2019-03-13T09:53:08Z

@tautschnig Still get this invariant fail on top of your branch, specifically on cbmc-cprover-smt2:

json1/test.desc
trace_options_json_extended/extended.desc
trace_options_json_extended/non-extended.desc

If you want to investigate them further. For now I will put the invariant back and see if I can make the test a little more precise.

peterschrammel · 2019-03-18T20:52:49Z

src/goto-programs/json_goto_trace.cpp

@@ -118,6 +118,10 @@ void convert_decl(
  const symbolt *symbol;
  irep_idt base_name, display_name;

+  DATA_INVARIANT(


Compare with the corresponding code in goto_trace.cpp:

cbmc/src/goto-programs/goto_trace.cpp

Line 271 in 557be1d

if(value.is_nil())

tautschnig · 2019-03-29T23:17:40Z

@tautschnig Still get this invariant fail on top of your branch, specifically on cbmc-cprover-smt2: [...]

It seems the SMT2 solver simply is broken when it comes to unbounded/infinity-sized arrays (@kroening might have some input): The solver returns as model

((|__CPROVER_threads_exited#1| |__CPROVER_threads_exited#1|))

which is not usable as it is self-referential.

The full_lhs_value should have a non-nil value regardless of whether the identifier exists in the namespace. This makes visible that the SMT solver returns for an unbounded array as value ((|__CPROVER_threads_exited#1| |__CPROVER_threads_exited#1|)) which is self-referential and thus not usable.

tautschnig · 2019-03-29T23:28:16Z

@thk123 I took the liberty to rebase your branch, include tags for the broken SMT test, and apply @smowton text suggestion. I'll leave it to you to merge this as I'm not sure whether moving the invariant would break TG in some way.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 08c7c9d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106404959

thk123 · 2019-04-02T11:28:42Z

This passes tests locally for me, I believe I only ever saw problems on JBMC

thk123 requested review from kroening, peterschrammel, pkesseli, smowton and tautschnig as code owners March 12, 2019 14:34

thk123 changed the title ~~Invalid trace dynamic array~~ Add test verifying no invalid trace with dynamic array Mar 12, 2019

tautschnig approved these changes Mar 12, 2019

View reviewed changes

smowton approved these changes Mar 12, 2019

View reviewed changes

peterschrammel reviewed Mar 18, 2019

View reviewed changes

peterschrammel assigned thk123 Mar 18, 2019

thk123 added 2 commits March 29, 2019 23:21

Adding test demonstrating fix to trace generation

08c7c9d

tautschnig force-pushed the invalid-trace-dynamic-array branch from 557be1d to 08c7c9d Compare March 29, 2019 23:26

tautschnig added the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Mar 29, 2019

tautschnig mentioned this pull request Mar 30, 2019

Remove invariant on full_lhs_value in printing goto_tracet #4153

Closed

7 tasks

allredj reviewed Mar 30, 2019

View reviewed changes

tautschnig mentioned this pull request Apr 1, 2019

Do not generate nil_exprt in bv_get #4197

Merged

3 tasks

thk123 removed the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Apr 2, 2019

thk123 merged commit 8235cb4 into diffblue:develop Apr 2, 2019

thk123 deleted the invalid-trace-dynamic-array branch April 2, 2019 11:28

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add test verifying no invalid trace with dynamic array #4372

Add test verifying no invalid trace with dynamic array #4372

thk123 commented Mar 12, 2019

tautschnig left a comment

tautschnig Mar 12, 2019

tautschnig left a comment

tautschnig Mar 12, 2019

smowton left a comment

smowton Mar 12, 2019

thk123 commented Mar 12, 2019

thk123 commented Mar 12, 2019

tautschnig commented Mar 12, 2019

thk123 commented Mar 13, 2019

thk123 commented Mar 13, 2019

peterschrammel Mar 18, 2019

tautschnig commented Mar 29, 2019

tautschnig commented Mar 29, 2019

allredj left a comment

thk123 commented Apr 2, 2019

Add test verifying no invalid trace with dynamic array #4372

Add test verifying no invalid trace with dynamic array #4372

Conversation

thk123 commented Mar 12, 2019

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Mar 12, 2019

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Mar 12, 2019

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

smowton Mar 12, 2019

Choose a reason for hiding this comment

thk123 commented Mar 12, 2019

thk123 commented Mar 12, 2019

tautschnig commented Mar 12, 2019

thk123 commented Mar 13, 2019

thk123 commented Mar 13, 2019

peterschrammel Mar 18, 2019

Choose a reason for hiding this comment

tautschnig commented Mar 29, 2019

tautschnig commented Mar 29, 2019

allredj left a comment

Choose a reason for hiding this comment

thk123 commented Apr 2, 2019