Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[CN-exec] Runtime loop invariants #884

Open
wants to merge 28 commits into
base: master
Choose a base branch
from
Open

[CN-exec] Runtime loop invariants #884

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
ba4ceac
start loop plumbing
rbanerjee20 Nov 19, 2024
9020534
Add functions for separating variable declarations for loop purposes,…
rbanerjee20 Nov 19, 2024
aa64e07
Complete loop invariant plumbing + disable internal VIP allocations i…
rbanerjee20 Nov 20, 2024
6ddd7ba
Runtime loop invariants compiling and running
rbanerjee20 Nov 20, 2024
1df691e
Separate stack depth decr and postcondition leak check
rbanerjee20 Nov 20, 2024
a7cf6d3
runtime lib separation of decr and leak check
rbanerjee20 Nov 20, 2024
83b58fc
Add translation for computational arguments
rbanerjee20 Nov 20, 2024
01b29fd
End to end runtime loop invariants working for small example
rbanerjee20 Nov 20, 2024
4690478
Fix binding issue so runtime memcpy loop invariant working
rbanerjee20 Nov 20, 2024
d85b1fc
review changes
rbanerjee20 Nov 21, 2024
4844e5e
minor fixes
rbanerjee20 Nov 21, 2024
1f5587a
Propagate executable spec Ctype printing in GCC statement as expression
rbanerjee20 Nov 21, 2024
2a093fb
format
rbanerjee20 Nov 21, 2024
317df4d
experiments for not repeating bindings across loops
rbanerjee20 Nov 22, 2024
42ed2f6
Pre-deadline loop invariant changes
rbanerjee20 Dec 30, 2024
3ab2240
Revert "Pre-deadline loop invariant changes"
rbanerjee20 Jan 3, 2025
ce5f990
Revert "experiments for not repeating bindings across loops"
rbanerjee20 Jan 3, 2025
d9dc854
Begin second attempt of augmenting each with a binding+decl for
rbanerjee20 Jan 6, 2025
f52fa3f
Begin second attempt of augmenting each c_map_local(sym) with a bindi…
rbanerjee20 Jan 6, 2025
df4562f
some more progress
rbanerjee20 Jan 13, 2025
9e617e7
Finish task of creating + initialising addr_cn variables for all stac…
rbanerjee20 Feb 19, 2025
429a2c2
Enclose runtime loop invariant code in block
rbanerjee20 Feb 21, 2025
f4fb977
Add flag for disabling checking loop invariants at runtime
rbanerjee20 Feb 21, 2025
485c3e7
delete some commented code
rbanerjee20 Feb 21, 2025
abef895
Disable loop invariant translation in CN test gen
rbanerjee20 Feb 21, 2025
02c7f24
Add bool member to Mu.Label for keeping track of whether user has pro…
rbanerjee20 Feb 25, 2025
243795c
update TODO to mention Ethan instead of Zain
rbanerjee20 Feb 25, 2025
6df1e33
Refactor to make contains_user_spec flag part of the existing Loop in…
rbanerjee20 Feb 25, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 14 additions & 2 deletions backend/cn/bin/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -405,6 +405,7 @@ let generate_executable_specs
output_decorated
output_decorated_dir
without_ownership_checking
without_loop_invariants
with_test_gen
copy_source_dir
=
Expand Down Expand Up @@ -444,6 +445,7 @@ let generate_executable_specs
(try
Executable_spec.main
~without_ownership_checking
~without_loop_invariants
~with_test_gen
~copy_source_dir
filename
Expand Down Expand Up @@ -473,6 +475,7 @@ let run_seq_tests
magic_comment_char_dollar
(* Executable spec *)
without_ownership_checking
(* without_loop_invariants *)
(* Test Generation *)
output_dir
with_static_hack
Expand Down Expand Up @@ -524,7 +527,8 @@ let run_seq_tests
let _, sigma = ail_prog in
Cn_internal_to_ail.augment_record_map (BaseTypes.Record []);
Executable_spec.main
~without_ownership_checking
~without_ownership_checking (* TODO: Ethan *)
~without_loop_invariants:true
~with_test_gen:true
~copy_source_dir:false
filename
Expand Down Expand Up @@ -562,6 +566,7 @@ let run_tests
magic_comment_char_dollar
(* Executable spec *)
without_ownership_checking
(* without_loop_invariants *)
(* Test Generation *)
output_dir
only
Expand Down Expand Up @@ -662,7 +667,8 @@ let run_tests
Cn_internal_to_ail.augment_record_map (BaseTypes.Record []);
(try
Executable_spec.main
~without_ownership_checking
~without_ownership_checking (* TODO: Ethan *)
~without_loop_invariants:true
~with_test_gen:true
~copy_source_dir:false
filename
Expand Down Expand Up @@ -921,6 +927,11 @@ module Executable_spec_flags = struct
Arg.(value & flag & info [ "without-ownership-checking" ] ~doc)


let without_loop_invariants =
let doc = "Disable checking of loop invariants within CN runtime testing" in
Arg.(value & flag & info [ "without-loop-invariants" ] ~doc)


let with_test_gen =
let doc =
"Generate CN executable specifications in the correct format for feeding into \n\
Expand Down Expand Up @@ -1426,6 +1437,7 @@ let instrument_cmd =
$ Executable_spec_flags.output_decorated
$ Executable_spec_flags.output_decorated_dir
$ Executable_spec_flags.without_ownership_checking
$ Executable_spec_flags.without_loop_invariants
$ Executable_spec_flags.with_test_gen
$ Executable_spec_flags.copy_source_dir
in
Expand Down
Loading