Explicit nondet initialisation #35

tautschnig · 2016-03-21T19:50:50Z

Instead of leaving the right-hand side empty, explicitly assign non-deterministic values when creating objects. This enables constant propagation for non-POD types.

tautschnig · 2016-11-17T21:00:41Z

@martin-cs If you have any spare cycles to evaluate the performance impact of this pull request I'd be grateful. It should enable a lot more constant propagation for any code using structs or fixed-size arrays.

peterschrammel · 2017-01-11T19:01:32Z

@tautschnig, needs rebasing...

tautschnig · 2017-01-12T10:24:25Z

@peterschrammel Rebasing done.

forejtv · 2017-02-21T17:37:36Z

@tautschnig can you please rebase to see if all tests pass?

tautschnig · 2017-02-22T08:37:22Z

Rebased, all checks passing. There is another question about performance, however.

forejtv · 2017-02-22T13:12:06Z

@kroening can you let me know if this is good to go or whom I should ask to evaluate the performance?

kroening · 2017-04-03T12:49:23Z

Would the performance concern be addressed by only doing this for compound/array types?

tautschnig · 2017-04-03T14:43:44Z

I don't necessarily think there is a performance problem - it just needs to be evaluated to make sure there is no such problem. The lack of evaluation infrastructure for doing this evaluation is a problem...

tautschnig · 2018-05-13T10:59:53Z

CI passes here, TG bump would be appreciated. I am meanwhile working on eliminating/clarifying init_l1 and then some performance evaluation.

smowton · 2018-05-14T07:52:49Z

https://github.com/diffblue/test-gen/pull/1811

tautschnig · 2018-05-14T11:26:23Z

I have now added two additional commits that clean up the code a fair bit, most notably is the init_l1 gone (and all the special-casing at the beginning of symex_assign_symbol). Could the TG run please be updated (if that's necessary)?

smowton · 2018-05-14T12:26:39Z

Updated.

smowton · 2018-05-14T14:47:39Z

Test-gen bump fails; it appears to break lots of tests, but they all have strings in common, so I suspect the string solver is being perturbed somehow. @romainbrenguier @allredj could either of you have a look here please?

tautschnig · 2018-05-14T14:52:44Z

If there's any info that can be shared (such as a failing assertion) then I'm happy to take a look. It is entirely possible that there are more places in the code that handle ID_symbol but don't yet handle ID_nondet_symbol.

Edit: I am meanwhile working on the performance analysis. There are some cases that show improvement, while others have considerable higher memory consumption, which I need to investigate.

smowton · 2018-05-14T14:52:07Z

src/goto-symex/symex_decl.cpp

@@ -90,10 +73,16 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
    state.top().hidden_function ||
    state.source.pc->source_location.get_hide();

-  target.decl(


Surprised the target doesn't get told of the declaration anymore?

That's a point worth considering, but really symex_targett::decl just bloats the formula. I might rather go one step further and remove it completely?!

smowton · 2018-05-14T14:54:49Z

src/ansi-c/c_typecheck_argc_argv.cpp

@@ -42,6 +42,7 @@ void c_typecheck_baset::add_argc_argv(const symbolt &main_symbol)
    argc_symbol.type=op0.type();
    argc_symbol.is_static_lifetime=true;
    argc_symbol.is_lvalue=true;
+    argc_symbol.value = side_effect_expr_nondett(op0.type());


This is surprising -- the convention elsewhere seems to be that a nil value implies nondet init (for example, Java globals)

Is that maybe only the case in Java? The one place that takes care of initialising globals is static_lifetime_init, which will zero-initialise all symbols that don't have a value (unless they are marked extern). Now of course the Java front-end had to do this in its very own way...

romainbrenguier · 2018-05-15T11:21:07Z

src/goto-symex/goto_symex_state.cpp

@@ -83,7 +83,7 @@ void goto_symex_statet::level1t::operator()(ssa_exprt &ssa_expr)
 /// "constants"
 bool goto_symex_statet::constant_propagation(const exprt &expr) const
 {
-  if(expr.is_constant())
+  if(expr.is_constant() || expr.id() == ID_nondet_symbol)


This commit ( cb6f737 ) seems to be breaking our string tests...

We can see the difference on this example:

public class test { public static int check(String s) { if(s.length()==2) return 2; if(s.length()==4) return 4; return s.length()+1; } }

running with options: jbmc test.class --refine-strings --function test.check --trace --string-max-length 100 --cover location --trace --json-ui
current develop as some assignment in the trace of the form

{ "assignmentType": "variable", "hidden": false, "internal": true, "lhs": "dynamic_object2", "mode": "java", "stepType": "assignment", "thread": 0, "value": { "elements": [ { "index": 0, "value": { "binary": "0000000000111111", "data": "(char)'?'", "name": "integer", "type": "char", "width": 16 } }, { "index": 1, "value": { "binary": "0000000000111111", "data": "(char)'?'", "name": "integer", "type": "char", "width": 16 } } ], "name": "array" } }

but with this commit, this is just replaced by

{ "assignmentType": "variable", "hidden": false, "internal": true, "lhs": "dynamic_object2", "mode": "java", "stepType": "assignment", "thread": 0, "value": { "name": "unknown" } }

Thank you for bisecting! I'll take a look and will try to figure out what is going on.

Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486]

Constant propagation now yields different right-hand sides in a test.

tautschnig · 2021-05-01T23:33:53Z

Closing as field sensitivity already covers possible benefits of this change.

tautschnig force-pushed the explicit-nondet-initialisation branch from 4efea63 to 17c27c1 Compare April 3, 2016 09:46

kroening self-assigned this Apr 18, 2016

tautschnig force-pushed the explicit-nondet-initialisation branch from 17c27c1 to 2b19b59 Compare May 18, 2016 16:58

tautschnig added enhancement Symbolic Execution labels May 29, 2016

tautschnig force-pushed the explicit-nondet-initialisation branch from 2b19b59 to e3767ec Compare May 30, 2016 11:39

tautschnig force-pushed the explicit-nondet-initialisation branch from e3767ec to d268552 Compare June 21, 2016 07:12

tautschnig force-pushed the explicit-nondet-initialisation branch from d268552 to a82ffaa Compare July 20, 2016 15:21

tautschnig force-pushed the explicit-nondet-initialisation branch from a82ffaa to c00ea94 Compare November 5, 2016 23:16

tautschnig force-pushed the explicit-nondet-initialisation branch from c00ea94 to 440d1e4 Compare November 17, 2016 20:58

tautschnig force-pushed the explicit-nondet-initialisation branch from 440d1e4 to f86fb0b Compare January 12, 2017 10:22

tautschnig mentioned this pull request Jan 20, 2017

Clean pr java front end #425

Merged

tautschnig force-pushed the explicit-nondet-initialisation branch from f86fb0b to 5d208a6 Compare January 25, 2017 21:23

forejtv assigned tautschnig and unassigned kroening Feb 21, 2017

tautschnig force-pushed the explicit-nondet-initialisation branch from 5d208a6 to 3090a26 Compare February 21, 2017 19:09

tautschnig mentioned this pull request Feb 22, 2017

Maintain ID_C_expr_simplified #37

Closed

forejtv assigned kroening and unassigned tautschnig Feb 22, 2017

tautschnig force-pushed the explicit-nondet-initialisation branch 3 times, most recently from 4242805 to 2262960 Compare April 10, 2017 10:05

tautschnig force-pushed the explicit-nondet-initialisation branch from 80f79a4 to 2775f9e Compare May 13, 2018 10:28

tautschnig force-pushed the explicit-nondet-initialisation branch from 2775f9e to 15c7af1 Compare May 14, 2018 11:22

tautschnig assigned romainbrenguier and allredj May 14, 2018

smowton reviewed May 14, 2018

View reviewed changes

romainbrenguier reviewed May 15, 2018

View reviewed changes

tautschnig unassigned romainbrenguier and allredj May 15, 2018

This was referenced May 22, 2018

nondet_initializer to build deep non-deterministic expressions #2219

Merged

Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486] #2220

Merged

tautschnig added a commit that referenced this pull request Dec 19, 2018

Merge pull request #2220 from tautschnig/phi-cleanup

a94389d

Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486]

tautschnig and others added 6 commits December 21, 2018 15:46

Flattening of ID_nondet_symbol for unbounded arrays

a007615

More constant propagation

9d44f13

Constant propagation now yields different right-hand sides in a test.

Explicitly initialise non-static objects with non-deterministic values

673e789

Fix for structs and nondet initialisation of pointers

e606e4f

Non-deterministic initialisation of argc/argv/envp

c5574b6

clang-format cleanup

efc5608

thk123 removed request for thk123 and mgudemann September 18, 2019 14:20

tautschnig force-pushed the explicit-nondet-initialisation branch from 15c7af1 to efc5608 Compare December 27, 2020 06:35

tautschnig requested a review from hannes-steffenhagen-diffblue as a code owner December 27, 2020 06:35

tautschnig closed this May 1, 2021

tautschnig mentioned this pull request Nov 1, 2024

[CONTRACTS] Detect loop locals with goto_rw in DFCC #8489

Merged

7 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Explicit nondet initialisation #35

Explicit nondet initialisation #35

tautschnig commented Mar 21, 2016

tautschnig commented Nov 17, 2016

peterschrammel commented Jan 11, 2017

tautschnig commented Jan 12, 2017

forejtv commented Feb 21, 2017

tautschnig commented Feb 22, 2017

forejtv commented Feb 22, 2017

kroening commented Apr 3, 2017

tautschnig commented Apr 3, 2017

tautschnig commented May 13, 2018

smowton commented May 14, 2018

tautschnig commented May 14, 2018

smowton commented May 14, 2018

smowton commented May 14, 2018

tautschnig commented May 14, 2018 •

edited

Loading

smowton May 14, 2018

tautschnig May 15, 2018

smowton May 14, 2018

tautschnig May 15, 2018

romainbrenguier May 15, 2018

romainbrenguier May 15, 2018

tautschnig May 15, 2018

tautschnig commented May 1, 2021

Explicit nondet initialisation #35

Explicit nondet initialisation #35

Conversation

tautschnig commented Mar 21, 2016

tautschnig commented Nov 17, 2016

peterschrammel commented Jan 11, 2017

tautschnig commented Jan 12, 2017

forejtv commented Feb 21, 2017

tautschnig commented Feb 22, 2017

forejtv commented Feb 22, 2017

kroening commented Apr 3, 2017

tautschnig commented Apr 3, 2017

tautschnig commented May 13, 2018

smowton commented May 14, 2018

tautschnig commented May 14, 2018

smowton commented May 14, 2018

smowton commented May 14, 2018

tautschnig commented May 14, 2018 • edited Loading

smowton May 14, 2018

Choose a reason for hiding this comment

tautschnig May 15, 2018

Choose a reason for hiding this comment

smowton May 14, 2018

Choose a reason for hiding this comment

tautschnig May 15, 2018

Choose a reason for hiding this comment

romainbrenguier May 15, 2018

Choose a reason for hiding this comment

romainbrenguier May 15, 2018

Choose a reason for hiding this comment

tautschnig May 15, 2018

Choose a reason for hiding this comment

tautschnig commented May 1, 2021

tautschnig commented May 14, 2018 •

edited

Loading