Code

Stacked Borrows in Kani#3406

Code

Merged

jsalzbergedu merged 74 commits intomodel-checking:aliasing-checksmodel-checking/kani:aliasing-checksfrom jsalzbergedu:mainjsalzbergedu/kani:mainCopy head branch name to clipboardAug 30, 2024

+1,512-24

Commits

Commits on Aug 1, 2024

• Add empty pass

  

  Jacob Salzberg

  committed
  829c3c0

  Copy full SHA for 829c3c0

Commits on Aug 2, 2024

• Add "boxed" test for pointers into the heap.

  

  Jacob Salzberg

  committed
  052545d

  Copy full SHA for 052545d

Commits on Aug 9, 2024

• Add Stacked Borrows instrumentation code for stack allocations

  

  Jacob Salzberg

  committed
  ba92c6b

  Copy full SHA for ba92c6b

• Fix dup. write code to take raw pointer from ref, not org. var

  

  Jacob Salzberg

  committed
  060cc6f

  Copy full SHA for 060cc6f

• Remove std/kani functions to get efficient impl.

  

  Jacob Salzberg

  committed
  63390fb

  Copy full SHA for 63390fb

Commits on Aug 10, 2024

• Instrument new stack references.

  

  Jacob Salzberg

  committed
  b503aa0

  Copy full SHA for b503aa0

Commits on Aug 11, 2024

• Add case x: *mut T = &raw *(y as &mut T);

  

  Jacob Salzberg

  committed
  bb6045b

  Copy full SHA for bb6045b

Commits on Aug 12, 2024

• Match both lvalue and rvalue projections

  

  Jacob Salzberg

  committed
  8df3234

  Copy full SHA for 8df3234

• Uncomment important lines

  

  Jacob Salzberg

  committed
  c732b70

  Copy full SHA for c732b70

• Instrument with use_2

  

  Jacob Salzberg

  committed
  4e298ce

  Copy full SHA for 4e298ce

• Add println statements for failing stack checks

  

  Jacob Salzberg

  committed
  a8e8470

  Copy full SHA for a8e8470

• To clear noise, instrument for non-kani in macros.

  

  Jacob Salzberg

  committed
  0294688

  Copy full SHA for 0294688

Commits on Aug 13, 2024

• Instrument duplicate write in both the rust and kani setting.

  

  Jacob Salzberg

  committed
  dca76d9

  Copy full SHA for dca76d9

• Make test pass

  

  Jacob Salzberg

  committed
  820584f

  Copy full SHA for 820584f

• Add one without macro invocations to show the instrumentation works

  

  Jacob Salzberg

  committed
  6327437

  Copy full SHA for 6327437

Commits on Aug 14, 2024

• Clean up for pr review

  

  Jacob Salzberg

  committed
  621287c

  Copy full SHA for 621287c

• apply formatter

  

  Jacob Salzberg

  committed
  05032da

  Copy full SHA for 05032da

• Commit and refactor

  

  Jacob Salzberg

  committed
  c39e8ca

  Copy full SHA for c39e8ca

Commits on Aug 15, 2024

• Add tests for C99 format locals and for control flow.

  Show description for e6126f4
  

  Jacob Salzberg

  committed
  e6126f4

  Copy full SHA for e6126f4

• Refactor imports

  

  Jacob Salzberg

  committed
  26623ce

  Copy full SHA for 26623ce

• Factor out local collection; local indices now computed directly

  

  Jacob Salzberg

  committed
  5155f36

  Copy full SHA for 5155f36

• Remove pub(self)

  

  Jacob Salzberg

  committed
  a0fe559

  Copy full SHA for a0fe559

• Add documentation for the module sstate.

  

  Jacob Salzberg

  committed
  ef833b2

  Copy full SHA for ef833b2

• Add demonic nondeterminism blurb

  

  Jacob Salzberg

  committed
  553c737

  Copy full SHA for 553c737

• provisionally add line numbers; tests failing

  

  Jacob Salzberg

  committed
  5df2dbc

  Copy full SHA for 5df2dbc

• Remove extraneous assertion

  

  Jacob Salzberg

  committed
  a190e1c

  Copy full SHA for a190e1c

Commits on Aug 16, 2024

• Merge remote-tracking branch 'kani/main'

  

  Jacob Salzberg

  committed
  6ce6942

  Copy full SHA for 6ce6942

• Make the pass compile on the current compiler version

  

  Jacob Salzberg

  committed
  79d40ad

  Copy full SHA for 79d40ad

Commits on Aug 19, 2024

• Change test to emit line number.

  Show description for 4a718f7
  

  Jacob Salzberg

  committed
  4a718f7

  Copy full SHA for 4a718f7

• Delete redundant tests, provide accurate line #s.

  

  Jacob Salzberg

  committed
  cf3e19c

  Copy full SHA for cf3e19c

Commits on Aug 23, 2024

• Improve error reporting.

  Show description for afc5eca
  

  Jacob Salzberg

  committed
  afc5eca

  Copy full SHA for afc5eca

• Document the actions module.

  

  Jacob Salzberg

  committed
  f0efc1e

  Copy full SHA for f0efc1e

• Add doc comments for each of the instrumentation data fields.

  

  Jacob Salzberg

  committed
  84ed701

  Copy full SHA for 84ed701

• -visibility, -raw MIR manipulation, -blacklist, +doc

  Show description for 1877591
  

  Jacob Salzberg

  committed
  1877591

  Copy full SHA for 1877591

• Add module level documentation + copyrights

  

  Jacob Salzberg

  committed
  4fd5842

  Copy full SHA for 4fd5842

• Add message to assertion

  

  Jacob Salzberg

  committed
  a742547

  Copy full SHA for a742547

• Apply formatter

  

  Jacob Salzberg

  committed
  69fd136

  Copy full SHA for 69fd136

• Remove extraneous arg

  

  Jacob Salzberg

  committed
  6b76832

  Copy full SHA for 6b76832

Commits on Aug 26, 2024

• Begin implementing artem's comments

  

  Jacob Salzberg

  committed
  3376a93

  Copy full SHA for 3376a93

• Fix code actions

  

  Jacob Salzberg

  committed
  dc332a7

  Copy full SHA for dc332a7

• Redo expected files with new line info

  

  Jacob Salzberg

  committed
  fb388f3

  Copy full SHA for fb388f3

• Notify the user of all unhandled cases

  

  Jacob Salzberg

  committed
  0c17fdd

  Copy full SHA for 0c17fdd

• Notify the user that term. does not change sb state

  

  Jacob Salzberg

  committed
  3cffb18

  Copy full SHA for 3cffb18

• Combine object & offset to reduce looping

  

  Jacob Salzberg

  committed
  fa201bc

  Copy full SHA for fa201bc

Commits on Aug 27, 2024

• Fix all monitor code to use nondet offset

  

  Jacob Salzberg

  committed
  25958c6

  Copy full SHA for 25958c6

• Run formatter

  

  Jacob Salzberg

  committed
  a86399d

  Copy full SHA for a86399d

• Add copyright info

  

  Jacob Salzberg

  committed
  c236c20

  Copy full SHA for c236c20

• Update for clippy

  

  Jacob Salzberg

  committed
  cda8657

  Copy full SHA for cda8657

• Fix lint on range

  

  Jacob Salzberg

  committed
  db2c570

  Copy full SHA for db2c570

• Run kani fmt

  

  Jacob Salzberg

  committed
  9953526

  Copy full SHA for 9953526

• More clippy lints

  

  Jacob Salzberg

  committed
  f0183d2

  Copy full SHA for f0183d2

• Update line numbers

  

  Jacob Salzberg

  committed
  cab1067

  Copy full SHA for cab1067

Commits on Aug 28, 2024

• Begin implementing the backwards pass artem suggested

  

  Jacob Salzberg

  committed
  0e99f41

  Copy full SHA for 0e99f41

• Continue implementing the changes Artem suggested

  

  Jacob Salzberg

  committed
  cff2102

  Copy full SHA for cff2102

Commits on Aug 29, 2024

• Complete instrumentation of instructions accum. by visitor

  

  Jacob Salzberg

  committed
  05cb010

  Copy full SHA for 05cb010

• Comment the instrumentation file

  

  Jacob Salzberg

  committed
  b447898

  Copy full SHA for b447898

• Comment the visitor file

  

  Jacob Salzberg

  committed
  aa0e691

  Copy full SHA for aa0e691

• Fix warnings, regression caused by terminator case

  

  Jacob Salzberg

  committed
  a4133c4

  Copy full SHA for a4133c4

• Merge branch 'kani-main'

  

  Jacob Salzberg

  committed
  e3ee7b1

  Copy full SHA for e3ee7b1

• Modify comments, change to enums.

  

  Jacob Salzberg

  committed
  61f8ce7

  Copy full SHA for 61f8ce7

• Try using bool instead

  

  Jacob Salzberg

  committed
  07028ee

  Copy full SHA for 07028ee

• Address performance regression by using assoc. constants

  

  Jacob Salzberg

  committed
  623278b

  Copy full SHA for 623278b

• Run kani-fmt

  

  Jacob Salzberg

  committed
  00ef0e9

  Copy full SHA for 00ef0e9

• Remove local variable that is only an alias

  

  Jacob Salzberg

  committed
  a4bb9be

  Copy full SHA for a4bb9be

• Remove unhelpful doc comment

  

  Jacob Salzberg

  committed
  3a2d693

  Copy full SHA for 3a2d693

• Fix tag --> PointerTag

  

  Jacob Salzberg

  committed
  443fb61

  Copy full SHA for 443fb61

Commits on Aug 30, 2024

• Cache FnDef instead of Instance; document test cases

  

  Jacob Salzberg

  committed
  23dad3b

  Copy full SHA for 23dad3b

• Update comment

  

  Jacob Salzberg

  committed
  a36a451

  Copy full SHA for a36a451

• Separate the constants and the types. Use the underlying value size.

  

  Jacob Salzberg

  committed
  16e4bdc

  Copy full SHA for 16e4bdc

• Remove unneccessary "use self::*" in functions

  

  Jacob Salzberg

  committed
  cfbb31e

  Copy full SHA for cfbb31e

• Move lookup into the if block

  

  Jacob Salzberg

  committed
  846975d

  Copy full SHA for 846975d

• Add size of val everywhere

  

  Jacob Salzberg

  committed
  9f10545

  Copy full SHA for 9f10545

• Add assertions, initialize in track_local

  

  Jacob Salzberg

  committed
  f24c327

  Copy full SHA for f24c327

• Clarify index comment

  

  Jacob Salzberg

  committed
  e33d6e9

  Copy full SHA for e33d6e9