Code

[CN-exec] Runtime loop invariants#723

Code

Open

rbanerjee20 wants to merge 16 commits intorems-project:masterrems-project/cerberus:masterfrom rbanerjee20:runtime-loop-invariantsrbanerjee20/cerberus:runtime-loop-invariantsCopy head branch name to clipboard

+414-137

Commits

Commits on Nov 19, 2024

• tiny script update

  rbanerjee20

  committed
  e0aae33

  Copy full SHA for e0aae33

• start loop plumbing

  rbanerjee20

  committed
  915c3fd

  Copy full SHA for 915c3fd

• Add functions for separating variable declarations for loop purposes, and add plumbing through to executable spec for whole loop location

  rbanerjee20

  committed
  26ecba6

  Copy full SHA for 26ecba6

Commits on Nov 20, 2024

• Complete loop invariant plumbing + disable internal VIP allocations in executable spec mode

  rbanerjee20

  committed
  c4dba37

  Copy full SHA for c4dba37

• Runtime loop invariants compiling and running

  rbanerjee20

  committed
  6bb6d4c

  Copy full SHA for 6bb6d4c

• Separate stack depth decr and postcondition leak check

  rbanerjee20

  committed
  4cbe251

  Copy full SHA for 4cbe251

• runtime lib separation of decr and leak check

  rbanerjee20

  committed
  878162d

  Copy full SHA for 878162d

• Add translation for computational arguments

  rbanerjee20

  committed
  dafc858

  Copy full SHA for dafc858

• End to end runtime loop invariants working for small example

  rbanerjee20

  committed
  ea6ff8b

  Copy full SHA for ea6ff8b

• Fix binding issue so runtime memcpy loop invariant working

  rbanerjee20

  committed
  586ff60

  Copy full SHA for 586ff60

Commits on Nov 21, 2024

• review changes

  rbanerjee20

  committed
  bce179a

  Copy full SHA for bce179a

• minor fixes

  rbanerjee20

  committed
  af0d56f

  Copy full SHA for af0d56f

• Propagate executable spec Ctype printing in GCC statement as expression

  rbanerjee20

  committed
  0e26633

  Copy full SHA for 0e26633

• format

  rbanerjee20

  committed
  dd5290d

  Copy full SHA for dd5290d

Commits on Nov 22, 2024

• experiments for not repeating bindings across loops

  rbanerjee20

  committed
  aa438e6

  Copy full SHA for aa438e6

Commits on Dec 30, 2024

• Pre-deadline loop invariant changes

  rbanerjee20

  committed
  20a763c

  Copy full SHA for 20a763c