Repository navigation

Changes to the compartment model - #2

Open

jeremyThibault wants to merge 87 commits into

cross-external-call-removal

Commits on Nov 10, 2023

initial working port of events
AndrewTolmach
committed
28b7b96
a fairly clean version
AndrewTolmach
committed
45d476c

Commits on Nov 16, 2023

Start removing the cross-compartment calls. Remove all compartments from external functions
jeremyThibault
committed
8fb5bb5

Commits on Nov 20, 2023

[Compartment model] Continue generalizing the compartment model
jeremyThibault
committed
2d16557

Commits on Nov 23, 2023

[Compartments] Continue fixing the compartment model, with changes in the builtins
jeremyThibault
committed
cb74dc2

Commits on Nov 24, 2023

[Compartments] Fix Selectionproof.v and modify RTL.v
jeremyThibault
committed
051e5c6

Commits on Nov 26, 2023

[Compartments] Restore two instances removed by mistake
jeremyThibault
committed
769c0e2
[Compartments] Fix RTLgenproof.v
jeremyThibault
committed
8edd816
[Compartments] Fix Tailcall pass
jeremyThibault
committed
30dbad3
[Compartments] Fix Inlining pass
jeremyThibault
committed
d85d37e
[Compartments] Fixers to RTLtyping, Renumber pass, and Cop/Ctypes
jeremyThibault
committed
363a5af
[Compartments] Various fixes in Allocation, Tunneling, Unusedglob, Csyntax, Events, and Memory
jeremyThibault
committed
4754b08

Commits on Dec 3, 2023

[Compartments] Fix the compilation process from start to end
jeremyThibault
committed
5173743

Commits on Dec 4, 2023

[Compartments] Little fixes
jeremyThibault
committed
e28fdea

Commits on Dec 7, 2023

Commits on Dec 8, 2023

Commits on Dec 11, 2023

Commits on Dec 13, 2023

Make all runs of tests deterministic and reproducible
argsv
committed
61baedb
Extract export of clight programs to compilable c files in custom module
argsv
committed
c99987b
Implement output functions for memory_deltas
argsv
committed
afb99de

Commits on Dec 15, 2023

Commits on Dec 18, 2023

Find block for each global var to ensure the inversion in BT works
argsv
committed
dabf3c8
Avoid linker errors for external symbols
argsv
committed
59912cb
Improve exporting/post-processing to fix more errors
argsv
committed
9128c30
Always print a global root seed for reproducibility
argsv
committed
5449c07
Ensure that pointer values in mem_deltas refer to valid global vars
argsv
committed
fb628b9
Ensure that we only write to non-const global variables
argsv
committed
5fe8f22
Fix type errors with more post-processing
argsv
committed
1d92355
Fix warning (tests now work also for non-empty memory deltas)
argsv
committed
7bf3f17

Commits on Dec 19, 2023

Commits on Jan 12, 2024

Harden against kill/abort signals for long runs
argsv
committed
dfadf6a

Commits on Jan 15, 2024

Commits on Jan 18, 2024

Commits on Jan 19, 2024

Support vstore and vload as external functions
argsv
committed
167b68e
[common] Fix proofs in linking
jeremyThibault
committed
0269bd7

Commits on Jan 21, 2024

[Backtranslation] Fix some proofs, readd one axiom about external calls (do not free non freeable blocks)
jeremyThibault
committed
2e6904f

Commits on Jan 22, 2024

[Backtranslation] WIP fixing backtranslation
jeremyThibault
committed
6051560

Commits on Jan 23, 2024

[Backtranslation] Progress integrating backtranslation proof
jeremyThibault
committed
184f10d
[Backtranslation] Checkpoint
jeremyThibault
committed
132733e

Commits on Jan 25, 2024

Add results02.txt from second and improved long run on server
argsv
committed
2b0c34d

Commits on Jan 28, 2024

Commits on Jan 29, 2024

Small fix
jeremyThibault
committed
0223a9d
Small fix again
jeremyThibault
committed
5efe296
Comments on technical lemmas
jeremyThibault
committed
93bf5e4
Fix
jeremyThibault
committed
4fca9b2

Commits on Feb 4, 2024

Fix correctness
jeremyThibault
committed
494a6f2