Make pointer encoding sound wrt integer address translation (and lift object limits) #1086

tautschnig · 2017-07-04T14:18:41Z

Instead of encoding pointers with the same bit width a pointer on a given
platform has, just widen the bit-blasted encoding to include both the previous
object/offset encoding as well as an (integer) address. The encoding is thus
also trivially be extended to handle larger numbers of objects and offsets of
the same width as the address.

Furthermore clean up the code to encapsulate encoding properly, and make in-code
layout of pointer encoding more natural (it's now object, offset,
integer-address).

Fixes: #436
Fixes: #311
Fixes: #94

tautschnig · 2017-08-11T10:02:31Z

~~As far as I'm aware this is now complete (and working) for the SAT back end. The work left to be done is getting #982 merged, adjusting the SMT back ends to do the same.~~ [edit: done]

We would then no longer have any limit on the number of objects or the particular addresses that pointers take.

martin-cs · 2017-11-17T14:59:01Z

Another "how alive / urgent is this one" type question?

tautschnig · 2017-11-17T15:03:26Z

It has been among the top elements on my stack for the last couple of weeks; realistically it will stay there until Christmas...

tautschnig · 2017-12-08T16:21:38Z

This should be ready for review now. I am aware that possible feedback includes "please refactor into multiple, smaller PRs." All feedback appreciated (including that one). A known point of concern, voiced by @kroening earlier: the pointer flattening is not amenable to incremental use. Ideas to fix that are most welcome!

thk123

Reviewed the changes in src/analyses only - some suggestions for making it more obvious what is going on but in principle seems correct. They to be honest seem like they could be pulled into their own PR and merged quickly.

thk123 · 2017-12-21T11:31:14Z

src/analyses/goto_check.cpp

-     expr.id()==ID_minus)
+  if(expr.id()!=ID_plus &&
+     expr.id()!=ID_minus)
+    return;


Nit: since condition is multiple lines can you wrap the return in braces

thk123 · 2017-12-21T11:38:43Z

src/analyses/goto_check.cpp

+    // The overflow checks are binary!
+    // We break these up.
+
+    for(unsigned i=1; i<expr.operands().size(); i++)


I needed a pen and paper to fully get what was going on here. I wonder if a comment with an example explaining the calls to pointer_overflow_check would help?

// an operand with 4 children, a, b, c, d we: // first check (a, b) // then c with a temporary expression with two children: (a, b) // then d with a temporary expression with three children: (a, b, c)

thk123 · 2017-12-21T11:41:49Z

src/analyses/goto_check.cpp

+      else
+      {
+        tmp=expr;
+        tmp.operands().resize(i);


You may want to make it explicit here that you are chopping off the last nodes for now to do an intermediate check

thk123 · 2017-12-21T11:56:02Z

I've created a TG PR to verify this doesn't break anything, but TBH looks like it won't be a problem: diffblue/test-gen#1322

thk123 · 2017-12-21T14:51:17Z

TG PR fails, but for what looks like rebase reasons, can I ask for this PR to be rebased on to current head of develop?

smowton · 2018-01-05T15:03:51Z

Guessing this needs @kroening's opinion?

tautschnig · 2018-01-05T15:16:32Z

This mainly needs work on my end to enable incremental use.

tautschnig · 2018-04-15T23:00:26Z

I have now created #2059, #2060, #2061, #2062, #2063, #2064, #2065, #2066 (and might create at least one more) to place all the preparatory work in separate pull requests that can reasonably be reviewed.

peterschrammel · 2018-11-19T17:57:15Z

Test case from SV-COMP: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i

The tests exercise the way the back-end encodes pointers. Upcoming encoding changes will ensure that these can soundly be handled.

Rather than handling the object/offset bit width in multiple places, make boolbv_widtht the only place to provide this information.

This is in preparation of the flattened bit width of pointers not necessarily matching the width claimed by the front-end.

This keeps configurable aspects out of bv_pointerst.

Instead of encoding pointers with the same bit width a pointer on a given platform has, just widen the bit-blasted encoding to include both the previous object/offset encoding as well as an (integer) address. The encoding is thus also trivially extended to handle larger numbers of objects and offsets of the same width as the address. Furthermore clean up the code to encapsulate encoding properly, and make in-code layout of pointer encoding more natural (it's now object, offset, integer-address). Fixes: diffblue#436 Fixes: diffblue#311 Fixes: diffblue#94

codecov · 2021-02-12T23:01:11Z

Codecov Report

Merging #1086 (bb9c198) into develop (23c11e8) will decrease coverage by 36.82%.
The diff coverage is 15.32%.

@@             Coverage Diff              @@
##           develop    #1086       +/-   ##
============================================
- Coverage    69.08%   32.25%   -36.83%     
============================================
  Files         1242      984      -258     
  Lines       100842    83944    -16898     
============================================
- Hits         69667    27080    -42587     
- Misses       31175    56864    +25689

Flag	Coverage Δ
regression	`?`
unit	`32.25% <15.32%> (-0.03%)`	⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/solvers/flattening/boolbv_byte_extract.cpp	`0.00% <0.00%> (-72.59%)`	⬇️
src/solvers/flattening/boolbv_byte_update.cpp	`0.00% <0.00%> (-100.00%)`	⬇️
src/solvers/flattening/boolbv_width.h	`100.00% <ø> (ø)`
src/solvers/flattening/bv_pointers.h	`11.11% <0.00%> (-88.89%)`	⬇️
src/solvers/flattening/pointer_logic.h	`0.00% <ø> (-50.00%)`	⬇️
src/solvers/smt2/smt2_conv.cpp	`0.00% <0.00%> (-31.31%)`	⬇️
src/solvers/flattening/bv_pointers.cpp	`16.37% <14.83%> (-66.69%)`	⬇️
src/solvers/flattening/boolbv_width.cpp	`39.25% <100.00%> (-33.20%)`	⬇️
src/solvers/flattening/pointer_logic.cpp	`8.95% <100.00%> (-72.87%)`	⬇️
src/cpp/cpp_id.h	`0.00% <0.00%> (-100.00%)`	⬇️
... and 963 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 23c11e8...bb9c198. Read the comment docs.

TGWDB · 2021-08-05T10:34:26Z

@tautschnig This looks interesting but very out of date now. I notice it was close to the top of your stack a few years ago, does that still hold, or has this fallen too far down to keep open? Generally we'd like to close old PRs that are not going to happen.

TGWDB · 2021-09-13T13:22:19Z

Closing due to age and not being actively worked on. Please reopen if you believe this is erroneous and new work towards merging this PR has progressed.

tautschnig added the do not merge label Jul 4, 2017

tautschnig self-assigned this Jul 4, 2017

tautschnig force-pushed the memory-region branch 2 times, most recently from 445790a to 16d81cb Compare July 6, 2017 13:20

tautschnig force-pushed the memory-region branch from 16d81cb to a029209 Compare July 15, 2017 10:22

tautschnig mentioned this pull request Jul 21, 2017

Set addr_bits via command line and per language #1161

Closed

tautschnig force-pushed the memory-region branch from a029209 to 078e2f5 Compare August 11, 2017 09:58

tautschnig changed the title ~~Change pointer encoding to include integer addresses~~ Make pointer encoding sound wrt integer address translation (and lift object limits) Aug 11, 2017

tautschnig changed the title ~~Make pointer encoding sound wrt integer address translation (and lift object limits)~~ [depends: #982] Make pointer encoding sound wrt integer address translation (and lift object limits) Aug 11, 2017

tautschnig force-pushed the memory-region branch 2 times, most recently from 6fdf7d2 to 11bd809 Compare August 14, 2017 13:15

tautschnig removed their assignment Aug 14, 2017

tautschnig added the bugfix label Aug 14, 2017

tautschnig mentioned this pull request Aug 15, 2017

Fixes and improvements to dynamic memory handling #982

Merged

tautschnig force-pushed the memory-region branch from 11bd809 to fb32812 Compare August 15, 2017 16:44

tautschnig self-assigned this Aug 20, 2017

tautschnig changed the base branch from master to develop August 22, 2017 12:21

tautschnig changed the title ~~[depends: #982] Make pointer encoding sound wrt integer address translation (and lift object limits)~~ Make pointer encoding sound wrt integer address translation (and lift object limits) Sep 1, 2017

tautschnig force-pushed the memory-region branch from fb32812 to 0932597 Compare September 1, 2017 11:10

tautschnig mentioned this pull request Nov 1, 2017

SV-COMP 2018: Rebase of Tautschnig's branch/PR sv-comp-2017 on cbmc/develop #1532

Closed

tautschnig force-pushed the memory-region branch from 0932597 to f8328fb Compare November 9, 2017 18:09

tautschnig requested review from kroening, martin-cs, peterschrammel, romainbrenguier and thk123 as code owners November 9, 2017 18:09

tautschnig force-pushed the memory-region branch from 56fb5c9 to 1d2a052 Compare December 8, 2017 13:04

thk123 approved these changes Dec 21, 2017

View reviewed changes

tautschnig mentioned this pull request Apr 6, 2018

bv_cbmct::unbounded_arrayt::U_AUTO is never enabled #2018

Open

tautschnig force-pushed the memory-region branch from 1d2a052 to 89bd8d5 Compare April 15, 2018 22:43

tautschnig force-pushed the memory-region branch from 89bd8d5 to d53377b Compare April 18, 2018 10:28

tautschnig mentioned this pull request Jun 14, 2018

[SV-COMP'18 5/19] Abort concurrency encoding in possibly unsound cases #1994

Merged

tautschnig mentioned this pull request Jun 14, 2019

Handle representation clause address diffblue/gnat2goto#233

Open

tautschnig mentioned this pull request Nov 13, 2020

Synchronise goto-cc command-line options to re-enable Windows regression tests #5572

Closed

3 tasks

tautschnig added 4 commits February 12, 2021 18:05

Tests demonstrating pointer-encoding unsoundness

a4e2c1b

The tests exercise the way the back-end encodes pointers. Upcoming encoding changes will ensure that these can soundly be handled.

Store pointer encoding configuration in boolbv_widtht

e6d5d49

Rather than handling the object/offset bit width in multiple places, make boolbv_widtht the only place to provide this information.

Lower byte_{extract,update} when pointers are involved

ea5c3bc

This is in preparation of the flattened bit width of pointers not necessarily matching the width claimed by the front-end.

Store null-pointer-is-zero in pointer_logict

726a92f

This keeps configurable aspects out of bv_pointerst.

tautschnig force-pushed the memory-region branch from d53377b to 1b0e0cf Compare February 12, 2021 22:24

tautschnig requested review from allredj and hannes-steffenhagen-diffblue as code owners February 12, 2021 22:24

tautschnig force-pushed the memory-region branch from 1b0e0cf to dc0b605 Compare February 12, 2021 22:37

tautschnig force-pushed the memory-region branch from dc0b605 to bb9c198 Compare February 12, 2021 22:37

tautschnig mentioned this pull request May 19, 2021

Spurious malloc behavior for large allocations #6130

Closed

TGWDB closed this Sep 13, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make pointer encoding sound wrt integer address translation (and lift object limits) #1086

Make pointer encoding sound wrt integer address translation (and lift object limits) #1086

tautschnig commented Jul 4, 2017 •

edited

Loading

tautschnig commented Aug 11, 2017 •

edited

Loading

martin-cs commented Nov 17, 2017

tautschnig commented Nov 17, 2017

tautschnig commented Dec 8, 2017

thk123 left a comment

thk123 Dec 21, 2017

thk123 Dec 21, 2017

thk123 Dec 21, 2017

thk123 commented Dec 21, 2017

thk123 commented Dec 21, 2017

smowton commented Jan 5, 2018

tautschnig commented Jan 5, 2018

tautschnig commented Apr 15, 2018

peterschrammel commented Nov 19, 2018

codecov bot commented Feb 12, 2021 •

edited

Loading

TGWDB commented Aug 5, 2021

TGWDB commented Sep 13, 2021

Make pointer encoding sound wrt integer address translation (and lift object limits) #1086

Make pointer encoding sound wrt integer address translation (and lift object limits) #1086

Conversation

tautschnig commented Jul 4, 2017 • edited Loading

tautschnig commented Aug 11, 2017 • edited Loading

martin-cs commented Nov 17, 2017

tautschnig commented Nov 17, 2017

tautschnig commented Dec 8, 2017

thk123 left a comment

Choose a reason for hiding this comment

thk123 Dec 21, 2017

Choose a reason for hiding this comment

thk123 Dec 21, 2017

Choose a reason for hiding this comment

thk123 Dec 21, 2017

Choose a reason for hiding this comment

thk123 commented Dec 21, 2017

thk123 commented Dec 21, 2017

smowton commented Jan 5, 2018

tautschnig commented Jan 5, 2018

tautschnig commented Apr 15, 2018

peterschrammel commented Nov 19, 2018

codecov bot commented Feb 12, 2021 • edited Loading

Codecov Report

TGWDB commented Aug 5, 2021

TGWDB commented Sep 13, 2021

tautschnig commented Jul 4, 2017 •

edited

Loading

tautschnig commented Aug 11, 2017 •

edited

Loading

codecov bot commented Feb 12, 2021 •

edited

Loading