Rearchitect var args support (making it actually work) [blocks: #4329] #4238

tautschnig · 2019-02-21T00:39:05Z

Previously all the logic to access values of variable argument lists was put
into our va_arg() implementation. This required guessing what the parameters
could have been, and did not take into account the initial value passed to
va_start.

Now va_start triggers constructing an array of pointers to parameters, the first
of which is the original argument to va_start. The va_list is then just a
pointer to the first element of the array. va_arg just increments the pointer.
goto_program conversion places a side_effect_exprt where va_start was, and
goto-symex populates the array with the actual values applicable for a
particular invocation of the function.

Each commit message has a non-empty body, explaining why the change was made.
n/a 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.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2019-02-21T23:11:29Z

Apologies for dragging in some many reviewers, that's just because I had to add the commits from #2068 to make things also work with the approach that Visual Studio uses for var args. Just the last three commits in this PR are actually new.

allredj

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

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 93ba1d6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102970072
Status will be re-evaluated on next push.
Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).
the compatibility was already broken by an earlier merge.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 7755806).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102970915
Status will be re-evaluated on next push.
Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).
the compatibility was already broken by an earlier merge.

allredj

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

martin-cs

Very little touches my areas of responsibility but those bits ae fine.

allredj

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

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: dfd298a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108813088
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

kroening · 2019-05-15T09:46:47Z

regression/cbmc/va_list3/windows-preprocessed.desc

+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring


Can you add a comment, say in the .desc file, how windows-preprocessed.i was produced?

It was kind-of noted in the commit message, but I'll add a note in the .desc file as well!

kroening · 2019-05-15T09:47:48Z

src/ansi-c/expr2c.cpp

-    else if(statement==ID_gcc_builtin_va_arg_next)
-      return convert_function(src, "gcc_builtin_va_arg_next");
+    else if(statement == ID_va_start)
+      return convert_function(src, CPROVER_PREFIX "va_start");
    else


Does dumping still work with that change? Meaning do we still get a C program that gcc compiles?

The changes (in this PR) to goto-instrument/goto_program2code.cpp take care of this.

kroening · 2019-05-15T09:54:23Z

src/solvers/flattening/bv_pointers.cpp

-      op_type.id() == ID_bool || op_type.id() == ID_c_enum ||
-      op_type.id() == ID_c_enum_tag || op_type.id() == ID_bv)
+      can_cast_type<bitvector_typet>(op_type) || op_type.id() == ID_c_enum ||
+      op_type.id() == ID_c_enum_tag)
    {


Note that ID_bool is not a bit vector type, i.e., this case is lost.

Ah, thanks, fixed!

kroening · 2019-05-15T09:56:19Z

src/goto-symex/symex_builtin_functions.cpp

+      fits_slot,
+      typecast_exprt::conditional_cast(parameter_expr, void_ptr_type),
+      typecast_exprt::conditional_cast(
+        address_of_exprt{parameter_expr}, void_ptr_type)};


I am a bit surprised that this distinction needs to be a formula -- sure this isn't known at compile time?

I believe that almost always the simplifier will be able to take care of this - but apart from that this used to construct an object that doesn't even exist at compile time, so I'm not really sure what you'd like me to do?

Even floating-point values are ok to just be re-interpreted as bit strings.

This will aid debugging as Visual Studio mostly just uses macros to implement the va_* functions.

We carry typedef names all the way now, there is no need for additional annotations to preserve the typedef name of va_list for dump-c.

Previously all the logic to access values of variable argument lists was put into our va_arg() implementation. This required guessing what the parameters could have been, and did not take into account the initial value passed to va_start. Now va_start triggers constructing an array of pointers to parameters, the first of which is the original argument to va_start. The va_list is then just a pointer to the first element of the array. va_arg just increments the pointer. goto_program conversion places a side_effect_exprt where va_start was, and goto-symex populates the array with the actual values applicable for a particular invocation of the function.

allredj

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

tautschnig added the bugfix label Feb 21, 2019

tautschnig requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, peterschrammel, pkesseli and smowton as code owners February 21, 2019 00:39

tautschnig changed the title ~~Rearchitect var args support (making it actually work)~~ Rearchitect var args support (making it actually work) [blocks: #4329] Feb 21, 2019

tautschnig added the blocker label Feb 21, 2019

tautschnig force-pushed the var-args branch from 40a5b94 to 278efde Compare February 21, 2019 01:17

tautschnig self-assigned this Feb 21, 2019

tautschnig force-pushed the var-args branch from 278efde to d1cbaad Compare February 21, 2019 22:27

tautschnig requested review from allredj and romainbrenguier as code owners February 21, 2019 22:27

tautschnig changed the title ~~Rearchitect var args support (making it actually work) [blocks: #4329]~~ Rearchitect var args support (making it actually work) [depends-on: #2068, blocks: #4329] Feb 21, 2019

tautschnig added the dependent - do not merge label Feb 21, 2019

smowton approved these changes Feb 22, 2019

View reviewed changes

tautschnig force-pushed the var-args branch 2 times, most recently from 33cbaa7 to 6c85222 Compare February 22, 2019 20:05

tautschnig changed the title ~~Rearchitect var args support (making it actually work) [depends-on: #2068, blocks: #4329]~~ Rearchitect var args support (making it actually work) [blocks: #4329] Feb 26, 2019

tautschnig removed the dependent - do not merge label Feb 26, 2019

tautschnig force-pushed the var-args branch from 6c85222 to ec8797e Compare February 26, 2019 19:17

tautschnig assigned kroening, peterschrammel and chrisr-diffblue and unassigned tautschnig Feb 26, 2019

allredj reviewed Feb 27, 2019

View reviewed changes

peterschrammel approved these changes Mar 3, 2019

View reviewed changes

peterschrammel removed their assignment Mar 3, 2019

tautschnig force-pushed the var-args branch from ec8797e to 93ba1d6 Compare March 3, 2019 21:08

tautschnig removed the Needs rebase label Mar 3, 2019

tautschnig unassigned chrisr-diffblue Mar 3, 2019

tautschnig force-pushed the var-args branch from 93ba1d6 to 7755806 Compare March 3, 2019 21:26

allredj reviewed Mar 3, 2019

View reviewed changes

tautschnig force-pushed the var-args branch 2 times, most recently from 617c92a to 00f323d Compare March 12, 2019 12:30

allredj reviewed Mar 12, 2019

View reviewed changes

martin-cs approved these changes Mar 26, 2019

View reviewed changes

tautschnig force-pushed the var-args branch from 00f323d to 0c5f08c Compare March 26, 2019 08:13

allredj reviewed Mar 26, 2019

View reviewed changes

tautschnig force-pushed the var-args branch from 0c5f08c to dfd298a Compare April 18, 2019 07:24

allredj reviewed Apr 18, 2019

View reviewed changes

tautschnig force-pushed the var-args branch from dfd298a to cdc6726 Compare April 30, 2019 23:44

kroening reviewed May 15, 2019

View reviewed changes

tautschnig added 4 commits May 15, 2019 11:24

Typecast to pointer: support all bitvector types

163f629

Even floating-point values are ok to just be re-interpreted as bit strings.

Add Visual Studio 2017 preprocessed variant of va_list3 test

5358144

This will aid debugging as Visual Studio mostly just uses macros to implement the va_* functions.

Remove ID_gcc_builtin_va_list

f5a14db

We carry typedef names all the way now, there is no need for additional annotations to preserve the typedef name of va_list for dump-c.

tautschnig force-pushed the var-args branch from cdc6726 to 18cbd69 Compare May 15, 2019 11:24

allredj reviewed May 15, 2019

View reviewed changes

kroening approved these changes May 15, 2019

View reviewed changes

kroening merged commit bc76446 into diffblue:develop May 15, 2019

tautschnig deleted the var-args branch May 16, 2019 08:39

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rearchitect var args support (making it actually work) [blocks: #4329] #4238

Rearchitect var args support (making it actually work) [blocks: #4329] #4238

tautschnig commented Feb 21, 2019

tautschnig commented Feb 21, 2019

allredj left a comment

allredj left a comment

allredj left a comment

allredj left a comment

martin-cs left a comment

allredj left a comment

allredj left a comment

kroening May 15, 2019

tautschnig May 15, 2019

kroening May 15, 2019

tautschnig May 15, 2019

kroening May 15, 2019

tautschnig May 15, 2019

kroening May 15, 2019

tautschnig May 15, 2019

allredj left a comment

Rearchitect var args support (making it actually work) [blocks: #4329] #4238

Rearchitect var args support (making it actually work) [blocks: #4329] #4238

Conversation

tautschnig commented Feb 21, 2019

tautschnig commented Feb 21, 2019

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a 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