Some developer documentation for memory bounds checking #5228

danpoe · 2020-02-06T20:26:10Z

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/
n/a 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.

majakusber · 2020-02-06T21:29:11Z

Codecov Report

Merging #5228 into develop will decrease coverage by 1.55%.
The diff coverage is n/a.

@@             Coverage Diff             @@
##           develop    #5228      +/-   ##
===========================================
- Coverage    67.43%   65.88%   -1.56%     
===========================================
  Files         1157     1157              
  Lines        95354    95354              
===========================================
- Hits         64306    62828    -1478     
- Misses       31048    32526    +1478

Flag	Coverage Δ
#cproversmt2	`?`
#regression	`63.96% <ø> (ø)`	⬆️
#unit	`31.95% <ø> (ø)`	⬆️

Impacted Files	Coverage Δ
src/solvers/smt2/letify.cpp	`0.00% <0.00%> (-100.00%)`	⬇️
src/solvers/smt2/smt2_dec.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/solvers/floatbv/float_bv.h	`0.00% <0.00%> (-100.00%)`	⬇️
src/solvers/smt2/smt2irep.cpp	`0.00% <0.00%> (-88.00%)`	⬇️
src/solvers/floatbv/float_bv.cpp	`0.00% <0.00%> (-74.37%)`	⬇️
src/solvers/smt2/smt2_dec.cpp	`0.00% <0.00%> (-67.70%)`	⬇️
src/solvers/smt2/letify.h	`33.33% <0.00%> (-66.67%)`	⬇️
src/solvers/smt2/smt2_conv.h	`36.36% <0.00%> (-63.64%)`	⬇️
src/solvers/smt2/smt2_conv.cpp	`19.81% <0.00%> (-37.43%)`	⬇️
src/solvers/flattening/pointer_logic.cpp	`71.21% <0.00%> (-18.19%)`	⬇️
... and 17 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 cccdfd9...31e9f50. Read the comment docs.

xbauch · 2020-02-06T21:30:02Z

doc/architectural/memory-bounds-checking.md

+cbmc provides means to verify that pointers are within the bounds of (statically
+or dynamically) allocated memory blocks. When the option `--pointer-check` is
+used, cbmc checks the safety of each pointer dereference in the program.
+Similary, the primitive `__CPROVER_r_ok(pointer, size)` returns true when it is


Suggested change

Similary, the primitive `__CPROVER_r_ok(pointer, size)` returns true when it is

Similarly, the primitive `__CPROVER_r_ok(pointer, size)` returns true when it is

codecov-io · 2020-02-06T21:32:02Z

Codecov Report

Merging #5228 into develop will not change coverage.
The diff coverage is n/a.

@@           Coverage Diff            @@
##           develop    #5228   +/-   ##
========================================
  Coverage    67.43%   67.43%           
========================================
  Files         1157     1157           
  Lines        95352    95352           
========================================
  Hits         64302    64302           
  Misses       31050    31050

Flag	Coverage Δ
#cproversmt2	`42.67% <ø> (ø)`	⬆️
#regression	`63.96% <ø> (ø)`	⬆️
#unit	`31.95% <ø> (ø)`	⬆️

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 778fb97...18c0550. Read the comment docs.

xbauch · 2020-02-06T21:35:12Z

doc/architectural/memory-bounds-checking.md

+```
+
+Both internal variables `__CPROVER_malloc_object` and `__CPROVER_malloc_size`
+are initialised to 0 in the `__CPROVER_initialize()` function of a goto program.


I think at some point it was decided that we stick to the Oxford spelling in documentation, i.e. "are initialized ..".

majakusber · 2020-02-07T09:52:03Z

Oh no, my face on the codecov again 🤷‍♀️ If it happens third time, I'll look into it. I promise I'm not monitoring your work @xbauch 😅

xbauch · 2020-02-07T09:53:22Z

Oh no, my face on the codecov again If it happens third time, I'll look into it. I promise I'm not monitoring your work @xbauch

Not my work in this case; it seems you're somehow responsible for the coverage of cprover documentation.

majakusber · 2020-02-07T09:58:15Z

The second codecov report is correctly by codecov-io, and that one actually seems correct - documentation should show no change to coverage I guess. So I'm hoping someone/something fixed it (just as mysteriously as it started using my face) 🤞

xbauch

Looks good.

martin-cs

Don't suppose you want to document how memory leaks and use-after-free are handled do you? :-)

danpoe requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners February 6, 2020 20:26

xbauch reviewed Feb 6, 2020

View reviewed changes

danpoe force-pushed the doc/memory-bounds-checking branch from 31e9f50 to 259691c Compare February 7, 2020 11:04

peterschrammel approved these changes Feb 7, 2020

View reviewed changes

xbauch approved these changes Feb 7, 2020

View reviewed changes

martin-cs approved these changes Feb 7, 2020

View reviewed changes

danpoe force-pushed the doc/memory-bounds-checking branch from 259691c to 18c0550 Compare February 9, 2020 13:25

Some developer documentation for memory bounds checking

18c0550

danpoe merged commit 6680696 into diffblue:develop Feb 9, 2020

danpoe deleted the doc/memory-bounds-checking branch June 2, 2020 17:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Some developer documentation for memory bounds checking #5228

Some developer documentation for memory bounds checking #5228

Uh oh!

danpoe commented Feb 6, 2020 •

edited

Loading

Uh oh!

majakusber commented Feb 6, 2020

Uh oh!

xbauch Feb 6, 2020

Uh oh!

codecov-io commented Feb 6, 2020 •

edited

Loading

Uh oh!

xbauch Feb 6, 2020

Uh oh!

majakusber commented Feb 7, 2020

Uh oh!

xbauch commented Feb 7, 2020

Uh oh!

majakusber commented Feb 7, 2020

Uh oh!

xbauch left a comment

Uh oh!

martin-cs left a comment

Uh oh!

Uh oh!

	Similary, the primitive `__CPROVER_r_ok(pointer, size)` returns true when it is
	Similarly, the primitive `__CPROVER_r_ok(pointer, size)` returns true when it is

Some developer documentation for memory bounds checking #5228

Some developer documentation for memory bounds checking #5228

Uh oh!

Conversation

danpoe commented Feb 6, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

majakusber commented Feb 6, 2020

Codecov Report

Uh oh!

xbauch Feb 6, 2020

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Feb 6, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

xbauch Feb 6, 2020

Choose a reason for hiding this comment

Uh oh!

majakusber commented Feb 7, 2020

Uh oh!

xbauch commented Feb 7, 2020

Uh oh!

majakusber commented Feb 7, 2020

Uh oh!

xbauch left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

danpoe commented Feb 6, 2020 •

edited

Loading

codecov-io commented Feb 6, 2020 •

edited

Loading