From a9871bcd230eb104cc7ed56e2ebc373b5b54f32f Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 11 Aug 2025 15:00:35 +0100 Subject: [PATCH 01/38] Add focus_context for runtime --- .../libcn/include/cn-autoannot/focus_ctx.h | 20 +++++++ runtime/libcn/include/dune | 2 + runtime/libcn/lib/dune | 9 ++-- runtime/libcn/src/cn-autoannot/focus_ctx.c | 53 +++++++++++++++++++ runtime/libcn/test/CMakeLists.txt | 1 + runtime/libcn/test/autoannot/focus.cpp | 19 +++++++ runtime/libcn/test/build/dune | 3 +- 7 files changed, 103 insertions(+), 4 deletions(-) create mode 100644 runtime/libcn/include/cn-autoannot/focus_ctx.h create mode 100644 runtime/libcn/src/cn-autoannot/focus_ctx.c create mode 100644 runtime/libcn/test/autoannot/focus.cpp diff --git a/runtime/libcn/include/cn-autoannot/focus_ctx.h b/runtime/libcn/include/cn-autoannot/focus_ctx.h new file mode 100644 index 000000000..7967f6272 --- /dev/null +++ b/runtime/libcn/include/cn-autoannot/focus_ctx.h @@ -0,0 +1,20 @@ +#ifndef FOCUS_CTX_H +#define FOCUS_CTX_H + +#include + +#ifdef __cplusplus +extern "C" { +#endif + +void initialise_focus_context(void); +void push_focus_context(void); +void pop_focus_context(void); +void insert_focus(int64_t index); +int check_focus(int64_t index); + +#ifdef __cplusplus +} +#endif + +#endif // FOCUS_CTX_H diff --git a/runtime/libcn/include/dune b/runtime/libcn/include/dune index be1df369b..15795fc21 100644 --- a/runtime/libcn/include/dune +++ b/runtime/libcn/include/dune @@ -20,6 +20,8 @@ (cn-executable/rts_deps.h as runtime/include/cn-executable/rts_deps.h) (cn-executable/cerb_types.h as runtime/include/cn-executable/cerb_types.h) (cn-executable/stack.h as runtime/include/cn-executable/stack.h) + ; AutoAnnot + (cn-autoannot/focus_ctx.h as runtime/include/cn-autoannot/focus_ctx.h) ; Bennet (bennet/prelude.h as runtime/include/bennet/prelude.h) (bennet/dsl/arbitrary.h as runtime/include/bennet/dsl/arbitrary.h) diff --git a/runtime/libcn/lib/dune b/runtime/libcn/lib/dune index 0425b73e1..03d70aa43 100644 --- a/runtime/libcn/lib/dune +++ b/runtime/libcn/lib/dune @@ -25,9 +25,11 @@ (target libcn_exec.a) (deps (:headers - (glob_files ../include/cn-executable/*.h)) + (glob_files ../include/cn-executable/*.h) + (glob_files ../include/cn-autoannot/*.h)) (:src - (glob_files ../src/cn-executable/*.c))) + (glob_files ../src/cn-executable/*.c) + (file ../src/cn-autoannot/focus_ctx.c))) (action (progn (run mkdir -p cn-executable) @@ -42,7 +44,8 @@ cn-executable/bump_alloc.o cn-executable/hash_table.o cn-executable/rmap.o - cn-executable/utils.o)))) + cn-executable/utils.o + cn-executable/focus_ctx.o)))) (rule (target libbennet.a) diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c new file mode 100644 index 000000000..c40e71040 --- /dev/null +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -0,0 +1,53 @@ +#include +#include +#include // for SIGABRT +#include +#include +#include + +#include +#include + +// hashset +typedef hash_table focus_set; + +struct focus_context { + focus_set* indices; + struct focus_context *prev; +}; + +struct focus_context* cn_focus_global_context; // top of the stack + +void initialise_focus_context(void) { + cn_focus_global_context = fulm_default_alloc.malloc(sizeof(struct focus_context)); + cn_focus_global_context->indices = ht_create(&fulm_default_alloc); + cn_focus_global_context->prev = NULL; +} + +// should happen simultaneously with ghost_stack_depth_incr +void push_focus_context(void) { + struct focus_context* new_context = fulm_default_alloc.malloc(sizeof(struct focus_context)); + new_context->indices = ht_create(&fulm_default_alloc); + new_context->prev = cn_focus_global_context; + cn_focus_global_context = new_context; +} + +void pop_focus_context(void) { + // Free is automatic, no? + cn_focus_global_context = cn_focus_global_context->prev; +} + +void insert_focus(int64_t index) { + int64_t* key = fulm_malloc(sizeof(int64_t), &fulm_default_alloc); + *key = index; + ht_set(cn_focus_global_context->indices, key, (void*)1); // value is not used +} + +int check_focus(int64_t index) { + if (ht_get(cn_focus_global_context->indices, &index) != NULL) { + return 1; + } else { + return 0; + } +} + diff --git a/runtime/libcn/test/CMakeLists.txt b/runtime/libcn/test/CMakeLists.txt index 077098c33..968707167 100644 --- a/runtime/libcn/test/CMakeLists.txt +++ b/runtime/libcn/test/CMakeLists.txt @@ -35,6 +35,7 @@ add_executable(libcn_tests cn-smt/subst.cpp cn-smt/sexp.cpp cn-smt/solver.cpp + autoannot/focus.cpp ) # Disable narrowing warnings diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp new file mode 100644 index 000000000..860412049 --- /dev/null +++ b/runtime/libcn/test/autoannot/focus.cpp @@ -0,0 +1,19 @@ +#include +#include + +class LibAutoAnnot : public ::testing::Test { + protected: + void SetUp() override; +}; + +TEST(LibAutoAnnot, BasicOperations) { + initialise_focus_context(); + push_focus_context(); + insert_focus(100); + + ASSERT_EQ(check_focus(100), 1) << "Focus 100 should be found in current context."; + + pop_focus_context(); + + ASSERT_EQ(check_focus(100), 0) << "Focus 100 should NOT be found after pop."; +} diff --git a/runtime/libcn/test/build/dune b/runtime/libcn/test/build/dune index 5bb03cc82..00ad7d402 100644 --- a/runtime/libcn/test/build/dune +++ b/runtime/libcn/test/build/dune @@ -15,7 +15,8 @@ (file Makefile) (glob_files ../bennet/*.hpp) (glob_files ../bennet/*.cpp) - (glob_files ../cn-smt/*.cpp)) + (glob_files ../cn-smt/*.cpp) + (glob_files ../autoannot/*.cpp)) (action (run make))) From e1be3bdeb08fc60c95fcdc5b63a7a7feb6b09852 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Tue, 12 Aug 2025 14:50:41 +0100 Subject: [PATCH 02/38] Store iterated resources in the context --- .../libcn/include/cn-autoannot/focus_ctx.h | 36 ++++++- runtime/libcn/src/cn-autoannot/focus_ctx.c | 94 ++++++++++++++----- runtime/libcn/test/autoannot/focus.cpp | 18 +++- 3 files changed, 119 insertions(+), 29 deletions(-) diff --git a/runtime/libcn/include/cn-autoannot/focus_ctx.h b/runtime/libcn/include/cn-autoannot/focus_ctx.h index 7967f6272..8827dd234 100644 --- a/runtime/libcn/include/cn-autoannot/focus_ctx.h +++ b/runtime/libcn/include/cn-autoannot/focus_ctx.h @@ -7,11 +7,43 @@ extern "C" { #endif +typedef const char *type_sig; + +// Limitation: we only consider contiguous iter ress. +struct iter_res { + uint64_t ptr; + uint64_t size; + uint64_t nelems; + type_sig sig; +}; + +typedef struct iter_res_set { + struct iter_res res; + struct iter_res_set *next; +} iter_res_set; + +struct focus_info { + int64_t index; + type_sig sig; +}; + +typedef struct focus_set { + struct focus_info info; + struct focus_set *next; +} focus_set; + +struct focus_context { + focus_set *indices; + iter_res_set *iter_ress; + struct focus_context *prev; +}; + void initialise_focus_context(void); void push_focus_context(void); void pop_focus_context(void); -void insert_focus(int64_t index); -int check_focus(int64_t index); +void insert_focus(int64_t index, const char *type_sig); +void insert_iter_res(uint64_t ptr, uint64_t size, uint64_t nelems, type_sig sig); +int needs_focus(uint64_t address, uint64_t size, type_sig sig); #ifdef __cplusplus } diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index c40e71040..68ba2ae64 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -1,53 +1,101 @@ +#include + #include #include #include // for SIGABRT #include #include #include +#include +#include #include #include +#include -// hashset -typedef hash_table focus_set; - -struct focus_context { - focus_set* indices; - struct focus_context *prev; -}; +// Note(HK): +// we don't have to care about the difference between Owned/Block here +// because they are handled by the standard Fulminate machinery. +// i.e., if there is a discrepancy, it will be caught by Fulminate. struct focus_context* cn_focus_global_context; // top of the stack -void initialise_focus_context(void) { - cn_focus_global_context = fulm_default_alloc.malloc(sizeof(struct focus_context)); - cn_focus_global_context->indices = ht_create(&fulm_default_alloc); - cn_focus_global_context->prev = NULL; -} - // should happen simultaneously with ghost_stack_depth_incr void push_focus_context(void) { struct focus_context* new_context = fulm_default_alloc.malloc(sizeof(struct focus_context)); - new_context->indices = ht_create(&fulm_default_alloc); + new_context->indices = NULL; + new_context->iter_ress = NULL; new_context->prev = cn_focus_global_context; cn_focus_global_context = new_context; } +void initialise_focus_context(void) { + push_focus_context(); +} + void pop_focus_context(void) { // Free is automatic, no? cn_focus_global_context = cn_focus_global_context->prev; } -void insert_focus(int64_t index) { - int64_t* key = fulm_malloc(sizeof(int64_t), &fulm_default_alloc); - *key = index; - ht_set(cn_focus_global_context->indices, key, (void*)1); // value is not used +void insert_focus(int64_t index, type_sig sig) { + struct focus_set* new_set = fulm_malloc(sizeof(struct focus_set), &fulm_default_alloc); + new_set->info.index = index; + new_set->info.sig = sig; + new_set->next = cn_focus_global_context->indices; + cn_focus_global_context->indices = new_set; +} + +void insert_iter_res(uint64_t ptr, uint64_t size, uint64_t nelems, type_sig sig) { + struct iter_res_set* new = fulm_malloc(sizeof(iter_res_set), &fulm_default_alloc); + new->res.ptr = ptr; + new->res.size = size; + new->res.nelems = nelems; + new->res.sig = sig; + new->next = cn_focus_global_context->iter_ress; + cn_focus_global_context->iter_ress = new; } -int check_focus(int64_t index) { - if (ht_get(cn_focus_global_context->indices, &index) != NULL) { +/// Checks if the given address +/// (i) is in a iterated resource +/// (ii) is not focused +/// If (i) and (ii), it needs focus, and returns 1. +int needs_focus(uint64_t address, uint64_t size, type_sig sig) { + assert(cn_focus_global_context != NULL); + // (i) search for iterated resource + iter_res_set *iter = cn_focus_global_context->iter_ress; + while (iter) { + iter_res_set *cur = iter; + iter = iter->next; + uint64_t start = cur->res.ptr; + uint64_t end = start + cur->res.size * cur->res.nelems; + uint64_t offset = address - start; + if (address < start || address + size > end) { + continue; + } + if (offset % cur->res.size != 0) { + continue; + } + + uint64_t index = offset / cur->res.size; + + if (strcmp(cur->res.sig, sig) != 0) { + continue; + } + + // Case: an appropriate iterated resource is found + // (ii) search for focus + focus_set* cur_focus = cn_focus_global_context->indices; + while (cur_focus) { + if (cur_focus->info.index == index && + strcmp(cur_focus->info.sig, sig) == 0) { + return 0; + } + cur_focus = cur_focus->next; + } + // The index is not focused return 1; - } else { - return 0; } + // We didn't find any appropriate iterated resource + return 0; } - diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp index 860412049..2585ab23c 100644 --- a/runtime/libcn/test/autoannot/focus.cpp +++ b/runtime/libcn/test/autoannot/focus.cpp @@ -9,11 +9,21 @@ class LibAutoAnnot : public ::testing::Test { TEST(LibAutoAnnot, BasicOperations) { initialise_focus_context(); push_focus_context(); - insert_focus(100); - ASSERT_EQ(check_focus(100), 1) << "Focus 100 should be found in current context."; + /* + let p = 0xcafe000; + take X = each(u64 i; i < 4) { RW(p) }; + */ + insert_iter_res(0xcafe0000, 8, 4, "u64"); + /* focus RW, 1u64; */ + insert_focus(1, "u64"); - pop_focus_context(); + ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 1) << "Lack of focus for p[0]"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, "u64"), 0) << "Focus has already been annotated"; + ASSERT_EQ(needs_focus(0xcafe1000, 8, "u64"), 0) + << "No appropriate resource, so we don't need focus"; - ASSERT_EQ(check_focus(100), 0) << "Focus 100 should NOT be found after pop."; + pop_focus_context(); + ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 0) << "No need for focus"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, "u64"), 0) << "No need for focus"; } From 92db011fd0ff180ce40488237c7f9b579c9755ab Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Tue, 12 Aug 2025 15:13:44 +0100 Subject: [PATCH 03/38] Update test --- runtime/libcn/test/autoannot/focus.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp index 2585ab23c..3cf05378d 100644 --- a/runtime/libcn/test/autoannot/focus.cpp +++ b/runtime/libcn/test/autoannot/focus.cpp @@ -23,6 +23,22 @@ TEST(LibAutoAnnot, BasicOperations) { ASSERT_EQ(needs_focus(0xcafe1000, 8, "u64"), 0) << "No appropriate resource, so we don't need focus"; + push_focus_context(); + insert_iter_res(0xcafe0000, 8, 4, "u64"); + insert_iter_res(0x10000000, 8, 4, "u64"); + ASSERT_EQ(needs_focus(0xcafe0008, 8, "u64"), 1) << "No focus in the current level"; + ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 1) << "No focus in the current level"; + + insert_focus(0, "u64"); + ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x10000000, 8, "u64"), 0) << "Just focused"; + + pop_focus_context(); + + // Check if it remembers the context + ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 1) << "Lack of focus for p[0]"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, "u64"), 0) << "Focus has already been annotated"; + pop_focus_context(); ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 0) << "No need for focus"; ASSERT_EQ(needs_focus(0xcafe0008, 8, "u64"), 0) << "No need for focus"; From 356bd6e76f42f4ba8a39303d6f7838eb08ad1a9b Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Tue, 12 Aug 2025 16:43:53 +0100 Subject: [PATCH 04/38] Fix the signature for needs_focus --- .../libcn/include/cn-autoannot/focus_ctx.h | 4 +-- runtime/libcn/src/cn-autoannot/focus_ctx.c | 8 ++---- runtime/libcn/test/autoannot/focus.cpp | 26 +++++++++++-------- 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/runtime/libcn/include/cn-autoannot/focus_ctx.h b/runtime/libcn/include/cn-autoannot/focus_ctx.h index 8827dd234..516260139 100644 --- a/runtime/libcn/include/cn-autoannot/focus_ctx.h +++ b/runtime/libcn/include/cn-autoannot/focus_ctx.h @@ -41,9 +41,9 @@ struct focus_context { void initialise_focus_context(void); void push_focus_context(void); void pop_focus_context(void); -void insert_focus(int64_t index, const char *type_sig); +void insert_focus(int64_t index, type_sig sig); void insert_iter_res(uint64_t ptr, uint64_t size, uint64_t nelems, type_sig sig); -int needs_focus(uint64_t address, uint64_t size, type_sig sig); +int needs_focus(uint64_t address, uint64_t size); #ifdef __cplusplus } diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index 68ba2ae64..e72aae498 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -60,7 +60,7 @@ void insert_iter_res(uint64_t ptr, uint64_t size, uint64_t nelems, type_sig sig) /// (i) is in a iterated resource /// (ii) is not focused /// If (i) and (ii), it needs focus, and returns 1. -int needs_focus(uint64_t address, uint64_t size, type_sig sig) { +int needs_focus(uint64_t address, uint64_t size) { assert(cn_focus_global_context != NULL); // (i) search for iterated resource iter_res_set *iter = cn_focus_global_context->iter_ress; @@ -79,16 +79,12 @@ int needs_focus(uint64_t address, uint64_t size, type_sig sig) { uint64_t index = offset / cur->res.size; - if (strcmp(cur->res.sig, sig) != 0) { - continue; - } - // Case: an appropriate iterated resource is found // (ii) search for focus focus_set* cur_focus = cn_focus_global_context->indices; while (cur_focus) { if (cur_focus->info.index == index && - strcmp(cur_focus->info.sig, sig) == 0) { + strcmp(cur_focus->info.sig, cur->res.sig) == 0) { return 0; } cur_focus = cur_focus->next; diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp index 3cf05378d..9bf4669af 100644 --- a/runtime/libcn/test/autoannot/focus.cpp +++ b/runtime/libcn/test/autoannot/focus.cpp @@ -18,28 +18,32 @@ TEST(LibAutoAnnot, BasicOperations) { /* focus RW, 1u64; */ insert_focus(1, "u64"); - ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 1) << "Lack of focus for p[0]"; - ASSERT_EQ(needs_focus(0xcafe0008, 8, "u64"), 0) << "Focus has already been annotated"; - ASSERT_EQ(needs_focus(0xcafe1000, 8, "u64"), 0) + ASSERT_EQ(needs_focus(0xcafe0000, 8), 1) << "Lack of focus for p[0]"; + ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Focus has already been annotated"; + ASSERT_EQ(needs_focus(0xcafe1000, 8), 0) << "No appropriate resource, so we don't need focus"; push_focus_context(); insert_iter_res(0xcafe0000, 8, 4, "u64"); insert_iter_res(0x10000000, 8, 4, "u64"); - ASSERT_EQ(needs_focus(0xcafe0008, 8, "u64"), 1) << "No focus in the current level"; - ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 1) << "No focus in the current level"; + insert_iter_res(0x20000000, 4, 4, "u32"); + ASSERT_EQ(needs_focus(0xcafe0008, 8), 1) << "No focus in the current level"; + ASSERT_EQ(needs_focus(0xcafe0000, 8), 1) << "No focus in the current level"; insert_focus(0, "u64"); - ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 0) << "Just focused"; - ASSERT_EQ(needs_focus(0x10000000, 8, "u64"), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0xcafe0000, 8), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x10000000, 8), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x20000000, 4), 1) << "Type mismatch"; + insert_focus(0, "u32"); + ASSERT_EQ(needs_focus(0x20000000, 4), 0) << "Just focused"; pop_focus_context(); // Check if it remembers the context - ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 1) << "Lack of focus for p[0]"; - ASSERT_EQ(needs_focus(0xcafe0008, 8, "u64"), 0) << "Focus has already been annotated"; + ASSERT_EQ(needs_focus(0xcafe0000, 8), 1) << "Lack of focus for p[0]"; + ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Focus has already been annotated"; pop_focus_context(); - ASSERT_EQ(needs_focus(0xcafe0000, 8, "u64"), 0) << "No need for focus"; - ASSERT_EQ(needs_focus(0xcafe0008, 8, "u64"), 0) << "No need for focus"; + ASSERT_EQ(needs_focus(0xcafe0000, 8), 0) << "No need for focus"; + ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "No need for focus"; } From 28a933d97e1df57c900485aebbd3a3ef3179aa76 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Tue, 12 Aug 2025 18:35:14 +0100 Subject: [PATCH 05/38] insert_focus... maybe? --- lib/fulminate/cn_to_ail.ml | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/lib/fulminate/cn_to_ail.ml b/lib/fulminate/cn_to_ail.ml index db970351b..08c5e29e6 100644 --- a/lib/fulminate/cn_to_ail.ml +++ b/lib/fulminate/cn_to_ail.ml @@ -3769,7 +3769,24 @@ let cn_to_ail_cnstatement | Have _lc -> failwith "TODO Have" | Instantiate (_to_instantiate, _it) -> (default_res_for_dest, true) | Split_case _ -> (default_res_for_dest, true) - | Extract (_, _, _it) -> (default_res_for_dest, true) + | Extract (_, to_extract, it) -> + let b, ss, e = cn_to_ail_expr filename dts globals spec_mode_opt it PassBack in + (match to_extract with + | E_Pred (CN_owned (Some ct)) | E_Pred (CN_block (Some ct)) -> + let s = Pp.plain (Sctypes.pp ct) in + Pp.(debug 10 (lazy (string s))); + let s_expr = mk_expr (A.AilEstr (None, [ (Cerb_location.unknown, [ s ]) ])) in + let call_expr = + A.AilEcall (mk_expr (A.AilEident (Sym.fresh "insert_focus")), [ e; s_expr ]) + in + let call_stat = A.AilSexpr (mk_expr call_expr) in + (prefix d (b, ss @ [ call_stat ]) (empty_for_dest d), false) + | E_Everything + | E_Pred (CN_owned None) + | E_Pred (CN_block None) + | E_Pred (CN_named _) -> + (* Not supported, or deprecated *) + (default_res_for_dest, true)) | Unfold (_fsym, _args) -> (default_res_for_dest, true) (* fsym is a function symbol *) | Apply (fsym, args) -> if without_lemma_checks then From 1b807f309127b515916dbdd73bb920f021f21709 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Wed, 13 Aug 2025 17:58:33 +0100 Subject: [PATCH 06/38] Update the API for focusing --- .../libcn/include/cn-autoannot/focus_ctx.h | 11 +++++--- runtime/libcn/src/cn-autoannot/focus_ctx.c | 11 ++++---- runtime/libcn/test/autoannot/focus.cpp | 25 ++++++++++--------- 3 files changed, 27 insertions(+), 20 deletions(-) diff --git a/runtime/libcn/include/cn-autoannot/focus_ctx.h b/runtime/libcn/include/cn-autoannot/focus_ctx.h index 516260139..03e798a46 100644 --- a/runtime/libcn/include/cn-autoannot/focus_ctx.h +++ b/runtime/libcn/include/cn-autoannot/focus_ctx.h @@ -12,8 +12,12 @@ typedef const char *type_sig; // Limitation: we only consider contiguous iter ress. struct iter_res { uint64_t ptr; + // contiguous indices (closed interval) + uint64_t start; + uint64_t end; + // step uint64_t size; - uint64_t nelems; + // type signature type_sig sig; }; @@ -42,8 +46,9 @@ void initialise_focus_context(void); void push_focus_context(void); void pop_focus_context(void); void insert_focus(int64_t index, type_sig sig); -void insert_iter_res(uint64_t ptr, uint64_t size, uint64_t nelems, type_sig sig); -int needs_focus(uint64_t address, uint64_t size); +void insert_iter_res( + uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig); + int needs_focus(uint64_t address, uint64_t size); #ifdef __cplusplus } diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index e72aae498..3535d4d08 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -46,11 +46,12 @@ void insert_focus(int64_t index, type_sig sig) { cn_focus_global_context->indices = new_set; } -void insert_iter_res(uint64_t ptr, uint64_t size, uint64_t nelems, type_sig sig) { +void insert_iter_res(uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig) { struct iter_res_set* new = fulm_malloc(sizeof(iter_res_set), &fulm_default_alloc); new->res.ptr = ptr; new->res.size = size; - new->res.nelems = nelems; + new->res.start = start; + new->res.end = end; new->res.sig = sig; new->next = cn_focus_global_context->iter_ress; cn_focus_global_context->iter_ress = new; @@ -67,9 +68,9 @@ int needs_focus(uint64_t address, uint64_t size) { while (iter) { iter_res_set *cur = iter; iter = iter->next; - uint64_t start = cur->res.ptr; - uint64_t end = start + cur->res.size * cur->res.nelems; - uint64_t offset = address - start; + uint64_t start = cur->res.ptr + cur->res.start * cur->res.size; + uint64_t end = cur->res.ptr + (cur->res.end + 1) * cur->res.size; + uint64_t offset = address - cur->res.ptr; if (address < start || address + size > end) { continue; } diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp index 9bf4669af..21a94d708 100644 --- a/runtime/libcn/test/autoannot/focus.cpp +++ b/runtime/libcn/test/autoannot/focus.cpp @@ -14,28 +14,29 @@ TEST(LibAutoAnnot, BasicOperations) { let p = 0xcafe000; take X = each(u64 i; i < 4) { RW(p) }; */ - insert_iter_res(0xcafe0000, 8, 4, "u64"); + insert_iter_res(0xcafe0000, 0, 4, 8, "unsigned long"); /* focus RW, 1u64; */ - insert_focus(1, "u64"); + insert_focus(1, "unsigned long"); ASSERT_EQ(needs_focus(0xcafe0000, 8), 1) << "Lack of focus for p[0]"; - ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Focus has already been annotated"; + ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Focused"; ASSERT_EQ(needs_focus(0xcafe1000, 8), 0) << "No appropriate resource, so we don't need focus"; push_focus_context(); - insert_iter_res(0xcafe0000, 8, 4, "u64"); - insert_iter_res(0x10000000, 8, 4, "u64"); - insert_iter_res(0x20000000, 4, 4, "u32"); + insert_iter_res(0xcafe0000, 0, 4, 8, "unsigned long"); + insert_iter_res(0x10000000, 1, 4, 8, "unsigned long"); + insert_iter_res(0x20000000, 0, 4, 4, "unsigned int"); ASSERT_EQ(needs_focus(0xcafe0008, 8), 1) << "No focus in the current level"; ASSERT_EQ(needs_focus(0xcafe0000, 8), 1) << "No focus in the current level"; - insert_focus(0, "u64"); - ASSERT_EQ(needs_focus(0xcafe0000, 8), 0) << "Just focused"; - ASSERT_EQ(needs_focus(0x10000000, 8), 0) << "Just focused"; - ASSERT_EQ(needs_focus(0x20000000, 4), 1) << "Type mismatch"; - insert_focus(0, "u32"); - ASSERT_EQ(needs_focus(0x20000000, 4), 0) << "Just focused"; + insert_focus(1, "unsigned long"); + ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x10000008, 8), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x20000004, 4), 1) << "Type mismatch"; + ASSERT_EQ(needs_focus(0x10000000, 8), 0) << "Out of the iter_res"; + insert_focus(1, "unsigned int"); + ASSERT_EQ(needs_focus(0x20000004, 4), 0) << "Just focused"; pop_focus_context(); From 4bfe10bd191953110b481a986464f7ac5bff8e9e Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Wed, 13 Aug 2025 18:24:04 +0100 Subject: [PATCH 07/38] Handle iterated resources --- lib/fulminate/cn_to_ail.ml | 88 +++++++++++++------ lib/fulminate/fulminate.ml | 1 + lib/fulminate/ownership.ml | 6 +- .../libcn/include/cn-autoannot/focus_ctx.h | 7 ++ 4 files changed, 75 insertions(+), 27 deletions(-) diff --git a/lib/fulminate/cn_to_ail.ml b/lib/fulminate/cn_to_ail.ml index 08c5e29e6..c84463a21 100644 --- a/lib/fulminate/cn_to_ail.ml +++ b/lib/fulminate/cn_to_ail.ml @@ -2878,11 +2878,8 @@ let cn_to_ail_struct ((sym, (loc, attrs, tag_def)) : A.sigma_tag_definition) | C.UnionDef _ -> [] -let get_while_bounds_and_cond (i_sym, i_bt) it = - (* Translation of q.pointer *) - let i_it = IT.IT (IT.(Sym i_sym), i_bt, Cerb_location.unknown) in - (* Start of range *) - let start_expr = +let get_range_from_it (i_sym, i_bt) it = + let lb = if BT.equal_sign (fst (Option.get (BT.is_bits_bt i_bt))) BT.Unsigned then IndexTerms.Bounds.get_lower_bound (i_sym, i_bt) it else ( @@ -2900,21 +2897,7 @@ let get_while_bounds_and_cond (i_sym, i_bt) it = (); exit 2) in - let start_expr = - IT.IT - ( IT.Cast (IT.get_bt start_expr, start_expr), - IT.get_bt start_expr, - Cerb_location.unknown ) - in - let start_cond = - match start_expr with - | IT (Binop (Add, start_expr', IT (Const (Bits (_, n)), _, _)), _, _) - when Z.equal n Z.one -> - IT.lt_ (start_expr', i_it) Cerb_location.unknown - | _ -> IT.le_ (start_expr, i_it) Cerb_location.unknown - in - (* End of range *) - let end_expr = + let ub = match IndexTerms.Bounds.get_upper_bound_opt (i_sym, i_bt) it with | Some e -> e | None -> @@ -2929,6 +2912,28 @@ let get_while_bounds_and_cond (i_sym, i_bt) it = (); exit 2 in + (lb, ub) + + +let get_while_bounds_and_cond (i_sym, i_bt) it = + (* Translation of q.pointer *) + let i_it = IT.IT (IT.(Sym i_sym), i_bt, Cerb_location.unknown) in + (* Start of range *) + let start_expr, end_expr = get_range_from_it (i_sym, i_bt) it in + let start_expr = + IT.IT + ( IT.Cast (IT.get_bt start_expr, start_expr), + IT.get_bt start_expr, + Cerb_location.unknown ) + in + let start_cond = + match start_expr with + | IT (Binop (Add, start_expr', IT (Const (Bits (_, n)), _, _)), _, _) + when Z.equal n Z.one -> + IT.lt_ (start_expr', i_it) Cerb_location.unknown + | _ -> IT.le_ (start_expr, i_it) Cerb_location.unknown + in + (* End of range *) let end_cond = match end_expr with | IT (Binop (Sub, end_expr', IT (Const (Bits (_, n)), _, _)), _, _) @@ -3079,10 +3084,37 @@ let cn_to_ail_resource } *) let i_sym, i_bt = q.q in - let start_expr, _, while_loop_cond = get_while_bounds_and_cond q.q q.permission in + let start_expr, end_expr, while_loop_cond = + get_while_bounds_and_cond q.q q.permission + in let _, _, e_start = cn_to_ail_expr filename dts globals spec_mode_opt start_expr PassBack in + let _, _, e_end = + cn_to_ail_expr filename dts globals spec_mode_opt end_expr PassBack + in + let pname = Sym.fresh "CN_INSERT_ITER_RES" in + let e_step = mk_expr A.(AilEsizeof (C.no_qualifiers, Sctypes.to_ctype q.step)) in + let _, _, e_pointer = + cn_to_ail_expr filename dts globals spec_mode_opt q.pointer PassBack + in + let itere_res_call_stmt_opt = + match q.name with + | Owned (sct, _) -> + let type_str = Pp.plain (Sctypes.pp sct) in + let ail_type_str = A.AilEstr (None, [ (Cerb_location.unknown, [ type_str ]) ]) in + let iter_res_call = + mk_expr + A.( + AilEcall + ( mk_expr (AilEident pname), + [ e_pointer; e_start; e_end; e_step; mk_expr ail_type_str ] )) + in + let iter_res_call_stmt = A.(AilSexpr iter_res_call) in + Some iter_res_call_stmt + | _ -> None + in + (* Generate while loop condition *) let _, _, while_cond_expr = cn_to_ail_expr filename dts globals spec_mode_opt while_loop_cond PassBack in @@ -3196,9 +3228,11 @@ let cn_to_ail_resource mk_stmt (AilSblock ([], List.map mk_stmt [ if_stat; increment_stat ])), 0 )) in - let ail_block = - A.(AilSblock ([ start_binding ], List.map mk_stmt [ start_assign; while_loop ])) + let stmts = [ start_assign; while_loop ] in + let stmts = + match itere_res_call_stmt_opt with Some stmt -> stmt :: stmts | None -> stmts in + let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in ([], [ ail_block ]) | _ -> (* TODO: Change to mostly use index terms rather than Ail directly - avoids duplication between these functions and cn_to_ail *) @@ -3252,9 +3286,11 @@ let cn_to_ail_resource mk_stmt A.(AilSblock ([], List.map mk_stmt [ if_stat; increment_stat ])), 0 )) in - let ail_block = - A.(AilSblock ([ start_binding ], List.map mk_stmt [ start_assign; while_loop ])) + let stmts = [ start_assign; while_loop ] in + let stmts = + match itere_res_call_stmt_opt with Some stmt -> stmt :: stmts | None -> stmts in + let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in ([ sym_binding ], [ sym_decl; ail_block ]) in (b1 @ b2 @ b3 @ bs' @ bs, s1 @ s2 @ s3 @ ss @ ss') @@ -3777,7 +3813,7 @@ let cn_to_ail_cnstatement Pp.(debug 10 (lazy (string s))); let s_expr = mk_expr (A.AilEstr (None, [ (Cerb_location.unknown, [ s ]) ])) in let call_expr = - A.AilEcall (mk_expr (A.AilEident (Sym.fresh "insert_focus")), [ e; s_expr ]) + A.AilEcall (mk_expr (A.AilEident (Sym.fresh "CN_INSERT_FOCUS")), [ e; s_expr ]) in let call_stat = A.AilSexpr (mk_expr call_expr) in (prefix d (b, ss @ [ call_stat ]) (empty_for_dest d), false) diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index bfe3208c1..c409caf29 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -765,6 +765,7 @@ let main (* Save things *) let oc = Stdlib.open_out out_filename in output_to_oc oc [ "#define __CN_INSTRUMENT\n"; "#include \n" ]; + output_to_oc oc [ "#include \n" ]; output_to_oc oc cn_header_decls_list; output_to_oc oc diff --git a/lib/fulminate/ownership.ml b/lib/fulminate/ownership.ml index a9afce2fc..72fe58f27 100644 --- a/lib/fulminate/ownership.ml +++ b/lib/fulminate/ownership.ml @@ -86,12 +86,16 @@ let get_ownership_global_init_stats (ConstantInteger (IConstant (Z.of_int ghost_array_size, Decimal, None)))) ] )) in + let cn_initialise_focus_context_fcall = + mk_expr A.(AilEcall (mk_expr (AilEident (Sym.fresh "initialise_focus_context")), [])) + in List.map (fun e -> A.(AilSexpr e)) (bump_config_calls @ [ cn_ghost_state_init_fcall; cn_ghost_stack_depth_init_fcall; - cn_ghost_arg_array_alloc_fcall + cn_ghost_arg_array_alloc_fcall; + cn_initialise_focus_context_fcall ]) diff --git a/runtime/libcn/include/cn-autoannot/focus_ctx.h b/runtime/libcn/include/cn-autoannot/focus_ctx.h index 03e798a46..063d12c75 100644 --- a/runtime/libcn/include/cn-autoannot/focus_ctx.h +++ b/runtime/libcn/include/cn-autoannot/focus_ctx.h @@ -9,6 +9,13 @@ extern "C" { typedef const char *type_sig; +// Wrapper for cn values +#define CN_INSERT_ITER_RES(base, start, end, size, sig) \ + insert_iter_res((uint64_t)base->ptr, start->val, end->val, size, sig) + +#define CN_INSERT_FOCUS(index, sig) insert_focus(index->val, sig) + + // Limitation: we only consider contiguous iter ress. struct iter_res { uint64_t ptr; From b805302f08eaf32b9798cea2957b5d83c85231f3 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Wed, 13 Aug 2025 18:52:16 +0100 Subject: [PATCH 08/38] Add needs_focus for each LOAD/STORE --- lib/fulminate/cn_to_ail.ml | 8 ++++++-- lib/fulminate/fulminate.ml | 10 +++++----- runtime/libcn/include/cn-executable/utils.h | 18 ++++++++++++++++++ 3 files changed, 29 insertions(+), 7 deletions(-) diff --git a/lib/fulminate/cn_to_ail.ml b/lib/fulminate/cn_to_ail.ml index c84463a21..1e816c9a0 100644 --- a/lib/fulminate/cn_to_ail.ml +++ b/lib/fulminate/cn_to_ail.ml @@ -3230,7 +3230,9 @@ let cn_to_ail_resource in let stmts = [ start_assign; while_loop ] in let stmts = - match itere_res_call_stmt_opt with Some stmt -> stmt :: stmts | None -> stmts + match (itere_res_call_stmt_opt, spec_mode_opt) with + | Some stmt, Some Pre -> stmt :: stmts + | _ -> stmts in let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in ([], [ ail_block ]) @@ -3288,7 +3290,9 @@ let cn_to_ail_resource in let stmts = [ start_assign; while_loop ] in let stmts = - match itere_res_call_stmt_opt with Some stmt -> stmt :: stmts | None -> stmts + match (itere_res_call_stmt_opt, spec_mode_opt) with + | Some stmt, Some Pre -> stmt :: stmts + | _ -> stmts in let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in ([ sym_binding ], [ sym_decl; ail_block ]) diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index c409caf29..ad36367c4 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -188,7 +188,7 @@ let memory_accesses_injections ail_prog = match access with | Load { loc; _ } -> let b, e = pos_bbox loc in - acc := (point b, [ "CN_LOAD(" ]) :: (point e, [ ")" ]) :: !acc + acc := (point b, [ "CN_LOAD_ANNOT(" ]) :: (point e, [ ")" ]) :: !acc | Store { lvalue; expr; _ } -> (* NOTE: we are not using the location of the access (the AilEassign), because if in the source the assignment was surrounded by parens its location will contain @@ -196,7 +196,7 @@ let memory_accesses_injections ail_prog = let b, pos1 = pos_bbox (loc_of_expr lvalue) in let pos2, e = pos_bbox (loc_of_expr expr) in acc - := (point b, [ "CN_STORE(" ]) + := (point b, [ "CN_STORE_ANNOT(" ]) :: (region (pos1, pos2) NoCursor, [ ", " ]) :: (point e, [ ")" ]) :: !acc @@ -212,7 +212,7 @@ let memory_accesses_injections ail_prog = acc := (region (sstart, b) NoCursor, [ "" ]) :: ( point b, - [ "CN_STORE_OP(" + [ "CN_STORE_OP_ANNOT(" ^ pp_expr lvalue ^ "," ^ string_of_aop aop @@ -226,7 +226,7 @@ let memory_accesses_injections ail_prog = let b, pos1 = pos_bbox (loc_of_expr lvalue) in let pos2, e = pos_bbox (loc_of_expr expr) in acc - := (point b, [ "CN_STORE_OP(" ]) + := (point b, [ "CN_STORE_OP_ANNOT(" ]) :: (region (pos1, pos2) NoCursor, [ "," ^ string_of_aop aop ^ "," ]) :: (point e, [ ")" ]) :: !acc) @@ -765,7 +765,7 @@ let main (* Save things *) let oc = Stdlib.open_out out_filename in output_to_oc oc [ "#define __CN_INSTRUMENT\n"; "#include \n" ]; - output_to_oc oc [ "#include \n" ]; + output_to_oc oc [ "#include \n"; "#include \n" ]; output_to_oc oc cn_header_decls_list; output_to_oc oc diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index 39ae8e662..549c2ad3f 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -628,6 +628,13 @@ static inline void cn_postfix(void* ptr, size_t size) { *__tmp; \ }) +#define CN_LOAD_ANNOT(LV) \ + ({ \ + typeof(LV) *__tmp = &(LV); \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) cn_printf(CN_LOGGING_ERROR, "needs focus\n"); \ + CN_LOAD(LV); \ + }) + #define CN_STORE_OP(LV, op, X) \ ({ \ typeof(LV)* __tmp; \ @@ -640,6 +647,17 @@ static inline void cn_postfix(void* ptr, size_t size) { #define CN_STORE(LV, X) CN_STORE_OP(LV, , X) +#define CN_STORE_OP_ANNOT(LV, op, X) \ + ({ \ + typeof(LV) *__tmp; \ + __tmp = &(LV); \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) \ + cn_printf(CN_LOGGING_ERROR, "needs focus\n"); \ + CN_STORE_OP(LV, op, X); \ + }) + +#define CN_STORE_ANNOT(LV, X) CN_STORE_OP_ANNOT(LV, , X) + #define CN_POSTFIX(LV, OP) \ ({ \ typeof(LV)* __tmp; \ From 1fa8602a721967d8499feddc3db5cf8e09c6d963 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 14 Aug 2025 17:34:54 +0100 Subject: [PATCH 09/38] Print variables when focus is missing --- lib/fulminate/fulminate.ml | 97 ++++++++++++++++++++- runtime/libcn/include/cn-executable/utils.h | 11 +-- 2 files changed, 99 insertions(+), 9 deletions(-) diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index ad36367c4..c517136e8 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -135,7 +135,28 @@ let collect_memory_accesses (_, sigm) = match stmt.node with | AilSskip | AilSbreak | AilScontinue | AilSreturnVoid | AilSgoto _ -> () | AilSexpr e | AilSreturn e | AilSreg_store (_, e) -> aux_expr e env - | AilSblock (bs, ss) -> scan_for_decls_and_update_env (bs, ss) env aux_expr aux_stmt + | AilSblock (bs, ss) -> + let lookup_ty sym = + let _, (_, _, _, ty) = List.find (fun (sym', _) -> Sym.equal sym sym') bs in + (sym, ty) + in + let env_cell = ref env in + List.iter + (fun s -> + match s.node with + (* Update the environment when variables are declared *) + | AilSdeclaration xs -> + List.iter + (function + | sym, None -> + env_cell := lookup_ty sym :: !env_cell; + () + | sym, Some e -> + env_cell := lookup_ty sym :: !env_cell; + aux_expr e !env_cell) + xs + | _ -> aux_stmt s !env_cell) + ss | AilSpar ss -> List.iter (fun s -> aux_stmt s env) ss | AilSif (e, s1, s2) -> aux_expr e env; @@ -154,10 +175,72 @@ let collect_memory_accesses (_, sigm) = (* AilSdeclaration must be handled in `AilSblock` *) failwith "unreachable" in - List.iter (fun (_, (_, _, _, _, stmt)) -> aux_stmt stmt []) sigm.function_definitions; + sigm.function_definitions + |> List.iter (fun (f, body) -> + match List.assoc Sym.equal f sigm.declarations with + | _, _, Decl_function (_, _, types, _, _, _) -> + let _, _, _, args, stmt = body in + let env = List.map2 (fun arg (_, ct, _) -> (arg, ct)) args types in + aux_stmt stmt env + | _ -> failwith "ill-formed program"); !acc +let gen_fmt_for_integer_type = + let open CF.Ctype in + (* Ignore IntN_t and its friends *) + let usable = function Ichar | Short | Int_ | Long | LongLong -> true | _ -> false in + function + | Char -> Some "%c" + | Bool -> Some "%d" + | Signed i when usable i -> + (match (CF.Ocaml_implementation.get ()).sizeof_ity (Signed i) with + | Some 1 -> Some "%c" + | Some 2 -> Some "%hd" + | Some 4 -> Some "%d" + | Some 8 -> Some "%lld" + | _ -> failwith "unimplemented") + | Unsigned u when usable u -> + (match (CF.Ocaml_implementation.get ()).sizeof_ity (Unsigned u) with + | Some 1 -> Some "%c" + | Some 2 -> Some "%hu" + | Some 4 -> Some "%u" + | Some 8 -> Some "%llu" + | _ -> failwith "unimplemented") + | _ -> None + + +let get_symbol = function + | CF.Symbol.Symbol (_, _, CF.Symbol.SD_Id s) + | CF.Symbol.Symbol (_, _, CF.Symbol.SD_ObjectAddress s) -> + Some s + | CF.Symbol.Symbol (_, _, CF.Symbol.SD_FunArg _) -> failwith "funarg" + | CF.Symbol.Symbol (_, _, CF.Symbol.SD_FunArgValue _) -> failwith "var" + | CF.Symbol.Symbol (_, _, CF.Symbol.SD_CN_Id _) -> failwith "cn id" + | _ -> None + + +let rec gen_env_fmt_printer = function + | [] -> ("", []) + | (sym, ty) :: xs -> + let fmt, args = gen_env_fmt_printer xs in + let open CF.Ctype in + Pp.(debug 10 (lazy (item "gen_env_fmt" (string (CF.Symbol.show_symbol sym))))); + let (Ctype (_, ty)) = ty in + (match ty with + | Basic (Integer b) -> + (match (gen_fmt_for_integer_type b, get_symbol sym) with + | Some f, Some sym -> + let f = Printf.sprintf "%s=%s, " sym f in + (f ^ fmt, sym :: args) + | _ -> (fmt, args)) + | Struct _ -> failwith "unimplemented" + | Basic (Floating _) + | Array _ | Function _ | Void | FunctionNoParams _ | Pointer _ | Atomic _ | Union _ + | Byte -> + (fmt, args)) + + let memory_accesses_injections ail_prog = let open Cerb_frontend in let open Cerb_location in @@ -184,11 +267,17 @@ let memory_accesses_injections ail_prog = let xs = collect_memory_accesses ail_prog in List.iter (* HK: Currently, `env` is ignored. It will be used in future patches. *) - (fun (access, _env) -> + (fun (access, env) -> match access with | Load { loc; _ } -> let b, e = pos_bbox loc in - acc := (point b, [ "CN_LOAD_ANNOT(" ]) :: (point e, [ ")" ]) :: !acc + let fmt, args = gen_env_fmt_printer env in + let fmt = "[auto annot (focus)]: " ^ fmt ^ "\\n" in + let args = List.fold_left (fun acc arg -> acc ^ ", " ^ arg) "" args in + acc + := (point b, [ "CN_LOAD_ANNOT(" ]) + :: (point e, [ ", \"" ^ fmt ^ "\"" ^ args ^ ")" ]) + :: !acc | Store { lvalue; expr; _ } -> (* NOTE: we are not using the location of the access (the AilEassign), because if in the source the assignment was surrounded by parens its location will contain diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index 549c2ad3f..28a139511 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -628,11 +628,12 @@ static inline void cn_postfix(void* ptr, size_t size) { *__tmp; \ }) -#define CN_LOAD_ANNOT(LV) \ - ({ \ - typeof(LV) *__tmp = &(LV); \ - if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) cn_printf(CN_LOGGING_ERROR, "needs focus\n"); \ - CN_LOAD(LV); \ +#define CN_LOAD_ANNOT(LV, FMT, ...) \ + ({ \ + typeof(LV) *__tmp = &(LV); \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) \ + cn_printf(CN_LOGGING_ERROR, FMT, ##__VA_ARGS__); \ + CN_LOAD(LV); \ }) #define CN_STORE_OP(LV, op, X) \ From f24ebdc5bde8a55bcabea75602b848c30ee6fbad Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 14 Aug 2025 18:07:35 +0100 Subject: [PATCH 10/38] Do free when pop --- runtime/libcn/src/cn-autoannot/focus_ctx.c | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index 3535d4d08..4b183e827 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -34,8 +34,22 @@ void initialise_focus_context(void) { } void pop_focus_context(void) { - // Free is automatic, no? + struct focus_context *old_context = cn_focus_global_context; cn_focus_global_context = cn_focus_global_context->prev; + // free + focus_set *cur_focus = old_context->indices; + while (cur_focus) { + focus_set *next = cur_focus->next; + fulm_free(cur_focus, &fulm_default_alloc); + cur_focus = next; + } + + iter_res_set *cur_iter_res = old_context->iter_ress; + while (cur_iter_res) { + iter_res_set *next = cur_iter_res->next; + fulm_free(cur_iter_res, &fulm_default_alloc); + cur_iter_res = next; + } } void insert_focus(int64_t index, type_sig sig) { From 8ce2d7ee143b60ec6bedcdd10bcb689f48f7a08c Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 14 Aug 2025 18:22:22 +0100 Subject: [PATCH 11/38] Store & push pop context --- lib/fulminate/cn_to_ail.ml | 13 +++++++++++-- lib/fulminate/fulminate.ml | 14 ++++++-------- runtime/libcn/include/cn-executable/utils.h | 6 +++--- 3 files changed, 20 insertions(+), 13 deletions(-) diff --git a/lib/fulminate/cn_to_ail.ml b/lib/fulminate/cn_to_ail.ml index 1e816c9a0..aa6c8dad7 100644 --- a/lib/fulminate/cn_to_ail.ml +++ b/lib/fulminate/cn_to_ail.ml @@ -4523,7 +4523,11 @@ let rec cn_to_ail_lat_2 List.map (fun fn_sym -> mk_stmt (A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident fn_sym), []))))) - OE.[ cn_stack_depth_decr_sym; cn_postcondition_leak_check_sym ] + OE. + [ cn_stack_depth_decr_sym; + cn_postcondition_leak_check_sym; + Sym.fresh "pop_focus_context" + ] in let block = A.( @@ -4736,7 +4740,12 @@ let cn_to_ail_pre_post A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_stack_depth_incr_sym), []))) in - [ cn_stack_depth_incr_stat_ ]) + let push_focus_context = + A.AilSexpr + (mk_expr + (AilEcall (mk_expr (AilEident (Sym.fresh "push_focus_context")), []))) + in + [ cn_stack_depth_incr_stat_; push_focus_context ]) in let bump_alloc_binding, bump_alloc_start_stat_, bump_alloc_end_stat_ = gen_bump_alloc_bs_and_ss () diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index c517136e8..7881fc339 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -268,16 +268,14 @@ let memory_accesses_injections ail_prog = List.iter (* HK: Currently, `env` is ignored. It will be used in future patches. *) (fun (access, env) -> + let fmt, args = gen_env_fmt_printer env in + let fmt = "[auto annot (focus)]: " ^ fmt ^ "\\n" in + let args = List.fold_left (fun acc arg -> acc ^ ", " ^ arg) "" args in + let args = ", \"" ^ fmt ^ "\"" ^ args in match access with | Load { loc; _ } -> let b, e = pos_bbox loc in - let fmt, args = gen_env_fmt_printer env in - let fmt = "[auto annot (focus)]: " ^ fmt ^ "\\n" in - let args = List.fold_left (fun acc arg -> acc ^ ", " ^ arg) "" args in - acc - := (point b, [ "CN_LOAD_ANNOT(" ]) - :: (point e, [ ", \"" ^ fmt ^ "\"" ^ args ^ ")" ]) - :: !acc + acc := (point b, [ "CN_LOAD_ANNOT(" ]) :: (point e, [ args ^ ")" ]) :: !acc | Store { lvalue; expr; _ } -> (* NOTE: we are not using the location of the access (the AilEassign), because if in the source the assignment was surrounded by parens its location will contain @@ -287,7 +285,7 @@ let memory_accesses_injections ail_prog = acc := (point b, [ "CN_STORE_ANNOT(" ]) :: (region (pos1, pos2) NoCursor, [ ", " ]) - :: (point e, [ ")" ]) + :: (point e, [ args ^ ")" ]) :: !acc | StoreOp { lvalue; aop; expr; loc } -> (match bbox [ loc_of_expr expr ] with diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index 28a139511..a27e89723 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -648,16 +648,16 @@ static inline void cn_postfix(void* ptr, size_t size) { #define CN_STORE(LV, X) CN_STORE_OP(LV, , X) -#define CN_STORE_OP_ANNOT(LV, op, X) \ +#define CN_STORE_OP_ANNOT(LV, op, X, FMT, ...) \ ({ \ typeof(LV) *__tmp; \ __tmp = &(LV); \ if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) \ - cn_printf(CN_LOGGING_ERROR, "needs focus\n"); \ + cn_printf(CN_LOGGING_ERROR, FMT, ##__VA_ARGS__); \ CN_STORE_OP(LV, op, X); \ }) -#define CN_STORE_ANNOT(LV, X) CN_STORE_OP_ANNOT(LV, , X) +#define CN_STORE_ANNOT(LV, X, FMT, ...) CN_STORE_OP_ANNOT(LV, , X, FMT, ##__VA_ARGS__) #define CN_POSTFIX(LV, OP) \ ({ \ From 2ccb63915357cb5fe2ca19f3e9ea9abdac45a5ba Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 14 Aug 2025 18:32:50 +0100 Subject: [PATCH 12/38] Add line number --- lib/fulminate/fulminate.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index 7881fc339..f57abacb9 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -269,12 +269,15 @@ let memory_accesses_injections ail_prog = (* HK: Currently, `env` is ignored. It will be used in future patches. *) (fun (access, env) -> let fmt, args = gen_env_fmt_printer env in - let fmt = "[auto annot (focus)]: " ^ fmt ^ "\\n" in + let fmt = fmt ^ "\\n" in let args = List.fold_left (fun acc arg -> acc ^ ", " ^ arg) "" args in - let args = ", \"" ^ fmt ^ "\"" ^ args in match access with | Load { loc; _ } -> let b, e = pos_bbox loc in + let pos_info = Cerb_location.location_to_string loc in + let args = + ", \"" ^ "[auto annot (focus)]" ^ pos_info ^ ", " ^ fmt ^ "\"" ^ args + in acc := (point b, [ "CN_LOAD_ANNOT(" ]) :: (point e, [ args ^ ")" ]) :: !acc | Store { lvalue; expr; _ } -> (* NOTE: we are not using the location of the access (the AilEassign), because if @@ -282,6 +285,10 @@ let memory_accesses_injections ail_prog = the parens, which will break the CN_STORE macro call *) let b, pos1 = pos_bbox (loc_of_expr lvalue) in let pos2, e = pos_bbox (loc_of_expr expr) in + let pos_info = Cerb_location.location_to_string (loc_of_expr lvalue) in + let args = + ", \"" ^ "[auto annot (focus)]" ^ pos_info ^ ", " ^ fmt ^ "\"" ^ args + in acc := (point b, [ "CN_STORE_ANNOT(" ]) :: (region (pos1, pos2) NoCursor, [ ", " ]) From 0bde239d5a1b9f3845245c0c9134ca0bb80c2ce5 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Fri, 15 Aug 2025 12:22:40 +0100 Subject: [PATCH 13/38] Fix a printer logging problem for storeop --- lib/fulminate/fulminate.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index f57abacb9..37be256bf 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -278,7 +278,7 @@ let memory_accesses_injections ail_prog = let args = ", \"" ^ "[auto annot (focus)]" ^ pos_info ^ ", " ^ fmt ^ "\"" ^ args in - acc := (point b, [ "CN_LOAD_ANNOT(" ]) :: (point e, [ args ^ ")" ]) :: !acc + acc := (point b, [ "CN_LOAD_ANNOT (" ]) :: (point e, [ args ^ ")" ]) :: !acc | Store { lvalue; expr; _ } -> (* NOTE: we are not using the location of the access (the AilEassign), because if in the source the assignment was surrounded by parens its location will contain @@ -302,6 +302,10 @@ let memory_accesses_injections ail_prog = simple literals *) let pp_expr e = CF.Pp_utils.to_plain_string (Pp_ail.pp_expression e) in let sstart, ssend = pos_bbox loc in + let pos_info = Cerb_location.location_to_string loc in + let args = + ", \"" ^ "[auto annot (focus)]" ^ pos_info ^ ", " ^ fmt ^ "\"" ^ args + in let b, _ = pos_bbox (loc_of_expr lvalue) in acc := (region (sstart, b) NoCursor, [ "" ]) @@ -312,6 +316,7 @@ let memory_accesses_injections ail_prog = ^ string_of_aop aop ^ "," ^ pp_expr expr + ^ args ^ ")" ] ) :: (region (b, ssend) NoCursor, [ "" ]) @@ -319,10 +324,14 @@ let memory_accesses_injections ail_prog = | `Bbox _ -> let b, pos1 = pos_bbox (loc_of_expr lvalue) in let pos2, e = pos_bbox (loc_of_expr expr) in + let pos_info = Cerb_location.location_to_string (loc_of_expr lvalue) in + let args = + ", \"" ^ "[auto annot (focus)]" ^ pos_info ^ ", " ^ fmt ^ "\"" ^ args + in acc := (point b, [ "CN_STORE_OP_ANNOT(" ]) :: (region (pos1, pos2) NoCursor, [ "," ^ string_of_aop aop ^ "," ]) - :: (point e, [ ")" ]) + :: (point e, [ args ^ ")" ]) :: !acc) | Postfix { loc; op; lvalue } -> let op_str = match op with `Incr -> "++" | `Decr -> "--" in From d973d59d2f1c07aa50a62574baa44f890e55a7d1 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Fri, 15 Aug 2025 12:34:26 +0100 Subject: [PATCH 14/38] Small refactoring --- lib/fulminate/fulminate.ml | 59 ++++++++++++++++++++++++++++---------- 1 file changed, 44 insertions(+), 15 deletions(-) diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index 37be256bf..7d53e68dd 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -266,19 +266,30 @@ let memory_accesses_injections ail_prog = let acc = ref [] in let xs = collect_memory_accesses ail_prog in List.iter - (* HK: Currently, `env` is ignored. It will be used in future patches. *) (fun (access, env) -> + (* autoannot things *) let fmt, args = gen_env_fmt_printer env in - let fmt = fmt ^ "\\n" in - let args = List.fold_left (fun acc arg -> acc ^ ", " ^ arg) "" args in + let autoannot_fmt = fmt ^ "\\n" in + let autoannot_fmt_args = + List.fold_left (fun acc arg -> acc ^ ", " ^ arg) "" args + in match access with | Load { loc; _ } -> let b, e = pos_bbox loc in let pos_info = Cerb_location.location_to_string loc in - let args = - ", \"" ^ "[auto annot (focus)]" ^ pos_info ^ ", " ^ fmt ^ "\"" ^ args + let autoannot_fmt_args = + ", \"" + ^ "[auto annot (focus)]" + ^ pos_info + ^ ", " + ^ autoannot_fmt + ^ "\"" + ^ autoannot_fmt_args in - acc := (point b, [ "CN_LOAD_ANNOT (" ]) :: (point e, [ args ^ ")" ]) :: !acc + acc + := (point b, [ "CN_LOAD_ANNOT (" ]) + :: (point e, [ autoannot_fmt_args ^ ")" ]) + :: !acc | Store { lvalue; expr; _ } -> (* NOTE: we are not using the location of the access (the AilEassign), because if in the source the assignment was surrounded by parens its location will contain @@ -286,13 +297,19 @@ let memory_accesses_injections ail_prog = let b, pos1 = pos_bbox (loc_of_expr lvalue) in let pos2, e = pos_bbox (loc_of_expr expr) in let pos_info = Cerb_location.location_to_string (loc_of_expr lvalue) in - let args = - ", \"" ^ "[auto annot (focus)]" ^ pos_info ^ ", " ^ fmt ^ "\"" ^ args + let autoannot_fmt_args = + ", \"" + ^ "[auto annot (focus)]" + ^ pos_info + ^ ", " + ^ autoannot_fmt + ^ "\"" + ^ autoannot_fmt_args in acc := (point b, [ "CN_STORE_ANNOT(" ]) :: (region (pos1, pos2) NoCursor, [ ", " ]) - :: (point e, [ args ^ ")" ]) + :: (point e, [ autoannot_fmt_args ^ ")" ]) :: !acc | StoreOp { lvalue; aop; expr; loc } -> (match bbox [ loc_of_expr expr ] with @@ -303,8 +320,14 @@ let memory_accesses_injections ail_prog = let pp_expr e = CF.Pp_utils.to_plain_string (Pp_ail.pp_expression e) in let sstart, ssend = pos_bbox loc in let pos_info = Cerb_location.location_to_string loc in - let args = - ", \"" ^ "[auto annot (focus)]" ^ pos_info ^ ", " ^ fmt ^ "\"" ^ args + let autoannot_fmt_args = + ", \"" + ^ "[auto annot (focus)]" + ^ pos_info + ^ ", " + ^ autoannot_fmt + ^ "\"" + ^ autoannot_fmt_args in let b, _ = pos_bbox (loc_of_expr lvalue) in acc @@ -316,7 +339,7 @@ let memory_accesses_injections ail_prog = ^ string_of_aop aop ^ "," ^ pp_expr expr - ^ args + ^ autoannot_fmt_args ^ ")" ] ) :: (region (b, ssend) NoCursor, [ "" ]) @@ -325,13 +348,19 @@ let memory_accesses_injections ail_prog = let b, pos1 = pos_bbox (loc_of_expr lvalue) in let pos2, e = pos_bbox (loc_of_expr expr) in let pos_info = Cerb_location.location_to_string (loc_of_expr lvalue) in - let args = - ", \"" ^ "[auto annot (focus)]" ^ pos_info ^ ", " ^ fmt ^ "\"" ^ args + let autoannot_fmt_args = + ", \"" + ^ "[auto annot (focus)]" + ^ pos_info + ^ ", " + ^ autoannot_fmt + ^ "\"" + ^ autoannot_fmt_args in acc := (point b, [ "CN_STORE_OP_ANNOT(" ]) :: (region (pos1, pos2) NoCursor, [ "," ^ string_of_aop aop ^ "," ]) - :: (point e, [ args ^ ")" ]) + :: (point e, [ autoannot_fmt_args ^ ")" ]) :: !acc) | Postfix { loc; op; lvalue } -> let op_str = match op with `Incr -> "++" | `Decr -> "--" in From b4f5e256b5ee19a5d4161d3608cb2537d2d4ea94 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Fri, 15 Aug 2025 17:39:26 +0100 Subject: [PATCH 15/38] Handle loop (wip) --- lib/fulminate/cn_to_ail.ml | 15 ++++++++++++++- lib/fulminate/fulminate.ml | 2 +- lib/fulminate/internal.ml | 13 ++++++++++++- 3 files changed, 27 insertions(+), 3 deletions(-) diff --git a/lib/fulminate/cn_to_ail.ml b/lib/fulminate/cn_to_ail.ml index aa6c8dad7..1f3ab7f56 100644 --- a/lib/fulminate/cn_to_ail.ml +++ b/lib/fulminate/cn_to_ail.ml @@ -4337,8 +4337,21 @@ let cn_to_ail_loop_inv let cn_ownership_leak_check_call = A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident OE.cn_loop_leak_check_sym), []))) in + (* reset the current focus context *) + let pop_focus_context_fn_call = + A.AilSexpr + (mk_expr (AilEcall (mk_expr (AilEident (Sym.fresh "push_focus_context")), []))) + in + let push_focus_context_fn_call = + A.AilSexpr + (mk_expr (AilEcall (mk_expr (AilEident (Sym.fresh "push_focus_context")), []))) + in let stats = - (bump_alloc_assign :: loop_ownership_state.assign :: cond_ss) + (bump_alloc_assign + :: loop_ownership_state.assign + :: pop_focus_context_fn_call + :: push_focus_context_fn_call + :: cond_ss) @ (if with_loop_leak_checks then [ cn_ownership_leak_check_call ] else []) @ [ cn_loop_put_call; dummy_expr_as_stat ] in diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index 7d53e68dd..52d685a98 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -287,7 +287,7 @@ let memory_accesses_injections ail_prog = ^ autoannot_fmt_args in acc - := (point b, [ "CN_LOAD_ANNOT (" ]) + := (point b, [ "CN_LOAD_ANNOT(" ]) :: (point e, [ autoannot_fmt_args ^ ")" ]) :: !acc | Store { lvalue; expr; _ } -> diff --git a/lib/fulminate/internal.ml b/lib/fulminate/internal.ml index 411061513..dc08d3414 100644 --- a/lib/fulminate/internal.ml +++ b/lib/fulminate/internal.ml @@ -123,7 +123,18 @@ let generate_c_loop_invariants [ cond_inj; decl_inj; end_internal_inj; end_external_inj ]) ail_loop_invariants in - List.concat injs) + let ail_loop_decl_injs = + List.map + (fun (loc, bs_and_ss) -> + (get_start_loc loc, "{" :: generate_ail_stat_strs bs_and_ss)) + ail_loop_decls + in + let ail_loop_close_block_injs = + List.map + (fun (loc, _) -> (get_end_loc loc, [ "} \nclear_focus ();" ])) + ail_loop_decls + in + ail_cond_injs @ ail_loop_decl_injs @ ail_loop_close_block_injs) let generate_fn_call_ghost_args_injs From 3c6d634563aaf01a5db7e041467d971dff6ff892 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Fri, 15 Aug 2025 17:47:51 +0100 Subject: [PATCH 16/38] Add clear_focus function --- runtime/libcn/include/cn-autoannot/focus_ctx.h | 1 + runtime/libcn/src/cn-autoannot/focus_ctx.c | 10 ++++++++++ runtime/libcn/test/autoannot/focus.cpp | 6 ++++++ 3 files changed, 17 insertions(+) diff --git a/runtime/libcn/include/cn-autoannot/focus_ctx.h b/runtime/libcn/include/cn-autoannot/focus_ctx.h index 063d12c75..fbbc6bd73 100644 --- a/runtime/libcn/include/cn-autoannot/focus_ctx.h +++ b/runtime/libcn/include/cn-autoannot/focus_ctx.h @@ -52,6 +52,7 @@ struct focus_context { void initialise_focus_context(void); void push_focus_context(void); void pop_focus_context(void); +void clear_focus(void); void insert_focus(int64_t index, type_sig sig); void insert_iter_res( uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig); diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index 4b183e827..c614113c5 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -60,6 +60,16 @@ void insert_focus(int64_t index, type_sig sig) { cn_focus_global_context->indices = new_set; } +void clear_focus() { + focus_set *cur_focus = cn_focus_global_context->indices; + while (cur_focus) { + focus_set *next = cur_focus->next; + fulm_free(cur_focus, &fulm_default_alloc); + cur_focus = next; + } + cn_focus_global_context->indices = NULL; +} + void insert_iter_res(uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig) { struct iter_res_set* new = fulm_malloc(sizeof(iter_res_set), &fulm_default_alloc); new->res.ptr = ptr; diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp index 21a94d708..fb1d4f9b8 100644 --- a/runtime/libcn/test/autoannot/focus.cpp +++ b/runtime/libcn/test/autoannot/focus.cpp @@ -23,6 +23,12 @@ TEST(LibAutoAnnot, BasicOperations) { ASSERT_EQ(needs_focus(0xcafe1000, 8), 0) << "No appropriate resource, so we don't need focus"; + clear_focus(); + ASSERT_EQ(needs_focus(0xcafe0008, 8), 1) << "Cleared"; + + insert_focus(1, "unsigned long"); + ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Focused"; + push_focus_context(); insert_iter_res(0xcafe0000, 0, 4, 8, "unsigned long"); insert_iter_res(0x10000000, 1, 4, 8, "unsigned long"); From 5bdeebf70b485bdf3e3ff0ad46b04c27f4645c32 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 18 Aug 2025 12:47:52 +0100 Subject: [PATCH 17/38] Add switch for introducing autoannot things --- lib/fulminate/cn_to_ail.ml | 19 ++++++----- lib/fulminate/config.ml | 1 + lib/fulminate/config.mli | 1 + lib/fulminate/fulminate.ml | 68 ++++++++++++++++++++++++++------------ 4 files changed, 60 insertions(+), 29 deletions(-) create mode 100644 lib/fulminate/config.ml create mode 100644 lib/fulminate/config.mli diff --git a/lib/fulminate/cn_to_ail.ml b/lib/fulminate/cn_to_ail.ml index 1f3ab7f56..dea30fa48 100644 --- a/lib/fulminate/cn_to_ail.ml +++ b/lib/fulminate/cn_to_ail.ml @@ -3098,7 +3098,7 @@ let cn_to_ail_resource let _, _, e_pointer = cn_to_ail_expr filename dts globals spec_mode_opt q.pointer PassBack in - let itere_res_call_stmt_opt = + let iter_res_call_stmt_opt = match q.name with | Owned (sct, _) -> let type_str = Pp.plain (Sctypes.pp sct) in @@ -3230,8 +3230,8 @@ let cn_to_ail_resource in let stmts = [ start_assign; while_loop ] in let stmts = - match (itere_res_call_stmt_opt, spec_mode_opt) with - | Some stmt, Some Pre -> stmt :: stmts + match (iter_res_call_stmt_opt, spec_mode_opt) with + | Some stmt, Some Pre when !Config.with_auto_annot -> stmt :: stmts | _ -> stmts in let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in @@ -3290,8 +3290,8 @@ let cn_to_ail_resource in let stmts = [ start_assign; while_loop ] in let stmts = - match (itere_res_call_stmt_opt, spec_mode_opt) with - | Some stmt, Some Pre -> stmt :: stmts + match (iter_res_call_stmt_opt, spec_mode_opt) with + | Some stmt, Some Pre when !Config.with_auto_annot -> stmt :: stmts | _ -> stmts in let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in @@ -3809,6 +3809,7 @@ let cn_to_ail_cnstatement | Have _lc -> failwith "TODO Have" | Instantiate (_to_instantiate, _it) -> (default_res_for_dest, true) | Split_case _ -> (default_res_for_dest, true) + | Extract (_, _, _) when not !Config.with_auto_annot -> (default_res_for_dest, true) | Extract (_, to_extract, it) -> let b, ss, e = cn_to_ail_expr filename dts globals spec_mode_opt it PassBack in (match to_extract with @@ -4349,9 +4350,11 @@ let cn_to_ail_loop_inv let stats = (bump_alloc_assign :: loop_ownership_state.assign - :: pop_focus_context_fn_call - :: push_focus_context_fn_call - :: cond_ss) + :: + (if !Config.with_auto_annot then + pop_focus_context_fn_call :: push_focus_context_fn_call :: cond_ss + else + cond_ss)) @ (if with_loop_leak_checks then [ cn_ownership_leak_check_call ] else []) @ [ cn_loop_put_call; dummy_expr_as_stat ] in diff --git a/lib/fulminate/config.ml b/lib/fulminate/config.ml new file mode 100644 index 000000000..88c4477fb --- /dev/null +++ b/lib/fulminate/config.ml @@ -0,0 +1 @@ +let with_auto_annot = ref false diff --git a/lib/fulminate/config.mli b/lib/fulminate/config.mli new file mode 100644 index 000000000..35ddebbf8 --- /dev/null +++ b/lib/fulminate/config.mli @@ -0,0 +1 @@ +val with_auto_annot : bool ref diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index 52d685a98..98d286e31 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -287,9 +287,12 @@ let memory_accesses_injections ail_prog = ^ autoannot_fmt_args in acc - := (point b, [ "CN_LOAD_ANNOT(" ]) - :: (point e, [ autoannot_fmt_args ^ ")" ]) - :: !acc + := if !Config.with_auto_annot then + (point b, [ "CN_LOAD_ANNOT(" ]) + :: (point e, [ autoannot_fmt_args ^ ")" ]) + :: !acc + else + (point b, [ "CN_LOAD(" ]) :: (point e, [ ")" ]) :: !acc | Store { lvalue; expr; _ } -> (* NOTE: we are not using the location of the access (the AilEassign), because if in the source the assignment was surrounded by parens its location will contain @@ -307,10 +310,16 @@ let memory_accesses_injections ail_prog = ^ autoannot_fmt_args in acc - := (point b, [ "CN_STORE_ANNOT(" ]) - :: (region (pos1, pos2) NoCursor, [ ", " ]) - :: (point e, [ autoannot_fmt_args ^ ")" ]) - :: !acc + := if !Config.with_auto_annot then + (point b, [ "CN_STORE_ANNOT(" ]) + :: (region (pos1, pos2) NoCursor, [ ", " ]) + :: (point e, [ autoannot_fmt_args ^ ")" ]) + :: !acc + else + (point b, [ "CN_STORE(" ]) + :: (region (pos1, pos2) NoCursor, [ ", " ]) + :: (point e, [ ")" ]) + :: !acc | StoreOp { lvalue; aop; expr; loc } -> (match bbox [ loc_of_expr expr ] with | `Other _ -> @@ -332,16 +341,27 @@ let memory_accesses_injections ail_prog = let b, _ = pos_bbox (loc_of_expr lvalue) in acc := (region (sstart, b) NoCursor, [ "" ]) - :: ( point b, - [ "CN_STORE_OP_ANNOT(" - ^ pp_expr lvalue - ^ "," - ^ string_of_aop aop - ^ "," - ^ pp_expr expr - ^ autoannot_fmt_args - ^ ")" - ] ) + :: (if !Config.with_auto_annot then + ( point b, + [ "CN_STORE_OP_ANNOT(" + ^ pp_expr lvalue + ^ "," + ^ string_of_aop aop + ^ "," + ^ pp_expr expr + ^ autoannot_fmt_args + ^ ")" + ] ) + else + ( point b, + [ "CN_STORE_OP(" + ^ pp_expr lvalue + ^ "," + ^ string_of_aop aop + ^ "," + ^ pp_expr expr + ^ ")" + ] )) :: (region (b, ssend) NoCursor, [ "" ]) :: !acc | `Bbox _ -> @@ -358,10 +378,16 @@ let memory_accesses_injections ail_prog = ^ autoannot_fmt_args in acc - := (point b, [ "CN_STORE_OP_ANNOT(" ]) - :: (region (pos1, pos2) NoCursor, [ "," ^ string_of_aop aop ^ "," ]) - :: (point e, [ autoannot_fmt_args ^ ")" ]) - :: !acc) + := if !Config.with_auto_annot then + (point b, [ "CN_STORE_OP_ANNOT(" ]) + :: (region (pos1, pos2) NoCursor, [ "," ^ string_of_aop aop ^ "," ]) + :: (point e, [ autoannot_fmt_args ^ ")" ]) + :: !acc + else + (point b, [ "CN_STORE_OP(" ]) + :: (region (pos1, pos2) NoCursor, [ "," ^ string_of_aop aop ^ "," ]) + :: (point e, [ ")" ]) + :: !acc) | Postfix { loc; op; lvalue } -> let op_str = match op with `Incr -> "++" | `Decr -> "--" in let b, e = pos_bbox loc in From 37ccabe72f3f02610a0d23f3e0bde938a6e2bd52 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 18 Aug 2025 15:37:15 +0100 Subject: [PATCH 18/38] Add autoannot subcommand --- bin/autoAnnot.ml | 555 ++++++++++++++++++++++++++++++++++++ bin/common.ml | 2 + bin/instrument.ml | 8 + bin/main.ml | 4 +- lib/fulminate/cn_to_ail.ml | 18 +- lib/fulminate/config.ml | 4 + lib/fulminate/config.mli | 4 + lib/fulminate/fulminate.ml | 6 +- lib/fulminate/fulminate.mli | 1 + lib/fulminate/internal.ml | 5 +- lib/fulminate/ownership.ml | 19 +- 11 files changed, 606 insertions(+), 20 deletions(-) create mode 100644 bin/autoAnnot.ml diff --git a/bin/autoAnnot.ml b/bin/autoAnnot.ml new file mode 100644 index 000000000..ba2049e47 --- /dev/null +++ b/bin/autoAnnot.ml @@ -0,0 +1,555 @@ +(* Almost a copy of test.ml. Might be better to extract common parts. *) +module CF = Cerb_frontend +module CB = Cerb_backend +open Cn + +let run_auto_annot + (* Common *) + filename + cc + macros + incl_dirs + incl_files + debug_level + print_level + csv_times + astprints + no_inherit_loc + magic_comment_char_dollar + allow_split_magic_comments + (* Executable spec *) + without_ownership_checking + (* without_loop_invariants *) + (* Test Generation *) + print_steps + output_dir + only + skip + dont_run + num_samples + max_backtracks + _max_unfolds + _max_array_length + build_tool + sanitizers + print_seed + input_timeout + null_in_every + seed + logging_level + trace_granularity + progress_level + until_timeout + exit_fast + max_stack_depth + _allowed_depth_failures + max_generator_size + sizing_strategy + random_size_splits + allowed_size_split_backtracks + _sized_null + coverage + disable_passes + trap + no_replays + no_replicas + output_tyche + inline_everything + experimental_struct_asgn_destruction + experimental_product_arg_destruction + experimental_learning + smt_pruning + print_size_info + print_backtrack_info + print_satisfaction_info + = + (* flags *) + Cerb_debug.debug_level := debug_level; + Pp.print_level := print_level; + Check.skip_and_only := (skip, only); + Sym.executable_spec_enabled := true; + let handle_error (e : TypeErrors.t) = + let report = TypeErrors.pp_message e.msg in + Pp.error e.loc report.short (Option.to_list report.descr); + match e.msg with TypeErrors.Unsupported _ -> exit 2 | _ -> exit 1 + in + let filename = Common.there_can_only_be_one filename in + let output_dir = + Common.mk_dir_if_not_exist_maybe_tmp ~mktemp:true AutoAnnot output_dir + in + Pp.(debug 2 (lazy (item "Output directory" (string output_dir)))); + let basefile = Filename.basename filename in + let pp_file = Filename.temp_file "cn_" basefile in + let out_file = Fulminate.get_instrumented_filename basefile in + Common.with_well_formedness_check (* CLI arguments *) + ~filename + ~cc + ~macros:(("__CN_TEST", None) :: ("__CN_INSTRUMENT", None) :: macros) + ~incl_dirs + ~incl_files + ~csv_times + ~coq_export_file:None + ~coq_mucore:false + ~coq_proof_log:false + ~coq_check_proof_log:false + ~astprints + ~no_inherit_loc + ~magic_comment_char_dollar + ~allow_split_magic_comments (* Callbacks *) + ~save_cpp:(Some pp_file) + ~disable_linemarkers:true + ~skip_label_inlining:true + ~handle_error + ~f:(fun ~cabs_tunit ~prog5 ~ail_prog ~statement_locs:_ ~paused -> + let config : TestGeneration.config = + { cc; + print_steps; + num_samples; + max_backtracks; + build_tool; + sanitizers; + inline_everything; + experimental_struct_asgn_destruction; + experimental_product_arg_destruction; + experimental_learning; + smt_pruning; + print_seed; + input_timeout; + null_in_every; + seed; + logging_level; + trace_granularity; + progress_level; + until_timeout; + exit_fast; + max_stack_depth; + max_generator_size; + sizing_strategy; + random_size_splits; + allowed_size_split_backtracks; + coverage; + disable_passes; + trap; + no_replays; + no_replicas; + output_tyche; + print_size_info; + print_backtrack_info; + print_satisfaction_info + } + in + TestGeneration.set_config config; + let _, sigma = ail_prog in + if + List.is_empty + (TestGeneration.functions_under_test + ~with_warning:true + cabs_tunit + sigma + prog5 + paused) + then ( + print_endline "No testable functions, trivially passing"; + exit 0); + (* Enable additional instrumentations for auto-annot *) + Fulminate.Config.enable_auto_annot (); + Cerb_colour.do_colour := false; + (try + Fulminate.main + ~without_ownership_checking + ~without_loop_invariants:true + ~with_loop_leak_checks:false + ~with_testing:true + filename + cc + pp_file + out_file + output_dir + cabs_tunit + ail_prog + prog5 + with + | e -> Common.handle_error_with_user_guidance ~label:"CN-Exec" e); + (try + TestGeneration.run + ~output_dir + ~filename + ~without_ownership_checking + build_tool + cabs_tunit + sigma + prog5 + paused + with + | e -> Common.handle_error_with_user_guidance ~label:"CN-Test-Gen" e); + if not dont_run then ( + Cerb_debug.maybe_close_csv_timing_file (); + match build_tool with + | Bash -> + Unix.execv (Filename.concat output_dir "run_tests.sh") (Array.of_list []) + | Make -> + Unix.chdir output_dir; + Unix.execvp "make" (Array.of_list [ "make" ])); + Result.ok ()) + + +open Cmdliner + +module Flags = struct + let print_steps = + let doc = + "Print successful stages, such as directory creation, compilation and linking." + in + Arg.(value & flag & info [ "print-steps" ] ~doc) + + + let output_dir = + let doc = "Place generated tests in the provided directory" in + Arg.(value & opt (some string) None & info [ "output-dir" ] ~docv:"DIR" ~doc) + + + let only = + let doc = "Only test this function (or comma-separated names)" in + Arg.(value & opt (list string) [] & info [ "only" ] ~doc) + + + let skip = + let doc = "Skip testing of this function (or comma-separated names)" in + Arg.(value & opt (list string) [] & info [ "skip" ] ~doc) + + + let dont_run = + let doc = "Do not run tests, only generate them" in + Arg.(value & flag & info [ "no-run" ] ~doc) + + + let gen_num_samples = + let doc = "Set the number of samples to test" in + Arg.( + value & opt int TestGeneration.default_cfg.num_samples & info [ "num-samples" ] ~doc) + + + let gen_backtrack_attempts = + let doc = + "Set the maximum attempts to satisfy a constraint before backtracking further, \ + during input generation" + in + Arg.( + value + & opt int TestGeneration.default_cfg.max_backtracks + & info [ "max-backtrack-attempts" ] ~doc) + + + let gen_max_unfolds = + let doc = "Does nothing." in + let deprecated = "Will be removed after June 31." in + Arg.(value & opt (some int) None & info [ "max-unfolds" ] ~deprecated ~doc) + + + let max_array_length = + let doc = "Does nothing." in + let deprecated = "Will be removed after June 31." in + Arg.(value & opt int 0 & info [ "max-array-length" ] ~deprecated ~doc) + + + let build_tool = + let doc = "Set which build tool to use." in + Arg.( + value + & opt (enum TestGeneration.Options.build_tool) TestGeneration.default_cfg.build_tool + & info [ "build-tool" ] ~doc) + + + let sanitize = + let doc = "Forwarded to the '-fsanitize' argument of the C compiler" in + Arg.( + value + & opt (some string) (fst TestGeneration.default_cfg.sanitizers) + & info [ "sanitize" ] ~doc) + + + let no_sanitize = + let doc = "Forwarded to the '-fno-sanitize' argument of the C compiler" in + Arg.( + value + & opt (some string) (snd TestGeneration.default_cfg.sanitizers) + & info [ "no-sanitize" ] ~doc) + + + let print_seed = + let doc = "Print seed used by PRNG." in + Arg.(value & flag & info [ "print-seed" ] ~doc) + + + let input_timeout = + let doc = "Timeout for discarding a generation attempt (ms)" in + Arg.( + value + & opt (some int) TestGeneration.default_cfg.input_timeout + & info [ "input-timeout" ] ~doc) + + + let null_in_every = + let doc = "Set the likelihood of NULL being generated as 1 in every " in + Arg.( + value + & opt (some int) TestGeneration.default_cfg.null_in_every + & info [ "null-in-every" ] ~doc) + + + let seed = + let doc = "Set the seed for random testing" in + Arg.(value & opt (some string) TestGeneration.default_cfg.seed & info [ "seed" ] ~doc) + + + let logging_level = + let doc = "Set the logging level for failing inputs from tests" in + Arg.( + value + & opt + (some (enum TestGeneration.Options.logging_level)) + TestGeneration.default_cfg.logging_level + & info [ "logging-level" ] ~doc) + + + let trace_granularity = + let doc = "Set the trace granularity for failing inputs from tests" in + Arg.( + value + & opt + (some (enum TestGeneration.Options.trace_granularity)) + TestGeneration.default_cfg.trace_granularity + & info [ "trace-granularity" ] ~doc) + + + let progress_level = + let doc = "Set the frequency of progress updates." in + Arg.( + value + & opt + (some (enum TestGeneration.Options.progress_level)) + TestGeneration.default_cfg.progress_level + & info [ "progress-level" ] ~doc) + + + let until_timeout = + let doc = + "Keep rerunning tests until the given timeout (in seconds) has been reached" + in + Arg.( + value + & opt (some int) TestGeneration.default_cfg.until_timeout + & info [ "until-timeout" ] ~doc) + + + let exit_fast = + let doc = "Stop testing upon finding the first failure" in + Arg.(value & flag & info [ "exit-fast" ] ~doc) + + + let max_stack_depth = + let doc = "Maximum stack depth for generators" in + Arg.( + value + & opt (some int) TestGeneration.default_cfg.max_stack_depth + & info [ "max-stack-depth" ] ~doc) + + + let allowed_depth_failures = + let doc = "Does nothing." in + let deprecated = "Will be removed after July 31." in + Arg.(value & opt (some int) None & info [ "allowed-depth-failures" ] ~deprecated ~doc) + + + let max_generator_size = + let doc = "Maximum size for generated values" in + Arg.( + value + & opt (some int) TestGeneration.default_cfg.max_generator_size + & info [ "max-generator-size" ] ~doc) + + + let sizing_strategy = + let doc = "Strategy for deciding test case size." in + Arg.( + value + & opt + (some (enum TestGeneration.Options.sizing_strategy)) + TestGeneration.default_cfg.sizing_strategy + & info [ "sizing-strategy" ] ~doc) + + + let random_size_splits = + let doc = "Randomly split sizes between recursive generator calls" in + Arg.(value & flag & info [ "random-size-splits" ] ~doc) + + + let allowed_size_split_backtracks = + let doc = + "Set the maximum attempts to split up a generator's size (between recursive calls) \ + before backtracking further, during input generation" + in + Arg.( + value + & opt (some int) TestGeneration.default_cfg.allowed_size_split_backtracks + & info [ "allowed-size-split-backtracks" ] ~doc) + + + let sized_null = + let doc = "Does nothing." in + let deprecated = "Will be removed after July 31." in + Arg.(value & flag & info [ "sized-null" ] ~deprecated ~doc) + + + let coverage = + let doc = "(Experimental) Record coverage of tests via [lcov]" in + Arg.(value & flag & info [ "coverage" ] ~doc) + + + let disable_passes = + let doc = "skip this optimization pass (or comma-separated names)" in + Arg.( + value + & opt + (list + (enum + [ ("reorder", "reorder"); + ("picks", "picks"); + ("flatten", "flatten"); + ("consistency", "consistency"); + ("lift_constraints", "lift_constraints") + ])) + [] + & info [ "disable" ] ~doc) + + + let trap = + let doc = "Raise SIGTRAP on test failure" in + Arg.(value & flag & info [ "trap" ] ~doc) + + + let no_replays = + let doc = "Disable replaying errors for error messages" in + Arg.(value & flag & info [ "no-replays" ] ~doc) + + + let no_replicas = + let doc = "Disable synthesizing C code to replicate bugs" in + Arg.(value & flag & info [ "no-replicas" ] ~doc) + + + let output_tyche = + let doc = "Enable output in Tyche format" in + Arg.( + value + & opt (some string) TestGeneration.default_cfg.output_tyche + & info [ "output-tyche" ] ~doc) + + + let inline_everything = + let doc = "Maximally inline everything" in + Arg.(value & flag & info [ "inline-everything" ] ~doc) + + + let experimental_struct_asgn_destruction = + let doc = "Destructs struct assignments" in + Arg.(value & flag & info [ "experimental-struct-asgn-destruction" ] ~doc) + + + let experimental_product_arg_destruction = + let doc = "Destructs all records and structs arguments" in + Arg.(value & flag & info [ "experimental-product-arg-destruction" ] ~doc) + + + let experimental_learning = + let doc = "Use experimental domain learning" in + Arg.(value & flag & info [ "experimental-learning" ] ~doc) + + + let smt_pruning = + let doc = "(Experimental) Use SMT solver to prune unsatisfiable branches" in + Arg.( + value + & opt (enum [ ("none", `None); ("fast", `Fast); ("slow", `Slow) ]) `None + & info [ "smt-pruning" ] ~doc) + + + let print_size_info = + let doc = "(Experimental) Print size info" in + Arg.(value & flag & info [ "print-size-info" ] ~doc) + + + let print_backtrack_info = + let doc = "(Experimental) Print backtracking info" in + Arg.(value & flag & info [ "print-backtrack-info" ] ~doc) + + + let print_satisfaction_info = + let doc = "(Experimental) Print satisfaction info" in + Arg.(value & flag & info [ "print-satisfaction-info" ] ~doc) +end + +let cmd = + let open Term in + let test_t = + const run_auto_annot + $ Common.Flags.file + $ Common.Flags.cc + $ Common.Flags.macros + $ Common.Flags.incl_dirs + $ Common.Flags.incl_files + $ Common.Flags.debug_level + $ Common.Flags.print_level + $ Common.Flags.csv_times + $ Common.Flags.astprints + $ Common.Flags.no_inherit_loc + $ Common.Flags.magic_comment_char_dollar + $ Common.Flags.allow_split_magic_comments + $ Instrument.Flags.without_ownership_checking + $ Flags.print_steps + $ Flags.output_dir + $ Flags.only + $ Flags.skip + $ Flags.dont_run + $ Flags.gen_num_samples + $ Flags.gen_backtrack_attempts + $ Flags.gen_max_unfolds + $ Flags.max_array_length + $ Flags.build_tool + $ Term.product Flags.sanitize Flags.no_sanitize + $ Flags.print_seed + $ Flags.input_timeout + $ Flags.null_in_every + $ Flags.seed + $ Flags.logging_level + $ Flags.trace_granularity + $ Flags.progress_level + $ Flags.until_timeout + $ Flags.exit_fast + $ Flags.max_stack_depth + $ Flags.allowed_depth_failures + $ Flags.max_generator_size + $ Flags.sizing_strategy + $ Flags.random_size_splits + $ Flags.allowed_size_split_backtracks + $ Flags.sized_null + $ Flags.coverage + $ Flags.disable_passes + $ Flags.trap + $ Flags.no_replays + $ Flags.no_replicas + $ Flags.output_tyche + $ Flags.inline_everything + $ Flags.experimental_struct_asgn_destruction + $ Flags.experimental_product_arg_destruction + $ Flags.experimental_learning + $ Flags.smt_pruning + $ Flags.print_size_info + $ Flags.print_backtrack_info + $ Flags.print_satisfaction_info + in + let doc = + "Generates proof annotations such as `unfold` and `focus` from testing executions." + in + let info = Cmd.info "auto-annot" ~doc in + Cmd.v info test_t diff --git a/bin/common.ml b/bin/common.ml index 164f654a9..0bf5dae8e 100644 --- a/bin/common.ml +++ b/bin/common.ml @@ -285,6 +285,7 @@ type subcommand = | Instrument | Test | SeqTest + | AutoAnnot let tool_name cmd = match cmd with @@ -292,6 +293,7 @@ let tool_name cmd = | Instrument -> "Fulminate" | Test -> "Bennet" | SeqTest -> "CN-Seq-Test" + | AutoAnnot -> "AutoAnnot" open Cmdliner diff --git a/bin/instrument.ml b/bin/instrument.ml index 868743e30..1c1eaeb75 100644 --- a/bin/instrument.ml +++ b/bin/instrument.ml @@ -105,6 +105,7 @@ let generate_executable_specs print_steps max_bump_blocks bump_block_size + with_auto_annot = (* flags *) Cerb_debug.debug_level := debug_level; @@ -117,6 +118,7 @@ let generate_executable_specs Diagnostics.diag_string := diag; Sym.executable_spec_enabled := true; Sym.experimental_unions := experimental_unions; + Fulminate.Config.with_auto_annot := with_auto_annot; let handle_error (e : TypeErrors.t) = let report = TypeErrors.pp_message e.msg in Pp.error e.loc report.short (Option.to_list report.descr); @@ -359,6 +361,11 @@ module Flags = struct let experimental_curly_braces = let doc = "(experimental) Insert curly braces for single-statement control flow" in Arg.(value & flag & info [ "insert-curly-braces" ] ~doc) + + + let with_auto_annot = + let doc = "Instrument additional information for auto-annot (for debugging)" in + Arg.(value & flag & info [ "with-auto-annot" ] ~doc) end let cmd = @@ -405,6 +412,7 @@ let cmd = $ Flags.print_steps $ Flags.max_bump_blocks $ Flags.bump_block_size + $ Flags.with_auto_annot in let doc = "Instruments [FILE] with runtime C assertions that check the properties provided in \ diff --git a/bin/main.ml b/bin/main.ml index af492c695..217085e7c 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -1,6 +1,8 @@ open Cmdliner -let subcommands = [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd ] +let subcommands = + [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd; AutoAnnot.cmd ] + let () = let version_str = Cn_version.git_version ^ " [" ^ Cn_version.git_version_date ^ "]" in diff --git a/lib/fulminate/cn_to_ail.ml b/lib/fulminate/cn_to_ail.ml index dea30fa48..837165b57 100644 --- a/lib/fulminate/cn_to_ail.ml +++ b/lib/fulminate/cn_to_ail.ml @@ -4539,11 +4539,14 @@ let rec cn_to_ail_lat_2 List.map (fun fn_sym -> mk_stmt (A.AilSexpr (mk_expr (AilEcall (mk_expr (AilEident fn_sym), []))))) - OE. - [ cn_stack_depth_decr_sym; - cn_postcondition_leak_check_sym; - Sym.fresh "pop_focus_context" - ] + (if !Config.with_auto_annot then + OE. + [ cn_stack_depth_decr_sym; + cn_postcondition_leak_check_sym; + Sym.fresh "pop_focus_context" + ] + else + OE.[ cn_stack_depth_decr_sym; cn_postcondition_leak_check_sym ]) in let block = A.( @@ -4761,7 +4764,10 @@ let cn_to_ail_pre_post (mk_expr (AilEcall (mk_expr (AilEident (Sym.fresh "push_focus_context")), []))) in - [ cn_stack_depth_incr_stat_; push_focus_context ]) + if !Config.with_auto_annot then + [ cn_stack_depth_incr_stat_; push_focus_context ] + else + [ cn_stack_depth_incr_stat_ ]) in let bump_alloc_binding, bump_alloc_start_stat_, bump_alloc_end_stat_ = gen_bump_alloc_bs_and_ss () diff --git a/lib/fulminate/config.ml b/lib/fulminate/config.ml index 88c4477fb..8efaee1ed 100644 --- a/lib/fulminate/config.ml +++ b/lib/fulminate/config.ml @@ -1 +1,5 @@ let with_auto_annot = ref false + +let enable_auto_annot () = with_auto_annot := true + +let disable_auto_annot () = with_auto_annot := false diff --git a/lib/fulminate/config.mli b/lib/fulminate/config.mli index 35ddebbf8..41ee0e929 100644 --- a/lib/fulminate/config.mli +++ b/lib/fulminate/config.mli @@ -1 +1,5 @@ val with_auto_annot : bool ref + +val enable_auto_annot : unit -> unit + +val disable_auto_annot : unit -> unit diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index 98d286e31..bad5353c3 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -7,6 +7,7 @@ module Internal = Internal module Records = Records module Ownership = Ownership module Utils = Utils +module Config = Config let rec group_toplevel_defs new_list = function | [] -> new_list @@ -225,7 +226,6 @@ let rec gen_env_fmt_printer = function | (sym, ty) :: xs -> let fmt, args = gen_env_fmt_printer xs in let open CF.Ctype in - Pp.(debug 10 (lazy (item "gen_env_fmt" (string (CF.Symbol.show_symbol sym))))); let (Ctype (_, ty)) = ty in (match ty with | Basic (Integer b) -> @@ -923,7 +923,9 @@ let main (* Save things *) let oc = Stdlib.open_out out_filename in output_to_oc oc [ "#define __CN_INSTRUMENT\n"; "#include \n" ]; - output_to_oc oc [ "#include \n"; "#include \n" ]; + if !Config.with_auto_annot then + output_to_oc oc [ "#include \n" ]; + output_to_oc oc [ "#include \n" ]; output_to_oc oc cn_header_decls_list; output_to_oc oc diff --git a/lib/fulminate/fulminate.mli b/lib/fulminate/fulminate.mli index 7570986c6..5951437b5 100644 --- a/lib/fulminate/fulminate.mli +++ b/lib/fulminate/fulminate.mli @@ -5,6 +5,7 @@ module Internal = Internal module Ownership = Ownership module Records = Records module Utils = Utils +module Config = Config val get_instrumented_filename : string -> string diff --git a/lib/fulminate/internal.ml b/lib/fulminate/internal.ml index dc08d3414..b9bd33dd3 100644 --- a/lib/fulminate/internal.ml +++ b/lib/fulminate/internal.ml @@ -130,9 +130,8 @@ let generate_c_loop_invariants ail_loop_decls in let ail_loop_close_block_injs = - List.map - (fun (loc, _) -> (get_end_loc loc, [ "} \nclear_focus ();" ])) - ail_loop_decls + let close_token = if !Config.with_auto_annot then "}\nclear_focus ();" else "}" in + List.map (fun (loc, _) -> (get_end_loc loc, [ close_token ])) ail_loop_decls in ail_cond_injs @ ail_loop_decl_injs @ ail_loop_close_block_injs) diff --git a/lib/fulminate/ownership.ml b/lib/fulminate/ownership.ml index 72fe58f27..032933c9f 100644 --- a/lib/fulminate/ownership.ml +++ b/lib/fulminate/ownership.ml @@ -89,14 +89,17 @@ let get_ownership_global_init_stats let cn_initialise_focus_context_fcall = mk_expr A.(AilEcall (mk_expr (AilEident (Sym.fresh "initialise_focus_context")), [])) in - List.map - (fun e -> A.(AilSexpr e)) - (bump_config_calls - @ [ cn_ghost_state_init_fcall; - cn_ghost_stack_depth_init_fcall; - cn_ghost_arg_array_alloc_fcall; - cn_initialise_focus_context_fcall - ]) + let fns = + if !Config.with_auto_annot then + [ cn_ghost_state_init_fcall; + cn_ghost_stack_depth_init_fcall; + cn_ghost_arg_array_alloc_fcall; + cn_initialise_focus_context_fcall + ] + else + [ cn_ghost_state_init_fcall; cn_ghost_stack_depth_init_fcall ] + in + List.map (fun e -> A.(AilSexpr e)) (bump_config_calls @ fns) let generate_c_local_cn_addr_var sym = From 3b55f7464e7ab2d94bff1a2cf346032df0749ea5 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 18 Aug 2025 16:31:25 +0100 Subject: [PATCH 19/38] Fix bugs --- lib/fulminate/cn_to_ail.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/fulminate/cn_to_ail.ml b/lib/fulminate/cn_to_ail.ml index 837165b57..7a3ae6b75 100644 --- a/lib/fulminate/cn_to_ail.ml +++ b/lib/fulminate/cn_to_ail.ml @@ -3231,7 +3231,8 @@ let cn_to_ail_resource let stmts = [ start_assign; while_loop ] in let stmts = match (iter_res_call_stmt_opt, spec_mode_opt) with - | Some stmt, Some Pre when !Config.with_auto_annot -> stmt :: stmts + | (Some stmt, Some Pre | Some stmt, Some Loop) when !Config.with_auto_annot -> + stmt :: stmts | _ -> stmts in let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in @@ -3291,7 +3292,8 @@ let cn_to_ail_resource let stmts = [ start_assign; while_loop ] in let stmts = match (iter_res_call_stmt_opt, spec_mode_opt) with - | Some stmt, Some Pre when !Config.with_auto_annot -> stmt :: stmts + | (Some stmt, Some Pre | Some stmt, Some Loop) when !Config.with_auto_annot -> + stmt :: stmts | _ -> stmts in let ail_block = A.(AilSblock ([ start_binding ], List.map mk_stmt stmts)) in @@ -4341,7 +4343,7 @@ let cn_to_ail_loop_inv (* reset the current focus context *) let pop_focus_context_fn_call = A.AilSexpr - (mk_expr (AilEcall (mk_expr (AilEident (Sym.fresh "push_focus_context")), []))) + (mk_expr (AilEcall (mk_expr (AilEident (Sym.fresh "pop_focus_context")), []))) in let push_focus_context_fn_call = A.AilSexpr From 416761226877552a642f0a58bda4829f79f44d52 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 18 Aug 2025 17:32:40 +0100 Subject: [PATCH 20/38] Log to a file instead of stdout --- lib/autoannot/autoannot.ml | 14 +++ lib/autoannot/autoannot.mli | 12 +++ lib/fulminate/fulminate.ml | 2 +- lib/fulminate/internal.ml | 14 +++ lib/fulminate/ownership.ml | 12 ++- .../libcn/include/cn-autoannot/auto_annot.h | 95 +++++++++++++++++++ .../libcn/include/cn-autoannot/focus_ctx.h | 65 ------------- runtime/libcn/include/cn-executable/utils.h | 19 ---- runtime/libcn/include/dune | 2 +- runtime/libcn/lib/dune | 6 +- runtime/libcn/src/cn-autoannot/auto_annot.c | 21 ++++ runtime/libcn/src/cn-autoannot/focus_ctx.c | 6 +- runtime/libcn/test/autoannot/focus.cpp | 2 +- 13 files changed, 175 insertions(+), 95 deletions(-) create mode 100644 lib/autoannot/autoannot.ml create mode 100644 lib/autoannot/autoannot.mli create mode 100644 runtime/libcn/include/cn-autoannot/auto_annot.h delete mode 100644 runtime/libcn/include/cn-autoannot/focus_ctx.h create mode 100644 runtime/libcn/src/cn-autoannot/auto_annot.c diff --git a/lib/autoannot/autoannot.ml b/lib/autoannot/autoannot.ml new file mode 100644 index 000000000..9e47a9e1d --- /dev/null +++ b/lib/autoannot/autoannot.ml @@ -0,0 +1,14 @@ +module CF = Cerb_frontend +module A = CF.AilSyntax + +let log_filename = ref "cn_auto_annot.log" + +let run_autoannot + ~_output_dir + ~_filename + (_cabs_tunit : CF.Cabs.translation_unit) + (_sigma : Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.sigma) + (_prog5 : unit Mucore.file) + : int + = + 0 diff --git a/lib/autoannot/autoannot.mli b/lib/autoannot/autoannot.mli new file mode 100644 index 000000000..e35d9ae86 --- /dev/null +++ b/lib/autoannot/autoannot.mli @@ -0,0 +1,12 @@ +module CF = Cerb_frontend +module A = CF.AilSyntax + +val log_filename : string ref + +val run_autoannot + : _output_dir:string -> + _filename:string -> + CF.Cabs.translation_unit -> + Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.sigma -> + unit Mucore.file -> + int diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index bad5353c3..fb2631b9e 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -924,7 +924,7 @@ let main let oc = Stdlib.open_out out_filename in output_to_oc oc [ "#define __CN_INSTRUMENT\n"; "#include \n" ]; if !Config.with_auto_annot then - output_to_oc oc [ "#include \n" ]; + output_to_oc oc [ "#include \n" ]; output_to_oc oc [ "#include \n" ]; output_to_oc oc cn_header_decls_list; output_to_oc diff --git a/lib/fulminate/internal.ml b/lib/fulminate/internal.ml index b9bd33dd3..b5e6351fc 100644 --- a/lib/fulminate/internal.ml +++ b/lib/fulminate/internal.ml @@ -654,6 +654,13 @@ let has_main (sigm : CF.GenTypes.genTypeCategory CF.AilSyntax.sigma) = List.non_empty (get_main sigm) +let finalize_auto_annot () = + let cn_finalize_auto_annot_fcall = + mk_expr A.(AilEcall (mk_expr (AilEident (Sym.fresh "finalize_auto_annot")), [])) + in + A.(AilSexpr cn_finalize_auto_annot_fcall) + + let generate_global_assignments ?(exec_c_locs_mode = false) ?(experimental_ownership_stack_mode = false) @@ -714,6 +721,13 @@ let generate_global_assignments (mk_expr (AilEcall (mk_expr (AilEident (Sym.fresh free_ghost_array_fn_str)), [])))) in + let global_unmapping_stmts_ = + if !Config.with_auto_annot then ( + let finalize_stmt = finalize_auto_annot () in + finalize_stmt :: global_unmapping_stmts_) + else + global_unmapping_stmts_ + in let global_unmapping_str = generate_ail_stat_strs ([], global_unmapping_stmts_ @ [ free_ghost_array_decl ]) in diff --git a/lib/fulminate/ownership.ml b/lib/fulminate/ownership.ml index 032933c9f..230c45f8f 100644 --- a/lib/fulminate/ownership.ml +++ b/lib/fulminate/ownership.ml @@ -86,15 +86,21 @@ let get_ownership_global_init_stats (ConstantInteger (IConstant (Z.of_int ghost_array_size, Decimal, None)))) ] )) in - let cn_initialise_focus_context_fcall = - mk_expr A.(AilEcall (mk_expr (AilEident (Sym.fresh "initialise_focus_context")), [])) + let log_filename = + mk_expr (A.AilEstr (None, [ (Cerb_location.unknown, [ !Autoannot.log_filename ]) ])) + in + let cn_initialize_auto_annot_fcall = + mk_expr + A.( + AilEcall + (mk_expr (AilEident (Sym.fresh "initialize_auto_annot")), [ log_filename ])) in let fns = if !Config.with_auto_annot then [ cn_ghost_state_init_fcall; cn_ghost_stack_depth_init_fcall; cn_ghost_arg_array_alloc_fcall; - cn_initialise_focus_context_fcall + cn_initialize_auto_annot_fcall ] else [ cn_ghost_state_init_fcall; cn_ghost_stack_depth_init_fcall ] diff --git a/runtime/libcn/include/cn-autoannot/auto_annot.h b/runtime/libcn/include/cn-autoannot/auto_annot.h new file mode 100644 index 000000000..08cefc4e1 --- /dev/null +++ b/runtime/libcn/include/cn-autoannot/auto_annot.h @@ -0,0 +1,95 @@ +#ifndef FOCUS_CTX_H +#define FOCUS_CTX_H + +#include +#include +#include + + +#ifdef __cplusplus +extern "C" { +#endif + +typedef const char *type_sig; + +// Defined in cn-autoannot/auto_annot.c +extern FILE *auto_annot_log_file; + +#define cn_auto_annot_printf(...) \ + fprintf(auto_annot_log_file, __VA_ARGS__) + +// Wrapper for cn values +#define CN_INSERT_ITER_RES(base, start, end, size, sig) \ + insert_iter_res((uint64_t)base->ptr, start->val, end->val, size, sig) + +#define CN_INSERT_FOCUS(index, sig) insert_focus(index->val, sig) + +#define CN_LOAD_ANNOT(LV, FMT, ...) \ + ({ \ + typeof(LV) *__tmp = &(LV); \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) \ + cn_auto_annot_printf(FMT, ##__VA_ARGS__); \ + CN_LOAD(LV); \ + }) + +#define CN_STORE_OP_ANNOT(LV, op, X, FMT, ...) \ + ({ \ + typeof(LV) *__tmp; \ + __tmp = &(LV); \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) \ + cn_auto_annot_printf(FMT, ##__VA_ARGS__); \ + CN_STORE_OP(LV, op, X); \ + }) + +#define CN_STORE_ANNOT(LV, X, FMT, ...) CN_STORE_OP_ANNOT(LV, , X, FMT, ##__VA_ARGS__) + +void initialize_auto_annot(const char *log_file); +void finalize_auto_annot(void); + +// Limitation: we only consider contiguous iter ress. +struct iter_res { + uint64_t ptr; + // contiguous indices (closed interval) + uint64_t start; + uint64_t end; + // step + uint64_t size; + // type signature + type_sig sig; +}; + +typedef struct iter_res_set { + struct iter_res res; + struct iter_res_set *next; +} iter_res_set; + +struct focus_info { + int64_t index; + type_sig sig; +}; + +typedef struct focus_set { + struct focus_info info; + struct focus_set *next; +} focus_set; + +struct focus_context { + focus_set *indices; + iter_res_set *iter_ress; + struct focus_context *prev; +}; + +void initialise_focus_context(); +void push_focus_context(void); +void pop_focus_context(void); +void clear_focus(void); +void insert_focus(int64_t index, type_sig sig); +void insert_iter_res( + uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig); + int needs_focus(uint64_t address, uint64_t size); + +#ifdef __cplusplus +} +#endif + +#endif // FOCUS_CTX_H diff --git a/runtime/libcn/include/cn-autoannot/focus_ctx.h b/runtime/libcn/include/cn-autoannot/focus_ctx.h deleted file mode 100644 index fbbc6bd73..000000000 --- a/runtime/libcn/include/cn-autoannot/focus_ctx.h +++ /dev/null @@ -1,65 +0,0 @@ -#ifndef FOCUS_CTX_H -#define FOCUS_CTX_H - -#include - -#ifdef __cplusplus -extern "C" { -#endif - -typedef const char *type_sig; - -// Wrapper for cn values -#define CN_INSERT_ITER_RES(base, start, end, size, sig) \ - insert_iter_res((uint64_t)base->ptr, start->val, end->val, size, sig) - -#define CN_INSERT_FOCUS(index, sig) insert_focus(index->val, sig) - - -// Limitation: we only consider contiguous iter ress. -struct iter_res { - uint64_t ptr; - // contiguous indices (closed interval) - uint64_t start; - uint64_t end; - // step - uint64_t size; - // type signature - type_sig sig; -}; - -typedef struct iter_res_set { - struct iter_res res; - struct iter_res_set *next; -} iter_res_set; - -struct focus_info { - int64_t index; - type_sig sig; -}; - -typedef struct focus_set { - struct focus_info info; - struct focus_set *next; -} focus_set; - -struct focus_context { - focus_set *indices; - iter_res_set *iter_ress; - struct focus_context *prev; -}; - -void initialise_focus_context(void); -void push_focus_context(void); -void pop_focus_context(void); -void clear_focus(void); -void insert_focus(int64_t index, type_sig sig); -void insert_iter_res( - uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig); - int needs_focus(uint64_t address, uint64_t size); - -#ifdef __cplusplus -} -#endif - -#endif // FOCUS_CTX_H diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index a27e89723..39ae8e662 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -628,14 +628,6 @@ static inline void cn_postfix(void* ptr, size_t size) { *__tmp; \ }) -#define CN_LOAD_ANNOT(LV, FMT, ...) \ - ({ \ - typeof(LV) *__tmp = &(LV); \ - if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) \ - cn_printf(CN_LOGGING_ERROR, FMT, ##__VA_ARGS__); \ - CN_LOAD(LV); \ - }) - #define CN_STORE_OP(LV, op, X) \ ({ \ typeof(LV)* __tmp; \ @@ -648,17 +640,6 @@ static inline void cn_postfix(void* ptr, size_t size) { #define CN_STORE(LV, X) CN_STORE_OP(LV, , X) -#define CN_STORE_OP_ANNOT(LV, op, X, FMT, ...) \ - ({ \ - typeof(LV) *__tmp; \ - __tmp = &(LV); \ - if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) \ - cn_printf(CN_LOGGING_ERROR, FMT, ##__VA_ARGS__); \ - CN_STORE_OP(LV, op, X); \ - }) - -#define CN_STORE_ANNOT(LV, X, FMT, ...) CN_STORE_OP_ANNOT(LV, , X, FMT, ##__VA_ARGS__) - #define CN_POSTFIX(LV, OP) \ ({ \ typeof(LV)* __tmp; \ diff --git a/runtime/libcn/include/dune b/runtime/libcn/include/dune index 15795fc21..70e2f6a2b 100644 --- a/runtime/libcn/include/dune +++ b/runtime/libcn/include/dune @@ -21,7 +21,7 @@ (cn-executable/cerb_types.h as runtime/include/cn-executable/cerb_types.h) (cn-executable/stack.h as runtime/include/cn-executable/stack.h) ; AutoAnnot - (cn-autoannot/focus_ctx.h as runtime/include/cn-autoannot/focus_ctx.h) + (cn-autoannot/auto_annot.h as runtime/include/cn-autoannot/auto_annot.h) ; Bennet (bennet/prelude.h as runtime/include/bennet/prelude.h) (bennet/dsl/arbitrary.h as runtime/include/bennet/dsl/arbitrary.h) diff --git a/runtime/libcn/lib/dune b/runtime/libcn/lib/dune index 03d70aa43..3dc95f390 100644 --- a/runtime/libcn/lib/dune +++ b/runtime/libcn/lib/dune @@ -29,7 +29,8 @@ (glob_files ../include/cn-autoannot/*.h)) (:src (glob_files ../src/cn-executable/*.c) - (file ../src/cn-autoannot/focus_ctx.c))) + (file ../src/cn-autoannot/focus_ctx.c) + (file ../src/cn-autoannot/auto_annot.c))) (action (progn (run mkdir -p cn-executable) @@ -45,7 +46,8 @@ cn-executable/hash_table.o cn-executable/rmap.o cn-executable/utils.o - cn-executable/focus_ctx.o)))) + cn-executable/focus_ctx.o + cn-executable/auto_annot.o)))) (rule (target libbennet.a) diff --git a/runtime/libcn/src/cn-autoannot/auto_annot.c b/runtime/libcn/src/cn-autoannot/auto_annot.c new file mode 100644 index 000000000..f7183f1e0 --- /dev/null +++ b/runtime/libcn/src/cn-autoannot/auto_annot.c @@ -0,0 +1,21 @@ +#include +#include +#include + +// Single definition of the global log file pointer +FILE *auto_annot_log_file = NULL; + +//void initialise_focus_context(); + +void initialize_auto_annot(const char *log_file) { + auto_annot_log_file = fopen(log_file, "a"); + if (auto_annot_log_file == NULL) { + cn_printf(CN_LOGGING_ERROR, "Failed to open log file: %s\n", log_file); + exit(EXIT_FAILURE); + } + initialise_focus_context(); +} + +void finalize_auto_annot() { + fclose(auto_annot_log_file); +} diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index c614113c5..c5bd7931f 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -1,4 +1,4 @@ -#include +#include #include #include @@ -11,7 +11,7 @@ #include #include -#include +#include // Note(HK): // we don't have to care about the difference between Owned/Block here @@ -29,7 +29,7 @@ void push_focus_context(void) { cn_focus_global_context = new_context; } -void initialise_focus_context(void) { +void initialise_focus_context() { push_focus_context(); } diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp index fb1d4f9b8..32c986abe 100644 --- a/runtime/libcn/test/autoannot/focus.cpp +++ b/runtime/libcn/test/autoannot/focus.cpp @@ -1,4 +1,4 @@ -#include +#include #include class LibAutoAnnot : public ::testing::Test { From c3d24c7e80ff626412c891f254a6ff7e48097be8 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 18 Aug 2025 18:21:07 +0100 Subject: [PATCH 21/38] Integrate bennet with autoannot --- bin/{autoAnnot.ml => annot.ml} | 9 ++-- bin/main.ml | 4 +- bin/test.ml | 3 +- .../autoannot.ml => autoAnnot/autoAnnot.ml} | 4 ++ .../autoannot.mli => autoAnnot/autoAnnot.mli} | 2 + lib/fulminate/ownership.ml | 2 +- lib/testGeneration/testGenConfig.ml | 8 ++- lib/testGeneration/testGenConfig.mli | 5 +- lib/testGeneration/testGeneration.ml | 51 ++++++++++++------- 9 files changed, 59 insertions(+), 29 deletions(-) rename bin/{autoAnnot.ml => annot.ml} (98%) rename lib/{autoannot/autoannot.ml => autoAnnot/autoAnnot.ml} (76%) rename lib/{autoannot/autoannot.mli => autoAnnot/autoAnnot.mli} (87%) diff --git a/bin/autoAnnot.ml b/bin/annot.ml similarity index 98% rename from bin/autoAnnot.ml rename to bin/annot.ml index ba2049e47..255392fa1 100644 --- a/bin/autoAnnot.ml +++ b/bin/annot.ml @@ -81,6 +81,8 @@ let run_auto_annot let basefile = Filename.basename filename in let pp_file = Filename.temp_file "cn_" basefile in let out_file = Fulminate.get_instrumented_filename basefile in + let log_file = AutoAnnot.get_log_filename basefile in + AutoAnnot.log_filename := log_file; Common.with_well_formedness_check (* CLI arguments *) ~filename ~cc @@ -135,7 +137,8 @@ let run_auto_annot output_tyche; print_size_info; print_backtrack_info; - print_satisfaction_info + print_satisfaction_info; + with_auto_annot = true } in TestGeneration.set_config config; @@ -157,8 +160,8 @@ let run_auto_annot (try Fulminate.main ~without_ownership_checking - ~without_loop_invariants:true - ~with_loop_leak_checks:false + ~without_loop_invariants:false + ~with_loop_leak_checks:true ~with_testing:true filename cc diff --git a/bin/main.ml b/bin/main.ml index 217085e7c..73f3479aa 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -1,8 +1,6 @@ open Cmdliner -let subcommands = - [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd; AutoAnnot.cmd ] - +let subcommands = [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd; Annot.cmd ] let () = let version_str = Cn_version.git_version ^ " [" ^ Cn_version.git_version_date ^ "]" in diff --git a/bin/test.ml b/bin/test.ml index b60436d00..47843148b 100644 --- a/bin/test.ml +++ b/bin/test.ml @@ -190,7 +190,8 @@ let run_tests max_input_alloc; smt_skew_pointer_order; dsl_log_dir; - lazy_gen + lazy_gen; + with_auto_annot = false } in TestGeneration.set_config config; diff --git a/lib/autoannot/autoannot.ml b/lib/autoAnnot/autoAnnot.ml similarity index 76% rename from lib/autoannot/autoannot.ml rename to lib/autoAnnot/autoAnnot.ml index 9e47a9e1d..d0361c385 100644 --- a/lib/autoannot/autoannot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -3,6 +3,10 @@ module A = CF.AilSyntax let log_filename = ref "cn_auto_annot.log" +let get_log_filename filename = + Filename.(remove_extension (basename filename)) ^ ".autoannot.log" + + let run_autoannot ~_output_dir ~_filename diff --git a/lib/autoannot/autoannot.mli b/lib/autoAnnot/autoAnnot.mli similarity index 87% rename from lib/autoannot/autoannot.mli rename to lib/autoAnnot/autoAnnot.mli index e35d9ae86..30f0a1cfa 100644 --- a/lib/autoannot/autoannot.mli +++ b/lib/autoAnnot/autoAnnot.mli @@ -3,6 +3,8 @@ module A = CF.AilSyntax val log_filename : string ref +val get_log_filename : string -> string + val run_autoannot : _output_dir:string -> _filename:string -> diff --git a/lib/fulminate/ownership.ml b/lib/fulminate/ownership.ml index 230c45f8f..2357e43c1 100644 --- a/lib/fulminate/ownership.ml +++ b/lib/fulminate/ownership.ml @@ -87,7 +87,7 @@ let get_ownership_global_init_stats ] )) in let log_filename = - mk_expr (A.AilEstr (None, [ (Cerb_location.unknown, [ !Autoannot.log_filename ]) ])) + mk_expr (A.AilEstr (None, [ (Cerb_location.unknown, [ !AutoAnnot.log_filename ]) ])) in let cn_initialize_auto_annot_fcall = mk_expr diff --git a/lib/testGeneration/testGenConfig.ml b/lib/testGeneration/testGenConfig.ml index cde742924..a745869e1 100644 --- a/lib/testGeneration/testGenConfig.ml +++ b/lib/testGeneration/testGenConfig.ml @@ -104,7 +104,8 @@ type t = max_input_alloc : int option; smt_skew_pointer_order : bool; dsl_log_dir : string option; - lazy_gen : bool + lazy_gen : bool; + with_auto_annot : bool } let default = @@ -169,7 +170,8 @@ let default = max_input_alloc = None; smt_skew_pointer_order = false; dsl_log_dir = None; - lazy_gen = false + lazy_gen = false; + with_auto_annot = false } @@ -400,3 +402,5 @@ let get_dsl_log_dir () = (Option.get !instance).dsl_log_dir let is_lazy_gen () = (Option.get !instance).lazy_gen let is_specialization_disabled () = (Option.get !instance).disable_specialization + +let with_auto_annot () = (Option.get !instance).with_auto_annot diff --git a/lib/testGeneration/testGenConfig.mli b/lib/testGeneration/testGenConfig.mli index d9a744aa2..c5fd1e299 100644 --- a/lib/testGeneration/testGenConfig.mli +++ b/lib/testGeneration/testGenConfig.mli @@ -104,7 +104,8 @@ type t = max_input_alloc : int option; smt_skew_pointer_order : bool; dsl_log_dir : string option; - lazy_gen : bool + lazy_gen : bool; + with_auto_annot : bool } val default : t @@ -260,3 +261,5 @@ val get_dsl_log_dir : unit -> string option val is_lazy_gen : unit -> bool val is_specialization_disabled : unit -> bool + +val with_auto_annot : unit -> bool diff --git a/lib/testGeneration/testGeneration.ml b/lib/testGeneration/testGeneration.ml index 5cace29ae..c65cbc8c7 100644 --- a/lib/testGeneration/testGeneration.ml +++ b/lib/testGeneration/testGeneration.ml @@ -244,6 +244,10 @@ let compile_test_file "#include \n"; "#include \n" ]; + (if Config.with_auto_annot () then + [ "#include \n" ] + else + []); [ c_struct_decls ]; [ (* (if not (String.equal record_defs "") then "\n/* CN RECORDS */\n\n" else ""); *) (* record_defs; *) @@ -284,6 +288,13 @@ let compile_test_file |> Pp.(separate hardline) in let open Pp in + let initialize_auto_annot, finalize_auto_annot = + if Config.with_auto_annot () then + ( string ("initialize_auto_annot(\"" ^ !AutoAnnot.log_filename ^ "\");") ^^ hardline, + string "finalize_auto_annot();" ^^ hardline ) + else + (string "", string "") + in !^(String.concat " " cn_header_decls_list) ^^ compile_includes ~filename ~generators:(List.non_empty generator_tests) ^^ twice hardline @@ -295,24 +306,28 @@ let compile_test_file ^^ pp_label "Static Wrappers" static_wrappers_defs ^^ pp_label "Constant function tests" constant_tests_defs ^^ pp_label "Generator-based tests" generator_tests_defs - ^^ (!^"int main" - ^^ parens !^"int argc, char* argv[]" - ^/^ braces - (nest - 2 - (hardline - ^^ pp_label - "Allocator Configuration" - (!^"fulm_default_alloc.malloc = std_malloc;" - ^/^ !^"fulm_default_alloc.calloc = std_calloc;" - ^/^ !^"fulm_default_alloc.free = std_free;") - ^^ hardline - ^/^ pp_label - "Test Registration" - (separate_map hardline compile_test all_tests - ^^ twice hardline - ^^ !^"return cn_test_main(argc, argv);")) - ^^ hardline)) + ^^ pp_label + "Main function" + (!^"int main" + ^^ parens !^"int argc, char* argv[]" + ^/^ braces + (nest + 2 + (hardline + ^^ pp_label + "Allocator Configuration" + (!^"fulm_default_alloc.malloc = std_malloc;" + ^/^ !^"fulm_default_alloc.calloc = std_calloc;" + ^/^ !^"fulm_default_alloc.free = std_free;") + ^^ hardline + ^/^ initialize_auto_annot + ^^ separate_map hardline compile_test all_tests + ^^ twice hardline + ^^ !^"int cn_test_main_ret = cn_test_main(argc, argv);" + ^^ hardline + ^^ finalize_auto_annot + ^^ !^"return cn_test_main_ret;") + ^^ hardline)) ^^ hardline ^^ !^(String.concat " " From 0356b29762bd77fd61d99260e5952919788d73f1 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 18 Aug 2025 18:27:31 +0100 Subject: [PATCH 22/38] Clear log file everytime --- bin/annot.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/bin/annot.ml b/bin/annot.ml index 255392fa1..dec79a82b 100644 --- a/bin/annot.ml +++ b/bin/annot.ml @@ -82,6 +82,13 @@ let run_auto_annot let pp_file = Filename.temp_file "cn_" basefile in let out_file = Fulminate.get_instrumented_filename basefile in let log_file = AutoAnnot.get_log_filename basefile in + (* Clear the log file if it already exists *) + (try + if Sys.file_exists log_file then ( + let oc = open_out_gen [ Open_wronly; Open_creat; Open_trunc ] 0o644 log_file in + close_out oc + ) + with _ -> ()); AutoAnnot.log_filename := log_file; Common.with_well_formedness_check (* CLI arguments *) ~filename From 5ef815745ff6afbc69da282e7167f816557ae2a1 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 18 Aug 2025 18:57:48 +0100 Subject: [PATCH 23/38] Add the CSV parser --- lib/autoAnnot/autoAnnot.ml | 90 +++++++++++++++++++++++++++++++++---- lib/autoAnnot/autoAnnot.mli | 8 +--- 2 files changed, 82 insertions(+), 16 deletions(-) diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml index d0361c385..67c6bba5d 100644 --- a/lib/autoAnnot/autoAnnot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -7,12 +7,84 @@ let get_log_filename filename = Filename.(remove_extension (basename filename)) ^ ".autoannot.log" -let run_autoannot - ~_output_dir - ~_filename - (_cabs_tunit : CF.Cabs.translation_unit) - (_sigma : Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.sigma) - (_prog5 : unit Mucore.file) - : int - = - 0 +let trim (s : string) : string = + let is_space = function ' ' | '\t' | '\r' | '\n' -> true | _ -> false in + let len = String.length s in + let i = ref 0 in + let j = ref (len - 1) in + while !i < len && is_space s.[!i] do + incr i + done; + while !j >= !i && is_space s.[!j] do + decr j + done; + if !i > !j then "" else String.sub s !i (!j - !i + 1) + + +type assignment = + { accessor : string; + value : int + } + +type focus = + { filename : string; + line : int; + assignments : assignment list + } + +type annot = Focus of focus + +let parse (log_file : string) : annot list = + (* Open the file *) + let ic = open_in log_file in + let prefix = "[auto annot (focus)]" in + let split_and_trim ch s = String.split_on_char ch s |> List.map trim in + let parse_line (line : string) : annot option = + if not (String.starts_with ~prefix line) then + None + else ( + let rest = + String.sub line (String.length prefix) (String.length line - String.length prefix) + |> trim + in + match split_and_trim ',' rest |> List.filter (fun s -> not (String.equal s "")) with + | [] -> None + | loc :: assigns_parts -> + (match split_and_trim ':' loc with + | filename :: line_str :: _ -> + (match int_of_string_opt line_str with + | None -> None + | Some line -> + let assignments = + assigns_parts + |> List.filter_map (fun p -> + match String.split_on_char '=' p |> List.map trim with + | [ key; vstr ] when not (String.equal key "") -> + (match int_of_string_opt vstr with + | Some v -> Some { accessor = key; value = v } + | None -> None) + | _ -> None) + in + Some (Focus { filename; line; assignments })) + | _ -> None)) + in + let rec loop res = + match input_line ic with + | line -> + let res = match parse_line line with None -> res | Some f -> f :: res in + loop res + | exception End_of_file -> res + in + let res = + try loop [] with + | e -> + close_in_noerr ic; + raise e + in + close_in ic; + res + + +let run_autoannot (log_file : string) : unit = + let _data = parse log_file in + () diff --git a/lib/autoAnnot/autoAnnot.mli b/lib/autoAnnot/autoAnnot.mli index 30f0a1cfa..86e387b71 100644 --- a/lib/autoAnnot/autoAnnot.mli +++ b/lib/autoAnnot/autoAnnot.mli @@ -5,10 +5,4 @@ val log_filename : string ref val get_log_filename : string -> string -val run_autoannot - : _output_dir:string -> - _filename:string -> - CF.Cabs.translation_unit -> - Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.sigma -> - unit Mucore.file -> - int +val run_autoannot : string -> unit From 03f99cbcb780cadf8a5cd91a9ba8be07996090e4 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Tue, 19 Aug 2025 00:21:43 +0100 Subject: [PATCH 24/38] parse and group --- bin/annot.ml | 39 ++++++++++++++----- lib/autoAnnot/autoAnnot.ml | 78 +++++++++++++++++++++++++++++++++++++- 2 files changed, 106 insertions(+), 11 deletions(-) diff --git a/bin/annot.ml b/bin/annot.ml index dec79a82b..84674b42e 100644 --- a/bin/annot.ml +++ b/bin/annot.ml @@ -86,9 +86,9 @@ let run_auto_annot (try if Sys.file_exists log_file then ( let oc = open_out_gen [ Open_wronly; Open_creat; Open_trunc ] 0o644 log_file in - close_out oc - ) - with _ -> ()); + close_out oc) + with + | _ -> ()); AutoAnnot.log_filename := log_file; Common.with_well_formedness_check (* CLI arguments *) ~filename @@ -194,12 +194,33 @@ let run_auto_annot | e -> Common.handle_error_with_user_guidance ~label:"CN-Test-Gen" e); if not dont_run then ( Cerb_debug.maybe_close_csv_timing_file (); - match build_tool with - | Bash -> - Unix.execv (Filename.concat output_dir "run_tests.sh") (Array.of_list []) - | Make -> - Unix.chdir output_dir; - Unix.execvp "make" (Array.of_list [ "make" ])); + Pp.(debug 10 (lazy (item "wait for auto-annotation" (string log_file)))); + (* Run tests as a child process and wait, so we can continue afterwards *) + let status = + match build_tool with + | Bash -> + let prog = Filename.concat output_dir "run_tests.sh" in + let pid = + Unix.create_process prog [| prog |] Unix.stdin Unix.stdout Unix.stderr + in + snd (Unix.waitpid [] pid) + | Make -> + let pid = + Unix.create_process + "make" + [| "make"; "-C"; output_dir |] + Unix.stdin + Unix.stdout + Unix.stderr + in + snd (Unix.waitpid [] pid) + in + match status with + | Unix.WEXITED 0 -> () + | Unix.WEXITED n -> Pp.(debug 5 (lazy (item "Test runner exit code" (int n)))) + | Unix.WSIGNALED n -> Pp.(debug 5 (lazy (item "Test runner signaled" (int n)))) + | Unix.WSTOPPED n -> Pp.(debug 5 (lazy (item "Test runner stopped" (int n))))); + AutoAnnot.run_autoannot (Filename.concat output_dir log_file); Result.ok ()) diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml index 67c6bba5d..d7db8d11d 100644 --- a/lib/autoAnnot/autoAnnot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -34,6 +34,78 @@ type focus = type annot = Focus of focus +let generate_focus_annot_aux filename line assignments_list : unit = + Pp.( + debug + 10 + (lazy + (item + "Generating annotations" + (string filename ^^ string ":" ^^ (line |> string_of_int |> string))))); + match assignments_list with + | [] -> () + | first :: rest -> + let variables = + first + |> List.map (fun (a : assignment) -> a.accessor) + |> List.sort_uniq String.compare + in + (* Sanity check: all occurrences have the same variable set *) + let env_vars (env : assignment list) = + env + |> List.map (fun (a : assignment) -> a.accessor) + |> List.sort_uniq String.compare + in + let all_same_vars = + List.for_all + (fun env -> List.for_all2 (fun x y -> String.equal x y) (env_vars env) variables) + rest + in + if not all_same_vars then + Pp.( + debug + 5 + (lazy + (item + "AutoAnnot: inconsistent environments" + (string (filename ^ ":" ^ string_of_int line))))) + else ( + (* Build values per variable across occurrences *) + let tbl : (string, int list) Hashtbl.t = Hashtbl.create (List.length variables) in + List.iter (fun v -> Hashtbl.replace tbl v []) variables; + let add_value v n = + let prev = match Hashtbl.find_opt tbl v with Some xs -> xs | None -> [] in + Hashtbl.replace tbl v (prev @ [ n ]) + in + let lookup_value v (env : assignment list) = + match List.find_opt (fun (a : assignment) -> String.equal a.accessor v) env with + | Some a -> Some a.value + | None -> None + in + List.iter + (fun env -> + List.iter + (fun v -> + match lookup_value v env with Some n -> add_value v n | None -> ()) + variables) + assignments_list) + + +let generate_focus_annot (annots : focus list) : unit = + let tbl : (string * int, assignment list list) Hashtbl.t = Hashtbl.create 16 in + let add filename line assigns = + let key = (filename, line) in + let prev = match Hashtbl.find_opt tbl key with Some xs -> xs | None -> [] in + Hashtbl.replace tbl key (prev @ [ assigns ]) + in + List.iter + (function { filename; line; assignments } -> add filename line assignments) + annots; + Hashtbl.iter + (fun (filename, line) assigns -> generate_focus_annot_aux filename line assigns) + tbl + + let parse (log_file : string) : annot list = (* Open the file *) let ic = open_in log_file in @@ -86,5 +158,7 @@ let parse (log_file : string) : annot list = let run_autoannot (log_file : string) : unit = - let _data = parse log_file in - () + Pp.(debug 10 (lazy (item "Running auto-annotation" (string log_file)))); + let data = parse log_file in + let focus_annots = data |> List.filter_map (function Focus f -> Some f) in + generate_focus_annot focus_annots From f69f4846749fb708448b2d1572e586bfec753e17 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Tue, 19 Aug 2025 17:05:23 +0100 Subject: [PATCH 25/38] refactor --- lib/autoAnnot/autoAnnot.ml | 87 ++++++++++---------------------------- 1 file changed, 23 insertions(+), 64 deletions(-) diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml index d7db8d11d..c68d245b0 100644 --- a/lib/autoAnnot/autoAnnot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -7,20 +7,6 @@ let get_log_filename filename = Filename.(remove_extension (basename filename)) ^ ".autoannot.log" -let trim (s : string) : string = - let is_space = function ' ' | '\t' | '\r' | '\n' -> true | _ -> false in - let len = String.length s in - let i = ref 0 in - let j = ref (len - 1) in - while !i < len && is_space s.[!i] do - incr i - done; - while !j >= !i && is_space s.[!j] do - decr j - done; - if !i > !j then "" else String.sub s !i (!j - !i + 1) - - type assignment = { accessor : string; value : int @@ -42,53 +28,26 @@ let generate_focus_annot_aux filename line assignments_list : unit = (item "Generating annotations" (string filename ^^ string ":" ^^ (line |> string_of_int |> string))))); - match assignments_list with - | [] -> () - | first :: rest -> - let variables = - first - |> List.map (fun (a : assignment) -> a.accessor) - |> List.sort_uniq String.compare - in - (* Sanity check: all occurrences have the same variable set *) - let env_vars (env : assignment list) = - env - |> List.map (fun (a : assignment) -> a.accessor) - |> List.sort_uniq String.compare - in - let all_same_vars = - List.for_all - (fun env -> List.for_all2 (fun x y -> String.equal x y) (env_vars env) variables) - rest - in - if not all_same_vars then - Pp.( - debug - 5 - (lazy - (item - "AutoAnnot: inconsistent environments" - (string (filename ^ ":" ^ string_of_int line))))) - else ( - (* Build values per variable across occurrences *) - let tbl : (string, int list) Hashtbl.t = Hashtbl.create (List.length variables) in - List.iter (fun v -> Hashtbl.replace tbl v []) variables; - let add_value v n = - let prev = match Hashtbl.find_opt tbl v with Some xs -> xs | None -> [] in - Hashtbl.replace tbl v (prev @ [ n ]) - in - let lookup_value v (env : assignment list) = - match List.find_opt (fun (a : assignment) -> String.equal a.accessor v) env with - | Some a -> Some a.value - | None -> None - in - List.iter - (fun env -> - List.iter - (fun v -> - match lookup_value v env with Some n -> add_value v n | None -> ()) - variables) - assignments_list) + let first = List.hd assignments_list in + let variables = + first + |> List.map (fun (a : assignment) -> a.accessor) + |> List.sort_uniq String.compare + in + (* Sanity check: all occurrences have the same variable set *) + let all_unique = + List.for_all (fun x -> not (List.exists (String.equal x) variables)) variables + in + if not all_unique then + failwith "AutoAnnot: inconsistent environments"; + (* Build values per variable across occurrences *) + let tbl : (string, int list) Hashtbl.t = Hashtbl.create (List.length variables) in + List.iter (fun v -> Hashtbl.replace tbl v []) variables; + let add_value v n = Hashtbl.replace tbl v (n :: Hashtbl.find tbl v) in + let lookup_value v env = (List.find (fun a -> String.equal a.accessor v) env).value in + List.iter + (fun env -> List.iter (fun v -> lookup_value v env |> add_value v) variables) + assignments_list let generate_focus_annot (annots : focus list) : unit = @@ -110,14 +69,14 @@ let parse (log_file : string) : annot list = (* Open the file *) let ic = open_in log_file in let prefix = "[auto annot (focus)]" in - let split_and_trim ch s = String.split_on_char ch s |> List.map trim in + let split_and_trim ch s = String.split_on_char ch s |> List.map String.trim in let parse_line (line : string) : annot option = if not (String.starts_with ~prefix line) then None else ( let rest = String.sub line (String.length prefix) (String.length line - String.length prefix) - |> trim + |> String.trim in match split_and_trim ',' rest |> List.filter (fun s -> not (String.equal s "")) with | [] -> None @@ -130,7 +89,7 @@ let parse (log_file : string) : annot list = let assignments = assigns_parts |> List.filter_map (fun p -> - match String.split_on_char '=' p |> List.map trim with + match String.split_on_char '=' p |> List.map String.trim with | [ key; vstr ] when not (String.equal key "") -> (match int_of_string_opt vstr with | Some v -> Some { accessor = key; value = v } From f928303bd3e6308392b02c8cb0b5bf161bc57e2e Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Tue, 19 Aug 2025 18:42:06 +0100 Subject: [PATCH 26/38] Preliminary optimization --- cn.opam | 1 + lib/autoAnnot/autoAnnot.ml | 96 +++++++++++++++++++++++++++++++++----- lib/dune | 1 + 3 files changed, 87 insertions(+), 11 deletions(-) diff --git a/cn.opam b/cn.opam index 42a225366..c20ace84e 100644 --- a/cn.opam +++ b/cn.opam @@ -25,6 +25,7 @@ depends: [ "ounit2" {with-test} "qcheck" {with-test} "qcheck-ounit" {with-test} + "z3" ] pin-depends: [ ["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#4a18965"] diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml index c68d245b0..64932873b 100644 --- a/lib/autoAnnot/autoAnnot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -34,20 +34,94 @@ let generate_focus_annot_aux filename line assignments_list : unit = |> List.map (fun (a : assignment) -> a.accessor) |> List.sort_uniq String.compare in - (* Sanity check: all occurrences have the same variable set *) + (* Sanity: all occurrences have the same variable set *) let all_unique = - List.for_all (fun x -> not (List.exists (String.equal x) variables)) variables + List.for_all + (fun x -> + List.fold_left + (fun acc y -> if String.equal x y then acc + 1 else acc) + 0 + variables + = 1) + variables in if not all_unique then - failwith "AutoAnnot: inconsistent environments"; - (* Build values per variable across occurrences *) - let tbl : (string, int list) Hashtbl.t = Hashtbl.create (List.length variables) in - List.iter (fun v -> Hashtbl.replace tbl v []) variables; - let add_value v n = Hashtbl.replace tbl v (n :: Hashtbl.find tbl v) in - let lookup_value v env = (List.find (fun a -> String.equal a.accessor v) env).value in - List.iter - (fun env -> List.iter (fun v -> lookup_value v env |> add_value v) variables) - assignments_list + failwith "AutoAnnot: inconsistent environment"; + (* Create a template *) + (* like ax + by + c = 0, and try to find a, b, and c *) + (* For [[x = 1; y = 2]; [ x = 2; y = 4]] *) + (* generate a * 1 + b * 2 + c = 0 /\ a * 2 + b * 4 + c = 0 *) + (* and find a, b, and c that satisfy the above using Z3 Optimize *) + let open Z3 in + let ctx = Z3.mk_context [ ("model", "true") ] in + let opt = Optimize.mk_opt ctx in + let i_k n = Arithmetic.Integer.mk_numeral_i ctx n in + let mk_int name = Arithmetic.Integer.mk_const_s ctx name in + let zero = i_k 0 in + let add = Arithmetic.mk_add ctx in + let mul x y = Arithmetic.mk_mul ctx [ x; y ] in + let neg x = Arithmetic.mk_unary_minus ctx x in + let ge = Arithmetic.mk_ge ctx in + let eq = Boolean.mk_eq ctx in + (* constant *) + let w0 = mk_int "w0" in + (* coefficients *) + let coeffs = List.map (fun v -> (v, mk_int ("w_" ^ v))) variables in + (* For each sample env, assert: w0 + sum(w_v * val_v) = 0 *) + let value_of v (env : assignment list) = + (List.find (fun a -> String.equal a.accessor v) env).value + in + let sum_terms env = + let terms = List.map (fun (v, wv) -> mul wv (i_k (value_of v env))) coeffs in + add (w0 :: terms) + in + List.iter (fun env -> Optimize.add opt [ eq (sum_terms env) zero ]) assignments_list; + (* L1 norm: minimize t_v where t_v >= w_v and t_v >= -w_v*) + let ts = + List.map + (fun (v, wv) -> + let tv = mk_int ("t_" ^ v) in + Optimize.add opt [ ge tv wv; ge tv (neg wv) ]; + tv) + coeffs + in + let objective = add ts in + ignore (Optimize.minimize opt objective : Optimize.handle); + (* Solve and read model *) + match Optimize.check opt with + | Solver.SATISFIABLE -> + let m = Optimize.get_model opt in + let get_int e = + let m = match m with Some m -> m | None -> failwith "No model found" in + match Model.eval m e true with + | None -> 0 + | Some v -> int_of_string (Expr.to_string v) + in + let w0_v = get_int w0 in + let coeff_vals = List.map (fun (v, wv) -> (v, get_int wv)) coeffs in + Pp.( + debug + 10 + (lazy + (item + "AutoAnnot: inferred relation" + (string + ("0 = " + ^ string_of_int w0_v + ^ String.concat + "" + (List.map + (fun (v, c) -> " + (" ^ string_of_int c ^ " * " ^ v ^ ")") + coeff_vals)))))); + () + | Solver.UNSATISFIABLE | Solver.UNKNOWN -> + Pp.( + debug + 5 + (lazy + (item + "AutoAnnot: no relation found" + (string (filename ^ ":" ^ string_of_int line))))) let generate_focus_annot (annots : focus list) : unit = diff --git a/lib/dune b/lib/dune index 9b79569df..da781c008 100644 --- a/lib/dune +++ b/lib/dune @@ -14,6 +14,7 @@ ppx_deriving_yojson.runtime result str + z3 unix yojson) (preprocess From ec8eab8becdcf15acc4c9ab1bcc8d5e64220d840 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Wed, 20 Aug 2025 18:06:43 +0100 Subject: [PATCH 27/38] Add target index to the constraint --- lib/autoAnnot/autoAnnot.ml | 41 ++++++++++++------- lib/fulminate/fulminate.ml | 41 +++++++++++-------- .../libcn/include/cn-autoannot/auto_annot.h | 12 +++--- runtime/libcn/src/cn-autoannot/focus_ctx.c | 5 ++- runtime/libcn/test/autoannot/focus.cpp | 39 ++++++++++-------- 5 files changed, 82 insertions(+), 56 deletions(-) diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml index 64932873b..88b03cdaa 100644 --- a/lib/autoAnnot/autoAnnot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -15,12 +15,19 @@ type assignment = type focus = { filename : string; line : int; + (* TODO: should be int64 *) + target : int; assignments : assignment list } type annot = Focus of focus -let generate_focus_annot_aux filename line assignments_list : unit = +let generate_focus_annot_aux + filename + line + (assignments_list : (int * assignment list) list) + : unit + = Pp.( debug 10 @@ -28,11 +35,9 @@ let generate_focus_annot_aux filename line assignments_list : unit = (item "Generating annotations" (string filename ^^ string ":" ^^ (line |> string_of_int |> string))))); - let first = List.hd assignments_list in + let _, first = List.hd assignments_list in let variables = - first - |> List.map (fun (a : assignment) -> a.accessor) - |> List.sort_uniq String.compare + first |> List.map (fun a -> a.accessor) |> List.sort_uniq String.compare in (* Sanity: all occurrences have the same variable set *) let all_unique = @@ -57,7 +62,6 @@ let generate_focus_annot_aux filename line assignments_list : unit = let opt = Optimize.mk_opt ctx in let i_k n = Arithmetic.Integer.mk_numeral_i ctx n in let mk_int name = Arithmetic.Integer.mk_const_s ctx name in - let zero = i_k 0 in let add = Arithmetic.mk_add ctx in let mul x y = Arithmetic.mk_mul ctx [ x; y ] in let neg x = Arithmetic.mk_unary_minus ctx x in @@ -75,7 +79,9 @@ let generate_focus_annot_aux filename line assignments_list : unit = let terms = List.map (fun (v, wv) -> mul wv (i_k (value_of v env))) coeffs in add (w0 :: terms) in - List.iter (fun env -> Optimize.add opt [ eq (sum_terms env) zero ]) assignments_list; + List.iter + (fun (target, env) -> Optimize.add opt [ eq (sum_terms env) (i_k target) ]) + assignments_list; (* L1 norm: minimize t_v where t_v >= w_v and t_v >= -w_v*) let ts = List.map @@ -125,14 +131,15 @@ let generate_focus_annot_aux filename line assignments_list : unit = let generate_focus_annot (annots : focus list) : unit = - let tbl : (string * int, assignment list list) Hashtbl.t = Hashtbl.create 16 in + let tbl : (string * int, (int * assignment list) list) Hashtbl.t = Hashtbl.create 16 in let add filename line assigns = let key = (filename, line) in let prev = match Hashtbl.find_opt tbl key with Some xs -> xs | None -> [] in Hashtbl.replace tbl key (prev @ [ assigns ]) in List.iter - (function { filename; line; assignments } -> add filename line assignments) + (function + | { filename; line; assignments; target } -> add filename line (target, assignments)) annots; Hashtbl.iter (fun (filename, line) assigns -> generate_focus_annot_aux filename line assigns) @@ -162,15 +169,19 @@ let parse (log_file : string) : annot list = | Some line -> let assignments = assigns_parts - |> List.filter_map (fun p -> + |> List.map (fun p -> match String.split_on_char '=' p |> List.map String.trim with - | [ key; vstr ] when not (String.equal key "") -> + | [ key; vstr ] -> (match int_of_string_opt vstr with - | Some v -> Some { accessor = key; value = v } - | None -> None) - | _ -> None) + | Some v -> { accessor = key; value = v } + | None -> failwith "Invalid assignment value") + | _ -> failwith "ill-formed") in - Some (Focus { filename; line; assignments })) + (* assignments must be non-empty; as the first element is the target*) + let fst = List.hd assignments in + assert (String.equal fst.accessor "!index"); + let assignments = List.tl assignments in + Some (Focus { filename; line; assignments; target = fst.value })) | _ -> None)) in let rec loop res = diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index fb2631b9e..628e8239b 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -221,24 +221,29 @@ let get_symbol = function | _ -> None -let rec gen_env_fmt_printer = function - | [] -> ("", []) - | (sym, ty) :: xs -> - let fmt, args = gen_env_fmt_printer xs in - let open CF.Ctype in - let (Ctype (_, ty)) = ty in - (match ty with - | Basic (Integer b) -> - (match (gen_fmt_for_integer_type b, get_symbol sym) with - | Some f, Some sym -> - let f = Printf.sprintf "%s=%s, " sym f in - (f ^ fmt, sym :: args) - | _ -> (fmt, args)) - | Struct _ -> failwith "unimplemented" - | Basic (Floating _) - | Array _ | Function _ | Void | FunctionNoParams _ | Pointer _ | Atomic _ | Union _ - | Byte -> - (fmt, args)) +let gen_env_fmt_printer x = + let rec aux = function + | [] -> ("", []) + | (sym, ty) :: xs -> + let fmt, args = aux xs in + let open CF.Ctype in + let (Ctype (_, ty)) = ty in + (match ty with + | Basic (Integer b) -> + (match (gen_fmt_for_integer_type b, get_symbol sym) with + | Some f, Some sym -> + let f = Printf.sprintf "%s=%s, " sym f in + (f ^ fmt, sym :: args) + | _ -> (fmt, args)) + | Struct _ -> failwith "unimplemented" + | Basic (Floating _) + | Array _ | Function _ | Void | FunctionNoParams _ | Pointer _ | Atomic _ | Union _ + | Byte -> + (fmt, args)) + in + let fmt, args = aux x in + (* The first element is for the target index, which will be filled in CN_XXX_ANNOT macros *) + ("!index=%%lld, " ^ fmt, args) let memory_accesses_injections ail_prog = diff --git a/runtime/libcn/include/cn-autoannot/auto_annot.h b/runtime/libcn/include/cn-autoannot/auto_annot.h index 08cefc4e1..8b42b1359 100644 --- a/runtime/libcn/include/cn-autoannot/auto_annot.h +++ b/runtime/libcn/include/cn-autoannot/auto_annot.h @@ -27,8 +27,9 @@ extern FILE *auto_annot_log_file; #define CN_LOAD_ANNOT(LV, FMT, ...) \ ({ \ typeof(LV) *__tmp = &(LV); \ - if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) \ - cn_auto_annot_printf(FMT, ##__VA_ARGS__); \ + int64_t index; \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index)) \ + cn_auto_annot_printf(FMT, index, ##__VA_ARGS__); \ CN_LOAD(LV); \ }) @@ -36,8 +37,9 @@ extern FILE *auto_annot_log_file; ({ \ typeof(LV) *__tmp; \ __tmp = &(LV); \ - if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)))) \ - cn_auto_annot_printf(FMT, ##__VA_ARGS__); \ + int64_t index; \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index)) \ + cn_auto_annot_printf(FMT, index, ##__VA_ARGS__); \ CN_STORE_OP(LV, op, X); \ }) @@ -86,7 +88,7 @@ void clear_focus(void); void insert_focus(int64_t index, type_sig sig); void insert_iter_res( uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig); - int needs_focus(uint64_t address, uint64_t size); +int needs_focus(uint64_t address, uint64_t size, int64_t *index_out); #ifdef __cplusplus } diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index c5bd7931f..1f9217153 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -85,7 +85,7 @@ void insert_iter_res(uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, /// (i) is in a iterated resource /// (ii) is not focused /// If (i) and (ii), it needs focus, and returns 1. -int needs_focus(uint64_t address, uint64_t size) { +int needs_focus(uint64_t address, uint64_t size, int64_t *index_out) { assert(cn_focus_global_context != NULL); // (i) search for iterated resource iter_res_set *iter = cn_focus_global_context->iter_ress; @@ -94,7 +94,7 @@ int needs_focus(uint64_t address, uint64_t size) { iter = iter->next; uint64_t start = cur->res.ptr + cur->res.start * cur->res.size; uint64_t end = cur->res.ptr + (cur->res.end + 1) * cur->res.size; - uint64_t offset = address - cur->res.ptr; + int64_t offset = address - cur->res.ptr; if (address < start || address + size > end) { continue; } @@ -115,6 +115,7 @@ int needs_focus(uint64_t address, uint64_t size) { cur_focus = cur_focus->next; } // The index is not focused + *index_out = index; return 1; } // We didn't find any appropriate iterated resource diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp index 32c986abe..d1fc2d345 100644 --- a/runtime/libcn/test/autoannot/focus.cpp +++ b/runtime/libcn/test/autoannot/focus.cpp @@ -9,6 +9,7 @@ class LibAutoAnnot : public ::testing::Test { TEST(LibAutoAnnot, BasicOperations) { initialise_focus_context(); push_focus_context(); + int64_t index = -1; /* let p = 0xcafe000; @@ -18,39 +19,45 @@ TEST(LibAutoAnnot, BasicOperations) { /* focus RW, 1u64; */ insert_focus(1, "unsigned long"); - ASSERT_EQ(needs_focus(0xcafe0000, 8), 1) << "Lack of focus for p[0]"; - ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Focused"; - ASSERT_EQ(needs_focus(0xcafe1000, 8), 0) + ASSERT_EQ(needs_focus(0xcafe0000, 8, &index), 1) << "Lack of focus for p[0]"; + ASSERT_EQ(index, 0) << "Focused index should be 0"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "Focused"; + ASSERT_EQ(needs_focus(0xcafe1000, 8, &index), 0) << "No appropriate resource, so we don't need focus"; clear_focus(); - ASSERT_EQ(needs_focus(0xcafe0008, 8), 1) << "Cleared"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 1) << "Cleared"; + ASSERT_EQ(index, 1) << "Focused index should be 1"; insert_focus(1, "unsigned long"); - ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Focused"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "Focused"; push_focus_context(); insert_iter_res(0xcafe0000, 0, 4, 8, "unsigned long"); insert_iter_res(0x10000000, 1, 4, 8, "unsigned long"); insert_iter_res(0x20000000, 0, 4, 4, "unsigned int"); - ASSERT_EQ(needs_focus(0xcafe0008, 8), 1) << "No focus in the current level"; - ASSERT_EQ(needs_focus(0xcafe0000, 8), 1) << "No focus in the current level"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 1) << "No focus in the current level"; + ASSERT_EQ(index, 1) << "Focused index should be 1"; + ASSERT_EQ(needs_focus(0xcafe0000, 8, &index), 1) << "No focus in the current level"; + ASSERT_EQ(index, 0) << "Focused index should be 0"; insert_focus(1, "unsigned long"); - ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Just focused"; - ASSERT_EQ(needs_focus(0x10000008, 8), 0) << "Just focused"; - ASSERT_EQ(needs_focus(0x20000004, 4), 1) << "Type mismatch"; - ASSERT_EQ(needs_focus(0x10000000, 8), 0) << "Out of the iter_res"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x10000008, 8, &index), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x20000004, 4, &index), 1) << "Type mismatch"; + ASSERT_EQ(index, 1) << "Focused index should be 1"; + ASSERT_EQ(needs_focus(0x10000000, 8, &index), 0) << "Out of the iter_res"; insert_focus(1, "unsigned int"); - ASSERT_EQ(needs_focus(0x20000004, 4), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x20000004, 4, &index), 0) << "Just focused"; pop_focus_context(); // Check if it remembers the context - ASSERT_EQ(needs_focus(0xcafe0000, 8), 1) << "Lack of focus for p[0]"; - ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "Focus has already been annotated"; + ASSERT_EQ(needs_focus(0xcafe0000, 8, &index), 1) << "Lack of focus for p[0]"; + ASSERT_EQ(index, 0) << "Focused index should be 0"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "Focus has already been annotated"; pop_focus_context(); - ASSERT_EQ(needs_focus(0xcafe0000, 8), 0) << "No need for focus"; - ASSERT_EQ(needs_focus(0xcafe0008, 8), 0) << "No need for focus"; + ASSERT_EQ(needs_focus(0xcafe0000, 8, &index), 0) << "No need for focus"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "No need for focus"; } From c5daeebaedcf827a4151f6e406219fef5209cb32 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Wed, 20 Aug 2025 18:12:29 +0100 Subject: [PATCH 28/38] Fix a minor issue --- lib/autoAnnot/autoAnnot.ml | 8 +++----- lib/fulminate/fulminate.ml | 2 +- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml index 88b03cdaa..a7d6d5095 100644 --- a/lib/autoAnnot/autoAnnot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -112,8 +112,7 @@ let generate_focus_annot_aux (item "AutoAnnot: inferred relation" (string - ("0 = " - ^ string_of_int w0_v + (string_of_int w0_v ^ String.concat "" (List.map @@ -172,9 +171,8 @@ let parse (log_file : string) : annot list = |> List.map (fun p -> match String.split_on_char '=' p |> List.map String.trim with | [ key; vstr ] -> - (match int_of_string_opt vstr with - | Some v -> { accessor = key; value = v } - | None -> failwith "Invalid assignment value") + let v = int_of_string vstr in + { accessor = key; value = v } | _ -> failwith "ill-formed") in (* assignments must be non-empty; as the first element is the target*) diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index 628e8239b..7ab243a88 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -243,7 +243,7 @@ let gen_env_fmt_printer x = in let fmt, args = aux x in (* The first element is for the target index, which will be filled in CN_XXX_ANNOT macros *) - ("!index=%%lld, " ^ fmt, args) + ("!index=%lld, " ^ fmt, args) let memory_accesses_injections ail_prog = From 83a34a2581bec3ebfa88c361892d9ae98d0ad8d9 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Wed, 20 Aug 2025 18:27:36 +0100 Subject: [PATCH 29/38] pretty print the inferred index --- lib/autoAnnot/autoAnnot.ml | 32 ++++++++++++++++++-------------- 1 file changed, 18 insertions(+), 14 deletions(-) diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml index a7d6d5095..6df6fdea7 100644 --- a/lib/autoAnnot/autoAnnot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -22,6 +22,23 @@ type focus = type annot = Focus of focus +let print_focus_suggestion filename line w0 coeffs = + let pos = filename ^ ":" ^ string_of_int line in + let body = + List.filter_map + (fun (v, c) -> + match c with 0 -> None | 1 -> Some v | c -> Some (string_of_int c ^ " * " ^ v)) + coeffs + in + let elems = if w0 = 0 then body else string_of_int w0 :: body in + let sum = String.concat " + " elems in + Pp.( + debug + 10 + (lazy + (item "AutoAnnot: suggested annotation" (string pos ^^ string ": " ^^ string sum)))) + + let generate_focus_annot_aux filename line @@ -105,20 +122,7 @@ let generate_focus_annot_aux in let w0_v = get_int w0 in let coeff_vals = List.map (fun (v, wv) -> (v, get_int wv)) coeffs in - Pp.( - debug - 10 - (lazy - (item - "AutoAnnot: inferred relation" - (string - (string_of_int w0_v - ^ String.concat - "" - (List.map - (fun (v, c) -> " + (" ^ string_of_int c ^ " * " ^ v ^ ")") - coeff_vals)))))); - () + print_focus_suggestion filename line w0_v coeff_vals | Solver.UNSATISFIABLE | Solver.UNKNOWN -> Pp.( debug From 142a86dda080fc7d3b01ec6d1149cadb7246928c Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 21 Aug 2025 11:16:43 +0100 Subject: [PATCH 30/38] Show type annotation --- lib/autoAnnot/autoAnnot.ml | 99 ++++++++++--------- lib/fulminate/fulminate.ml | 8 ++ .../libcn/include/cn-autoannot/auto_annot.h | 14 +-- runtime/libcn/src/cn-autoannot/focus_ctx.c | 3 +- runtime/libcn/test/autoannot/focus.cpp | 42 +++++--- 5 files changed, 98 insertions(+), 68 deletions(-) diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml index 6df6fdea7..dab43f6fc 100644 --- a/lib/autoAnnot/autoAnnot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -15,6 +15,8 @@ type assignment = type focus = { filename : string; line : int; + kind : string; + ty : string; (* TODO: should be int64 *) target : int; assignments : assignment list @@ -22,7 +24,7 @@ type focus = type annot = Focus of focus -let print_focus_suggestion filename line w0 coeffs = +let print_focus_suggestion filename line kind ty w0 coeffs = let pos = filename ^ ":" ^ string_of_int line in let body = List.filter_map @@ -30,21 +32,20 @@ let print_focus_suggestion filename line w0 coeffs = match c with 0 -> None | 1 -> Some v | c -> Some (string_of_int c ^ " * " ^ v)) coeffs in + let signature = Printf.sprintf "focus %s<%s>, " kind ty in let elems = if w0 = 0 then body else string_of_int w0 :: body in let sum = String.concat " + " elems in + let annotation = signature ^ sum in Pp.( debug 10 (lazy - (item "AutoAnnot: suggested annotation" (string pos ^^ string ": " ^^ string sum)))) + (item + "AutoAnnot: suggested annotation" + (string pos ^^ string ": " ^^ string annotation)))) -let generate_focus_annot_aux - filename - line - (assignments_list : (int * assignment list) list) - : unit - = +let generate_focus_annot_aux filename line (kind, ty, assignments_list) : unit = Pp.( debug 10 @@ -122,7 +123,7 @@ let generate_focus_annot_aux in let w0_v = get_int w0 in let coeff_vals = List.map (fun (v, wv) -> (v, get_int wv)) coeffs in - print_focus_suggestion filename line w0_v coeff_vals + print_focus_suggestion filename line kind ty w0_v coeff_vals | Solver.UNSATISFIABLE | Solver.UNKNOWN -> Pp.( debug @@ -134,15 +135,23 @@ let generate_focus_annot_aux let generate_focus_annot (annots : focus list) : unit = - let tbl : (string * int, (int * assignment list) list) Hashtbl.t = Hashtbl.create 16 in - let add filename line assigns = + let tbl : (string * int, string * string * (int * assignment list) list) Hashtbl.t = + Hashtbl.create 16 + in + let add filename line assigns kind ty = let key = (filename, line) in - let prev = match Hashtbl.find_opt tbl key with Some xs -> xs | None -> [] in - Hashtbl.replace tbl key (prev @ [ assigns ]) + let prev = + match Hashtbl.find_opt tbl key with + | Some (kind2, ty2, xs) when String.equal kind kind2 && String.equal ty ty2 -> xs + | Some _ -> failwith "inconsistent focus types" + | None -> [] + in + Hashtbl.replace tbl key (kind, ty, prev @ [ assigns ]) in List.iter (function - | { filename; line; assignments; target } -> add filename line (target, assignments)) + | { filename; line; assignments; target; kind; ty } -> + add filename line (target, assignments) kind ty) annots; Hashtbl.iter (fun (filename, line) assigns -> generate_focus_annot_aux filename line assigns) @@ -154,42 +163,42 @@ let parse (log_file : string) : annot list = let ic = open_in log_file in let prefix = "[auto annot (focus)]" in let split_and_trim ch s = String.split_on_char ch s |> List.map String.trim in - let parse_line (line : string) : annot option = + let parse_line (line : string) : annot = if not (String.starts_with ~prefix line) then - None - else ( - let rest = - String.sub line (String.length prefix) (String.length line - String.length prefix) - |> String.trim - in - match split_and_trim ',' rest |> List.filter (fun s -> not (String.equal s "")) with - | [] -> None - | loc :: assigns_parts -> - (match split_and_trim ':' loc with - | filename :: line_str :: _ -> - (match int_of_string_opt line_str with - | None -> None - | Some line -> - let assignments = - assigns_parts - |> List.map (fun p -> - match String.split_on_char '=' p |> List.map String.trim with - | [ key; vstr ] -> - let v = int_of_string vstr in - { accessor = key; value = v } - | _ -> failwith "ill-formed") - in - (* assignments must be non-empty; as the first element is the target*) - let fst = List.hd assignments in - assert (String.equal fst.accessor "!index"); - let assignments = List.tl assignments in - Some (Focus { filename; line; assignments; target = fst.value })) - | _ -> None)) + failwith "ill-formed auto annot line"; + let rest = + String.sub line (String.length prefix) (String.length line - String.length prefix) + |> String.trim + in + match split_and_trim ',' rest |> List.filter (fun s -> not (String.equal s "")) with + | [] -> failwith "ill-formed focus annotation" + | loc :: assigns_parts -> + (match split_and_trim ':' loc with + (* ex: itres.c:46:12-16:RW:signed int *) + | [ filename; line_str; _; kind; ty ] -> + (match int_of_string_opt line_str with + | None -> failwith "ill-formed line number" + | Some line -> + let assignments = + assigns_parts + |> List.map (fun p -> + match String.split_on_char '=' p |> List.map String.trim with + | [ key; vstr ] -> + let v = int_of_string vstr in + { accessor = key; value = v } + | _ -> failwith "ill-formed") + in + (* assignments must be non-empty; as the first element is the target*) + let fst = List.hd assignments in + assert (String.equal fst.accessor "!index"); + let assignments = List.tl assignments in + Focus { filename; line; kind; ty; assignments; target = fst.value }) + | _ -> failwith "ill-formed line") in let rec loop res = match input_line ic with | line -> - let res = match parse_line line with None -> res | Some f -> f :: res in + let res = parse_line line :: res in loop res | exception End_of_file -> res in diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index 7ab243a88..3378a977b 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -286,6 +286,8 @@ let memory_accesses_injections ail_prog = ", \"" ^ "[auto annot (focus)]" ^ pos_info + (* The fmt for type. Filled by CN_XXX_ANNOT *) + ^ ":%s:%s" ^ ", " ^ autoannot_fmt ^ "\"" @@ -309,6 +311,8 @@ let memory_accesses_injections ail_prog = ", \"" ^ "[auto annot (focus)]" ^ pos_info + (* The fmt for type. Filled by CN_XXX_ANNOT *) + ^ ":%s:%s" ^ ", " ^ autoannot_fmt ^ "\"" @@ -338,6 +342,8 @@ let memory_accesses_injections ail_prog = ", \"" ^ "[auto annot (focus)]" ^ pos_info + (* The fmt for type. Filled by CN_XXX_ANNOT *) + ^ ":%s:%s" ^ ", " ^ autoannot_fmt ^ "\"" @@ -377,6 +383,8 @@ let memory_accesses_injections ail_prog = ", \"" ^ "[auto annot (focus)]" ^ pos_info + (* The fmt for type. Filled by CN_XXX_ANNOT *) + ^ ":%s:%s" ^ ", " ^ autoannot_fmt ^ "\"" diff --git a/runtime/libcn/include/cn-autoannot/auto_annot.h b/runtime/libcn/include/cn-autoannot/auto_annot.h index 8b42b1359..4cfd50eb0 100644 --- a/runtime/libcn/include/cn-autoannot/auto_annot.h +++ b/runtime/libcn/include/cn-autoannot/auto_annot.h @@ -28,18 +28,20 @@ extern FILE *auto_annot_log_file; ({ \ typeof(LV) *__tmp = &(LV); \ int64_t index; \ - if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index)) \ - cn_auto_annot_printf(FMT, index, ##__VA_ARGS__); \ + type_sig sig; \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index, &sig)) \ + cn_auto_annot_printf(FMT, "RW", sig, index, ##__VA_ARGS__); \ CN_LOAD(LV); \ }) -#define CN_STORE_OP_ANNOT(LV, op, X, FMT, ...) \ +#define CN_STORE_OP_ANNOT(LV, op, X, FMT, ...) \ ({ \ typeof(LV) *__tmp; \ __tmp = &(LV); \ int64_t index; \ - if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index)) \ - cn_auto_annot_printf(FMT, index, ##__VA_ARGS__); \ + type_sig sig; \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index, &sig)) \ + cn_auto_annot_printf(FMT, "RW", sig, index, ##__VA_ARGS__); \ CN_STORE_OP(LV, op, X); \ }) @@ -88,7 +90,7 @@ void clear_focus(void); void insert_focus(int64_t index, type_sig sig); void insert_iter_res( uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig); -int needs_focus(uint64_t address, uint64_t size, int64_t *index_out); +int needs_focus(uint64_t address, uint64_t size, int64_t *index_out, type_sig *sig_out); #ifdef __cplusplus } diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index 1f9217153..710d5b849 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -85,7 +85,7 @@ void insert_iter_res(uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, /// (i) is in a iterated resource /// (ii) is not focused /// If (i) and (ii), it needs focus, and returns 1. -int needs_focus(uint64_t address, uint64_t size, int64_t *index_out) { +int needs_focus(uint64_t address, uint64_t size, int64_t *index_out, type_sig* sig_out) { assert(cn_focus_global_context != NULL); // (i) search for iterated resource iter_res_set *iter = cn_focus_global_context->iter_ress; @@ -116,6 +116,7 @@ int needs_focus(uint64_t address, uint64_t size, int64_t *index_out) { } // The index is not focused *index_out = index; + *sig_out = cur->res.sig; return 1; } // We didn't find any appropriate iterated resource diff --git a/runtime/libcn/test/autoannot/focus.cpp b/runtime/libcn/test/autoannot/focus.cpp index d1fc2d345..7628266ea 100644 --- a/runtime/libcn/test/autoannot/focus.cpp +++ b/runtime/libcn/test/autoannot/focus.cpp @@ -10,6 +10,7 @@ TEST(LibAutoAnnot, BasicOperations) { initialise_focus_context(); push_focus_context(); int64_t index = -1; + type_sig sig = NULL; /* let p = 0xcafe000; @@ -19,45 +20,54 @@ TEST(LibAutoAnnot, BasicOperations) { /* focus RW, 1u64; */ insert_focus(1, "unsigned long"); - ASSERT_EQ(needs_focus(0xcafe0000, 8, &index), 1) << "Lack of focus for p[0]"; + ASSERT_EQ(needs_focus(0xcafe0000, 8, &index, &sig), 1) << "Lack of focus for p[0]"; ASSERT_EQ(index, 0) << "Focused index should be 0"; - ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "Focused"; - ASSERT_EQ(needs_focus(0xcafe1000, 8, &index), 0) + ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0) << "Focused"; + ASSERT_EQ(needs_focus(0xcafe1000, 8, &index, &sig), 0) << "No appropriate resource, so we don't need focus"; clear_focus(); - ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 1) << "Cleared"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 1) << "Cleared"; ASSERT_EQ(index, 1) << "Focused index should be 1"; + ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long"; insert_focus(1, "unsigned long"); - ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "Focused"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0) << "Focused"; push_focus_context(); insert_iter_res(0xcafe0000, 0, 4, 8, "unsigned long"); insert_iter_res(0x10000000, 1, 4, 8, "unsigned long"); insert_iter_res(0x20000000, 0, 4, 4, "unsigned int"); - ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 1) << "No focus in the current level"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 1) + << "No focus in the current level"; ASSERT_EQ(index, 1) << "Focused index should be 1"; - ASSERT_EQ(needs_focus(0xcafe0000, 8, &index), 1) << "No focus in the current level"; + ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long"; + ASSERT_EQ(needs_focus(0xcafe0000, 8, &index, &sig), 1) + << "No focus in the current level"; ASSERT_EQ(index, 0) << "Focused index should be 0"; + ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long"; insert_focus(1, "unsigned long"); - ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "Just focused"; - ASSERT_EQ(needs_focus(0x10000008, 8, &index), 0) << "Just focused"; - ASSERT_EQ(needs_focus(0x20000004, 4, &index), 1) << "Type mismatch"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x10000008, 8, &index, &sig), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x20000004, 4, &index, &sig), 1) << "Type mismatch"; ASSERT_EQ(index, 1) << "Focused index should be 1"; - ASSERT_EQ(needs_focus(0x10000000, 8, &index), 0) << "Out of the iter_res"; + ASSERT_EQ(strcmp(sig, "unsigned int"), 0) << "Focused type should be unsigned int"; + ASSERT_EQ(needs_focus(0x10000000, 8, &index, &sig), 0) << "Out of the iter_res"; insert_focus(1, "unsigned int"); - ASSERT_EQ(needs_focus(0x20000004, 4, &index), 0) << "Just focused"; + ASSERT_EQ(needs_focus(0x20000004, 4, &index, &sig), 0) << "Just focused"; pop_focus_context(); // Check if it remembers the context - ASSERT_EQ(needs_focus(0xcafe0000, 8, &index), 1) << "Lack of focus for p[0]"; + ASSERT_EQ(needs_focus(0xcafe0000, 8, &index, &sig), 1) << "Lack of focus for p[0]"; ASSERT_EQ(index, 0) << "Focused index should be 0"; - ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "Focus has already been annotated"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0) + << "Focus has already been annotated"; + ASSERT_EQ(strcmp(sig, "unsigned long"), 0) << "Focused type should be unsigned long"; pop_focus_context(); - ASSERT_EQ(needs_focus(0xcafe0000, 8, &index), 0) << "No need for focus"; - ASSERT_EQ(needs_focus(0xcafe0008, 8, &index), 0) << "No need for focus"; + ASSERT_EQ(needs_focus(0xcafe0000, 8, &index, &sig), 0) << "No need for focus"; + ASSERT_EQ(needs_focus(0xcafe0008, 8, &index, &sig), 0) << "No need for focus"; } From 94d76e539953a66b52a07f42220e8db30891b8e1 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 21 Aug 2025 17:48:32 +0100 Subject: [PATCH 31/38] clang format --- .../libcn/include/cn-autoannot/auto_annot.h | 16 +- runtime/libcn/include/cn-executable/utils.h | 5 + runtime/libcn/src/cn-autoannot/auto_annot.c | 18 +- runtime/libcn/src/cn-autoannot/focus_ctx.c | 157 +++++++++--------- 4 files changed, 101 insertions(+), 95 deletions(-) diff --git a/runtime/libcn/include/cn-autoannot/auto_annot.h b/runtime/libcn/include/cn-autoannot/auto_annot.h index 4cfd50eb0..67e8e6841 100644 --- a/runtime/libcn/include/cn-autoannot/auto_annot.h +++ b/runtime/libcn/include/cn-autoannot/auto_annot.h @@ -5,7 +5,6 @@ #include #include - #ifdef __cplusplus extern "C" { #endif @@ -15,12 +14,11 @@ typedef const char *type_sig; // Defined in cn-autoannot/auto_annot.c extern FILE *auto_annot_log_file; -#define cn_auto_annot_printf(...) \ - fprintf(auto_annot_log_file, __VA_ARGS__) +#define cn_auto_annot_printf(...) fprintf(auto_annot_log_file, __VA_ARGS__) // Wrapper for cn values -#define CN_INSERT_ITER_RES(base, start, end, size, sig) \ - insert_iter_res((uint64_t)base->ptr, start->val, end->val, size, sig) +#define CN_INSERT_ITER_RES(base, start, end, size, sig) \ + insert_iter_res((uint64_t)base->ptr, start->val, end->val, size, sig) #define CN_INSERT_FOCUS(index, sig) insert_focus(index->val, sig) @@ -29,19 +27,19 @@ extern FILE *auto_annot_log_file; typeof(LV) *__tmp = &(LV); \ int64_t index; \ type_sig sig; \ - if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index, &sig)) \ - cn_auto_annot_printf(FMT, "RW", sig, index, ##__VA_ARGS__); \ + if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index, &sig)) \ + cn_auto_annot_printf(FMT, "RW", sig, index, ##__VA_ARGS__); \ CN_LOAD(LV); \ }) -#define CN_STORE_OP_ANNOT(LV, op, X, FMT, ...) \ +#define CN_STORE_OP_ANNOT(LV, op, X, FMT, ...) \ ({ \ typeof(LV) *__tmp; \ __tmp = &(LV); \ int64_t index; \ type_sig sig; \ if (needs_focus((uint64_t)__tmp, sizeof(typeof(LV)), &index, &sig)) \ - cn_auto_annot_printf(FMT, "RW", sig, index, ##__VA_ARGS__); \ + cn_auto_annot_printf(FMT, "RW", sig, index, ##__VA_ARGS__); \ CN_STORE_OP(LV, op, X); \ }) diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index 39ae8e662..566e81131 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -612,8 +612,13 @@ static inline void cn_load(void* ptr, size_t size) { static inline void cn_store(void* ptr, size_t size) { // cn_printf(CN_LOGGING_INFO, " \x1b[31mSTORE\x1b[0m[%lu] - ptr: %p\n", size, ptr); } +<<<<<<< HEAD static inline void cn_postfix(void* ptr, size_t size) { // cn_printf(CN_LOGGING_INFO, " \x1b[31mPOSTFIX\x1b[0m[%lu] - ptr: %p\n", size, ptr); +======= +static inline void cn_postfix(void *ptr, size_t size){ + // cn_printf(CN_LOGGING_INFO, " \x1b[31mPOSTFIX\x1b[0m[%lu] - ptr: %p\n", size, ptr); +>>>>>>> fbd05b533 (clang format) } // use this macro to wrap an argument to another macro that contains commas diff --git a/runtime/libcn/src/cn-autoannot/auto_annot.c b/runtime/libcn/src/cn-autoannot/auto_annot.c index f7183f1e0..0dfca866e 100644 --- a/runtime/libcn/src/cn-autoannot/auto_annot.c +++ b/runtime/libcn/src/cn-autoannot/auto_annot.c @@ -1,21 +1,23 @@ #include -#include + #include +#include + // Single definition of the global log file pointer FILE *auto_annot_log_file = NULL; //void initialise_focus_context(); void initialize_auto_annot(const char *log_file) { - auto_annot_log_file = fopen(log_file, "a"); - if (auto_annot_log_file == NULL) { - cn_printf(CN_LOGGING_ERROR, "Failed to open log file: %s\n", log_file); - exit(EXIT_FAILURE); - } - initialise_focus_context(); + auto_annot_log_file = fopen(log_file, "a"); + if (auto_annot_log_file == NULL) { + cn_printf(CN_LOGGING_ERROR, "Failed to open log file: %s\n", log_file); + exit(EXIT_FAILURE); + } + initialise_focus_context(); } void finalize_auto_annot() { - fclose(auto_annot_log_file); + fclose(auto_annot_log_file); } diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index 710d5b849..d0be2a0e3 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -1,5 +1,6 @@ #include +#include #include #include #include // for SIGABRT @@ -7,118 +8,118 @@ #include #include #include -#include #include #include -#include // Note(HK): // we don't have to care about the difference between Owned/Block here // because they are handled by the standard Fulminate machinery. // i.e., if there is a discrepancy, it will be caught by Fulminate. -struct focus_context* cn_focus_global_context; // top of the stack +struct focus_context *cn_focus_global_context; // top of the stack // should happen simultaneously with ghost_stack_depth_incr void push_focus_context(void) { - struct focus_context* new_context = fulm_default_alloc.malloc(sizeof(struct focus_context)); - new_context->indices = NULL; - new_context->iter_ress = NULL; - new_context->prev = cn_focus_global_context; - cn_focus_global_context = new_context; + struct focus_context *new_context = + fulm_default_alloc.malloc(sizeof(struct focus_context)); + new_context->indices = NULL; + new_context->iter_ress = NULL; + new_context->prev = cn_focus_global_context; + cn_focus_global_context = new_context; } void initialise_focus_context() { - push_focus_context(); + push_focus_context(); } void pop_focus_context(void) { - struct focus_context *old_context = cn_focus_global_context; - cn_focus_global_context = cn_focus_global_context->prev; - // free - focus_set *cur_focus = old_context->indices; - while (cur_focus) { - focus_set *next = cur_focus->next; - fulm_free(cur_focus, &fulm_default_alloc); - cur_focus = next; - } + struct focus_context *old_context = cn_focus_global_context; + cn_focus_global_context = cn_focus_global_context->prev; + // free + focus_set *cur_focus = old_context->indices; + while (cur_focus) { + focus_set *next = cur_focus->next; + fulm_free(cur_focus, &fulm_default_alloc); + cur_focus = next; + } - iter_res_set *cur_iter_res = old_context->iter_ress; - while (cur_iter_res) { - iter_res_set *next = cur_iter_res->next; - fulm_free(cur_iter_res, &fulm_default_alloc); - cur_iter_res = next; - } + iter_res_set *cur_iter_res = old_context->iter_ress; + while (cur_iter_res) { + iter_res_set *next = cur_iter_res->next; + fulm_free(cur_iter_res, &fulm_default_alloc); + cur_iter_res = next; + } } void insert_focus(int64_t index, type_sig sig) { - struct focus_set* new_set = fulm_malloc(sizeof(struct focus_set), &fulm_default_alloc); - new_set->info.index = index; - new_set->info.sig = sig; - new_set->next = cn_focus_global_context->indices; - cn_focus_global_context->indices = new_set; + struct focus_set *new_set = fulm_malloc(sizeof(struct focus_set), &fulm_default_alloc); + new_set->info.index = index; + new_set->info.sig = sig; + new_set->next = cn_focus_global_context->indices; + cn_focus_global_context->indices = new_set; } void clear_focus() { - focus_set *cur_focus = cn_focus_global_context->indices; - while (cur_focus) { - focus_set *next = cur_focus->next; - fulm_free(cur_focus, &fulm_default_alloc); - cur_focus = next; - } - cn_focus_global_context->indices = NULL; + focus_set *cur_focus = cn_focus_global_context->indices; + while (cur_focus) { + focus_set *next = cur_focus->next; + fulm_free(cur_focus, &fulm_default_alloc); + cur_focus = next; + } + cn_focus_global_context->indices = NULL; } -void insert_iter_res(uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig) { - struct iter_res_set* new = fulm_malloc(sizeof(iter_res_set), &fulm_default_alloc); - new->res.ptr = ptr; - new->res.size = size; - new->res.start = start; - new->res.end = end; - new->res.sig = sig; - new->next = cn_focus_global_context->iter_ress; - cn_focus_global_context->iter_ress = new; +void insert_iter_res( + uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig) { + struct iter_res_set *new = fulm_malloc(sizeof(iter_res_set), &fulm_default_alloc); + new->res.ptr = ptr; + new->res.size = size; + new->res.start = start; + new->res.end = end; + new->res.sig = sig; + new->next = cn_focus_global_context->iter_ress; + cn_focus_global_context->iter_ress = new; } /// Checks if the given address /// (i) is in a iterated resource /// (ii) is not focused /// If (i) and (ii), it needs focus, and returns 1. -int needs_focus(uint64_t address, uint64_t size, int64_t *index_out, type_sig* sig_out) { - assert(cn_focus_global_context != NULL); - // (i) search for iterated resource - iter_res_set *iter = cn_focus_global_context->iter_ress; - while (iter) { - iter_res_set *cur = iter; - iter = iter->next; - uint64_t start = cur->res.ptr + cur->res.start * cur->res.size; - uint64_t end = cur->res.ptr + (cur->res.end + 1) * cur->res.size; - int64_t offset = address - cur->res.ptr; - if (address < start || address + size > end) { - continue; - } - if (offset % cur->res.size != 0) { - continue; - } +int needs_focus(uint64_t address, uint64_t size, int64_t *index_out, type_sig *sig_out) { + assert(cn_focus_global_context != NULL); + // (i) search for iterated resource + iter_res_set *iter = cn_focus_global_context->iter_ress; + while (iter) { + iter_res_set *cur = iter; + iter = iter->next; + uint64_t start = cur->res.ptr + cur->res.start * cur->res.size; + uint64_t end = cur->res.ptr + (cur->res.end + 1) * cur->res.size; + int64_t offset = address - cur->res.ptr; + if (address < start || address + size > end) { + continue; + } + if (offset % cur->res.size != 0) { + continue; + } - uint64_t index = offset / cur->res.size; + uint64_t index = offset / cur->res.size; - // Case: an appropriate iterated resource is found - // (ii) search for focus - focus_set* cur_focus = cn_focus_global_context->indices; - while (cur_focus) { - if (cur_focus->info.index == index && - strcmp(cur_focus->info.sig, cur->res.sig) == 0) { - return 0; - } - cur_focus = cur_focus->next; - } - // The index is not focused - *index_out = index; - *sig_out = cur->res.sig; - return 1; + // Case: an appropriate iterated resource is found + // (ii) search for focus + focus_set *cur_focus = cn_focus_global_context->indices; + while (cur_focus) { + if (cur_focus->info.index == index && + strcmp(cur_focus->info.sig, cur->res.sig) == 0) { + return 0; + } + cur_focus = cur_focus->next; } - // We didn't find any appropriate iterated resource - return 0; + // The index is not focused + *index_out = index; + *sig_out = cur->res.sig; + return 1; + } + // We didn't find any appropriate iterated resource + return 0; } From 0dfc56fd094a25b6cd9330fc6111bbab51c30567 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 21 Aug 2025 17:53:00 +0100 Subject: [PATCH 32/38] Only calls `gen_env_fmt_printer` when auto_annot is enabled --- lib/fulminate/fulminate.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index 3378a977b..2dd84f7a1 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -273,10 +273,12 @@ let memory_accesses_injections ail_prog = List.iter (fun (access, env) -> (* autoannot things *) - let fmt, args = gen_env_fmt_printer env in - let autoannot_fmt = fmt ^ "\\n" in - let autoannot_fmt_args = - List.fold_left (fun acc arg -> acc ^ ", " ^ arg) "" args + let autoannot_fmt, autoannot_fmt_args = + if !Config.with_auto_annot then ( + let fmt, args = gen_env_fmt_printer env in + (fmt ^ "\\n", List.fold_left (fun acc arg -> acc ^ ", " ^ arg) "" args)) + else + ("", "") in match access with | Load { loc; _ } -> From 4d3bdd1472740c7bef92eabb3b91508a4af72174 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 21 Aug 2025 18:14:08 +0100 Subject: [PATCH 33/38] clang-format, again ...? --- runtime/libcn/include/cn-executable/utils.h | 5 ----- 1 file changed, 5 deletions(-) diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index 566e81131..39ae8e662 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -612,13 +612,8 @@ static inline void cn_load(void* ptr, size_t size) { static inline void cn_store(void* ptr, size_t size) { // cn_printf(CN_LOGGING_INFO, " \x1b[31mSTORE\x1b[0m[%lu] - ptr: %p\n", size, ptr); } -<<<<<<< HEAD static inline void cn_postfix(void* ptr, size_t size) { // cn_printf(CN_LOGGING_INFO, " \x1b[31mPOSTFIX\x1b[0m[%lu] - ptr: %p\n", size, ptr); -======= -static inline void cn_postfix(void *ptr, size_t size){ - // cn_printf(CN_LOGGING_INFO, " \x1b[31mPOSTFIX\x1b[0m[%lu] - ptr: %p\n", size, ptr); ->>>>>>> fbd05b533 (clang format) } // use this macro to wrap an argument to another macro that contains commas From 037957356d1962c681b3e6e269874d3381900f3e Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 21 Aug 2025 18:27:48 +0100 Subject: [PATCH 34/38] print results to stdout --- lib/autoAnnot/autoAnnot.ml | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/lib/autoAnnot/autoAnnot.ml b/lib/autoAnnot/autoAnnot.ml index dab43f6fc..7aaba9fe7 100644 --- a/lib/autoAnnot/autoAnnot.ml +++ b/lib/autoAnnot/autoAnnot.ml @@ -36,13 +36,7 @@ let print_focus_suggestion filename line kind ty w0 coeffs = let elems = if w0 = 0 then body else string_of_int w0 :: body in let sum = String.concat " + " elems in let annotation = signature ^ sum in - Pp.( - debug - 10 - (lazy - (item - "AutoAnnot: suggested annotation" - (string pos ^^ string ": " ^^ string annotation)))) + Pp.progress_simple pos annotation let generate_focus_annot_aux filename line (kind, ty, assignments_list) : unit = @@ -213,7 +207,7 @@ let parse (log_file : string) : annot list = let run_autoannot (log_file : string) : unit = - Pp.(debug 10 (lazy (item "Running auto-annotation" (string log_file)))); + Pp.print stdout (Pp.string "[Result of auto-annotation]"); let data = parse log_file in let focus_annots = data |> List.filter_map (function Focus f -> Some f) in generate_focus_annot focus_annots From 63d549d533c2de916a4791e450d32bc29614250b Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 25 Sep 2025 14:05:32 +0100 Subject: [PATCH 35/38] Fix compile error --- bin/annot.ml | 92 +++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 84 insertions(+), 8 deletions(-) diff --git a/bin/annot.ml b/bin/annot.ml index 84674b42e..abbd1f770 100644 --- a/bin/annot.ml +++ b/bin/annot.ml @@ -28,8 +28,8 @@ let run_auto_annot dont_run num_samples max_backtracks - _max_unfolds - _max_array_length + max_unfolds + max_array_length build_tool sanitizers print_seed @@ -58,10 +58,16 @@ let run_auto_annot experimental_struct_asgn_destruction experimental_product_arg_destruction experimental_learning - smt_pruning + static_absint + smt_pruning_before_absinst + smt_pruning_after_absinst + smt_pruning_at_runtime + symbolic + symbolic_timeout print_size_info print_backtrack_info print_satisfaction_info + print_discard_info = (* flags *) Cerb_debug.debug_level := debug_level; @@ -121,7 +127,14 @@ let run_auto_annot experimental_struct_asgn_destruction; experimental_product_arg_destruction; experimental_learning; - smt_pruning; + static_absint; + smt_pruning_before_absinst; + smt_pruning_after_absinst; + smt_pruning_at_runtime; + symbolic; + symbolic_timeout; + max_unfolds; + max_array_length; print_seed; input_timeout; null_in_every; @@ -145,6 +158,7 @@ let run_auto_annot print_size_info; print_backtrack_info; print_satisfaction_info; + print_discard_info; with_auto_annot = true } in @@ -497,12 +511,45 @@ module Flags = struct Arg.(value & flag & info [ "experimental-learning" ] ~doc) - let smt_pruning = - let doc = "(Experimental) Use SMT solver to prune unsatisfiable branches" in + let smt_pruning_before_absinst = + let doc = + "(Experimental) Use SMT solver to prune unsatisfiable branches before abstract \ + interpretation" + in Arg.( value & opt (enum [ ("none", `None); ("fast", `Fast); ("slow", `Slow) ]) `None - & info [ "smt-pruning" ] ~doc) + & info [ "smt-pruning-before-absint" ] ~doc) + + + let smt_pruning_after_absinst = + let doc = + "(Experimental) Use SMT solver to prune unsatisfiable branches after abstract \ + interpretation" + in + Arg.( + value + & opt (enum [ ("none", `None); ("fast", `Fast); ("slow", `Slow) ]) `None + & info [ "smt-pruning-after-absint" ] ~doc) + + + let smt_pruning_at_runtime = + let doc = "(Experimental) Use SMT solver to prune branches at runtime" in + Arg.(value & flag & info [ "smt-pruning-at-runtime" ] ~doc) + + + let static_absint = + let doc = + "(Experimental) Use static abstract interpretation with specified domain (or a \ + comma-separated list). (e.g., 'interval', 'wrapped_interval')" + in + Arg.( + value + & opt + (list + (enum [ ("interval", "interval"); ("wrapped_interval", "wrapped_interval") ])) + [] + & info [ "static-absint" ] ~docv:"DOMAIN" ~doc) let print_size_info = @@ -518,6 +565,29 @@ module Flags = struct let print_satisfaction_info = let doc = "(Experimental) Print satisfaction info" in Arg.(value & flag & info [ "print-satisfaction-info" ] ~doc) + + + let print_discard_info = + let doc = "(Experimental) Print discard info" in + Arg.(value & flag & info [ "print-discard-info" ] ~doc) + + + let symbolic = + let doc = + "(Experimental) Use symbolic execution for test generation instead of concrete \ + value generation." + in + Arg.(value & flag & info [ "symbolic" ] ~doc) + + + let symbolic_timeout = + let doc = "Set timeout for SMT solver in symbolic mode (seconds)" in + Arg.(value & opt (some int) None & info [ "symbolic-timeout" ] ~doc) + + + let max_path_length = + let doc = "Set maximum symbolic path length for exploration" in + Arg.(value & opt (some int) None & info [ "max-path-length" ] ~doc) end let cmd = @@ -574,10 +644,16 @@ let cmd = $ Flags.experimental_struct_asgn_destruction $ Flags.experimental_product_arg_destruction $ Flags.experimental_learning - $ Flags.smt_pruning + $ Flags.static_absint + $ Flags.smt_pruning_before_absinst + $ Flags.smt_pruning_after_absinst + $ Flags.smt_pruning_at_runtime + $ Flags.symbolic + $ Flags.symbolic_timeout $ Flags.print_size_info $ Flags.print_backtrack_info $ Flags.print_satisfaction_info + $ Flags.print_discard_info in let doc = "Generates proof annotations such as `unfold` and `focus` from testing executions." From 8898d6398c536ecc558d2501d5c534f5cbaa39c6 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Thu, 25 Sep 2025 18:48:14 +0100 Subject: [PATCH 36/38] Merged the machinery (WIP) --- .../libcn/include/cn-autoannot/auto_annot.h | 18 +++-- runtime/libcn/include/cn-executable/utils.h | 10 +++ runtime/libcn/src/cn-autoannot/focus_ctx.c | 73 ++++++------------- runtime/libcn/src/cn-executable/utils.c | 2 +- 4 files changed, 46 insertions(+), 57 deletions(-) diff --git a/runtime/libcn/include/cn-autoannot/auto_annot.h b/runtime/libcn/include/cn-autoannot/auto_annot.h index 67e8e6841..d73292fae 100644 --- a/runtime/libcn/include/cn-autoannot/auto_annot.h +++ b/runtime/libcn/include/cn-autoannot/auto_annot.h @@ -60,10 +60,17 @@ struct iter_res { type_sig sig; }; -typedef struct iter_res_set { - struct iter_res res; - struct iter_res_set *next; -} iter_res_set; +enum cn_res_type { + CN_RES_ITER, + OTHER, +}; + +struct cn_res { + enum cn_res_type type; + union { + struct iter_res iter_res; + }; +}; struct focus_info { int64_t index; @@ -77,7 +84,6 @@ typedef struct focus_set { struct focus_context { focus_set *indices; - iter_res_set *iter_ress; struct focus_context *prev; }; @@ -86,8 +92,6 @@ void push_focus_context(void); void pop_focus_context(void); void clear_focus(void); void insert_focus(int64_t index, type_sig sig); -void insert_iter_res( - uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig); int needs_focus(uint64_t address, uint64_t size, int64_t *index_out, type_sig *sig_out); #ifdef __cplusplus diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index 39ae8e662..2c01222f6 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -7,6 +7,7 @@ #include "hash_table.h" #include "rts_deps.h" #include "stack.h" +#include #define fallthrough __attribute__((__fallthrough__)) @@ -152,6 +153,13 @@ typedef struct cn_alloc_id { typedef hash_table cn_map; +enum RuntimeMode { + RUNTIME_NORMAL_MODE, + RUNTIME_OWNERSHIP_STACK_MODE, + RUNTIME_AUTO_ANNOT_MODE, +}; +extern enum RuntimeMode runtime_mode; + void initialise_ownership_ghost_state(void); void free_ownership_ghost_state(void); void initialise_ghost_stack_depth(void); @@ -568,6 +576,8 @@ CN_GEN_MAP_GET(cn_map) // }; int ownership_ghost_state_get_depth(int64_t address); +ownership_ghost_info* ownership_ghost_state_get(int64_t address); + void ownership_ghost_state_set(int64_t address, size_t size, int stack_depth_val, diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index d0be2a0e3..cdcff5321 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -24,7 +24,6 @@ void push_focus_context(void) { struct focus_context *new_context = fulm_default_alloc.malloc(sizeof(struct focus_context)); new_context->indices = NULL; - new_context->iter_ress = NULL; new_context->prev = cn_focus_global_context; cn_focus_global_context = new_context; } @@ -44,12 +43,6 @@ void pop_focus_context(void) { cur_focus = next; } - iter_res_set *cur_iter_res = old_context->iter_ress; - while (cur_iter_res) { - iter_res_set *next = cur_iter_res->next; - fulm_free(cur_iter_res, &fulm_default_alloc); - cur_iter_res = next; - } } void insert_focus(int64_t index, type_sig sig) { @@ -70,56 +63,38 @@ void clear_focus() { cn_focus_global_context->indices = NULL; } -void insert_iter_res( - uint64_t ptr, uint64_t start, uint64_t end, uint64_t size, type_sig sig) { - struct iter_res_set *new = fulm_malloc(sizeof(iter_res_set), &fulm_default_alloc); - new->res.ptr = ptr; - new->res.size = size; - new->res.start = start; - new->res.end = end; - new->res.sig = sig; - new->next = cn_focus_global_context->iter_ress; - cn_focus_global_context->iter_ress = new; -} - /// Checks if the given address /// (i) is in a iterated resource /// (ii) is not focused /// If (i) and (ii), it needs focus, and returns 1. int needs_focus(uint64_t address, uint64_t size, int64_t *index_out, type_sig *sig_out) { assert(cn_focus_global_context != NULL); - // (i) search for iterated resource - iter_res_set *iter = cn_focus_global_context->iter_ress; - while (iter) { - iter_res_set *cur = iter; - iter = iter->next; - uint64_t start = cur->res.ptr + cur->res.start * cur->res.size; - uint64_t end = cur->res.ptr + (cur->res.end + 1) * cur->res.size; - int64_t offset = address - cur->res.ptr; - if (address < start || address + size > end) { - continue; - } - if (offset % cur->res.size != 0) { - continue; - } + ownership_ghost_info * info = ownership_ghost_state_get(address); + if (!info) { + return 0; + } + struct cn_res* res_info = info->res_info_stack->top->cn_res_info; + + if (res_info->type != CN_RES_ITER) { + return 0; + } + struct iter_res* res = &res_info->iter_res; - uint64_t index = offset / cur->res.size; + int64_t offset = address - res->ptr; + uint64_t index = offset / res->size; - // Case: an appropriate iterated resource is found - // (ii) search for focus - focus_set *cur_focus = cn_focus_global_context->indices; - while (cur_focus) { - if (cur_focus->info.index == index && - strcmp(cur_focus->info.sig, cur->res.sig) == 0) { - return 0; - } - cur_focus = cur_focus->next; + // Case: an appropriate iterated resource is found + // (ii) search for focus + focus_set *cur_focus = cn_focus_global_context->indices; + while (cur_focus) { + if (cur_focus->info.index == index && + strcmp(cur_focus->info.sig, res->sig) == 0) { + return 0; } - // The index is not focused - *index_out = index; - *sig_out = cur->res.sig; - return 1; + cur_focus = cur_focus->next; } - // We didn't find any appropriate iterated resource - return 0; + // The index is not focused + *index_out = index; + *sig_out = res->sig; + return 1; } diff --git a/runtime/libcn/src/cn-executable/utils.c b/runtime/libcn/src/cn-executable/utils.c index 974d940e0..6de0d4560 100644 --- a/runtime/libcn/src/cn-executable/utils.c +++ b/runtime/libcn/src/cn-executable/utils.c @@ -24,7 +24,7 @@ signed long nr_owned_predicates; _Bool exec_c_locs_mode; _Bool ownership_stack_mode; -static signed long UNMAPPED_VAL = -1; + static signed long UNMAPPED_VAL = -1; static signed long WILDCARD_DEPTH = INT_MIN + 1; static allocator bump_alloc = (allocator){ From d8e077523bfe154d8a0db37a9c503b5db7c9aadc Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Fri, 26 Sep 2025 17:27:29 +0100 Subject: [PATCH 37/38] Fix weired pointer cast problem --- bin/annot.ml | 3 +-- lib/fulminate/fulminate.ml | 14 +++++++++++--- runtime/libcn/include/cn-autoannot/auto_annot.h | 3 ++- runtime/libcn/src/cn-autoannot/focus_ctx.c | 1 + 4 files changed, 15 insertions(+), 6 deletions(-) diff --git a/bin/annot.ml b/bin/annot.ml index abbd1f770..5424048fe 100644 --- a/bin/annot.ml +++ b/bin/annot.ml @@ -230,11 +230,10 @@ let run_auto_annot snd (Unix.waitpid [] pid) in match status with - | Unix.WEXITED 0 -> () + | Unix.WEXITED 0 -> AutoAnnot.run_autoannot (Filename.concat output_dir log_file) | Unix.WEXITED n -> Pp.(debug 5 (lazy (item "Test runner exit code" (int n)))) | Unix.WSIGNALED n -> Pp.(debug 5 (lazy (item "Test runner signaled" (int n)))) | Unix.WSTOPPED n -> Pp.(debug 5 (lazy (item "Test runner stopped" (int n))))); - AutoAnnot.run_autoannot (Filename.concat output_dir log_file); Result.ok ()) diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index 2dd84f7a1..e8603ef17 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -937,9 +937,17 @@ let main in (* Save things *) let oc = Stdlib.open_out out_filename in - output_to_oc oc [ "#define __CN_INSTRUMENT\n"; "#include \n" ]; - if !Config.with_auto_annot then - output_to_oc oc [ "#include \n" ]; + if !Config.with_auto_annot then ( + output_to_oc + oc + [ "#define __CN_INSTRUMENT\n"; + "#include \n"; + "#include \n" + ]; + output_to_oc oc [ "#include \n" ]) + else ( + output_to_oc oc [ "#define __CN_INSTRUMENT\n"; "#include \n" ]; + output_to_oc oc [ "#include \n" ]); output_to_oc oc [ "#include \n" ]; output_to_oc oc cn_header_decls_list; output_to_oc diff --git a/runtime/libcn/include/cn-autoannot/auto_annot.h b/runtime/libcn/include/cn-autoannot/auto_annot.h index d73292fae..e65d8bcdd 100644 --- a/runtime/libcn/include/cn-autoannot/auto_annot.h +++ b/runtime/libcn/include/cn-autoannot/auto_annot.h @@ -1,9 +1,10 @@ #ifndef FOCUS_CTX_H #define FOCUS_CTX_H -#include #include #include +#include +#include #ifdef __cplusplus extern "C" { diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index cdcff5321..0cfcff7ba 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -9,6 +9,7 @@ #include #include +#include #include #include From b57893df7ed7e13da78e26c1f959a0ede31b0e78 Mon Sep 17 00:00:00 2001 From: Hiroyuki Katsura Date: Mon, 2 Mar 2026 13:34:36 +0000 Subject: [PATCH 38/38] wip rebasing --- bin/annot.ml | 17 +++++++-- lib/fulminate/fulminate.ml | 5 ++- lib/fulminate/internal.ml | 12 +------ .../libcn/include/cn-autoannot/auto_annot.h | 2 +- runtime/libcn/include/cn-executable/utils.h | 2 +- runtime/libcn/lib/dune | 2 +- runtime/libcn/src/cn-autoannot/auto_annot.c | 2 +- runtime/libcn/src/cn-autoannot/focus_ctx.c | 36 +++---------------- 8 files changed, 29 insertions(+), 49 deletions(-) diff --git a/bin/annot.ml b/bin/annot.ml index 5424048fe..29edd5c84 100644 --- a/bin/annot.ml +++ b/bin/annot.ml @@ -8,6 +8,7 @@ let run_auto_annot filename cc macros + permissive incl_dirs incl_files debug_level @@ -100,6 +101,7 @@ let run_auto_annot ~filename ~cc ~macros:(("__CN_TEST", None) :: ("__CN_INSTRUMENT", None) :: macros) + ~permissive ~incl_dirs ~incl_files ~csv_times @@ -117,13 +119,18 @@ let run_auto_annot ~handle_error ~f:(fun ~cabs_tunit ~prog5 ~ail_prog ~statement_locs:_ ~paused -> let config : TestGeneration.config = - { cc; + { TestGeneration.default_cfg with + cc; print_steps; num_samples; max_backtracks; build_tool; sanitizers; - inline_everything; + inline = + List.assoc + String.equal + (if inline_everything then "Everything" else "Nothing") + TestGeneration.Options.inline_mode; experimental_struct_asgn_destruction; experimental_product_arg_destruction; experimental_learning; @@ -183,7 +190,12 @@ let run_auto_annot ~without_ownership_checking ~without_loop_invariants:false ~with_loop_leak_checks:true + ~without_lemma_checks:false + ~exec_c_locs_mode:false + ~experimental_ownership_stack_mode:false + ~experimental_curly_braces:false ~with_testing:true + ~skip_and_only:(skip, only) filename cc pp_file @@ -596,6 +608,7 @@ let cmd = $ Common.Flags.file $ Common.Flags.cc $ Common.Flags.macros + $ Common.Flags.permissive $ Common.Flags.incl_dirs $ Common.Flags.incl_files $ Common.Flags.debug_level diff --git a/lib/fulminate/fulminate.ml b/lib/fulminate/fulminate.ml index e8603ef17..42d23a099 100644 --- a/lib/fulminate/fulminate.ml +++ b/lib/fulminate/fulminate.ml @@ -50,7 +50,10 @@ let collect_memory_accesses (_, sigm) = let acc = ref [] in (* list of scoped variables *) let scan_for_decls_and_update_env (bs, ss) env f_expr f_stmt = - let lookup_ty sym = List.find (fun (sym', _) -> Sym.equal sym sym') bs in + let lookup_ty sym = + let _, (_, _, _, ty) = List.find (fun (sym', _) -> Sym.equal sym sym') bs in + (sym, ty) + in let env_cell = ref env in List.iter (fun s -> diff --git a/lib/fulminate/internal.ml b/lib/fulminate/internal.ml index b5e6351fc..3ef34d122 100644 --- a/lib/fulminate/internal.ml +++ b/lib/fulminate/internal.ml @@ -123,17 +123,7 @@ let generate_c_loop_invariants [ cond_inj; decl_inj; end_internal_inj; end_external_inj ]) ail_loop_invariants in - let ail_loop_decl_injs = - List.map - (fun (loc, bs_and_ss) -> - (get_start_loc loc, "{" :: generate_ail_stat_strs bs_and_ss)) - ail_loop_decls - in - let ail_loop_close_block_injs = - let close_token = if !Config.with_auto_annot then "}\nclear_focus ();" else "}" in - List.map (fun (loc, _) -> (get_end_loc loc, [ close_token ])) ail_loop_decls - in - ail_cond_injs @ ail_loop_decl_injs @ ail_loop_close_block_injs) + List.concat injs) let generate_fn_call_ghost_args_injs diff --git a/runtime/libcn/include/cn-autoannot/auto_annot.h b/runtime/libcn/include/cn-autoannot/auto_annot.h index e65d8bcdd..1bcbed470 100644 --- a/runtime/libcn/include/cn-autoannot/auto_annot.h +++ b/runtime/libcn/include/cn-autoannot/auto_annot.h @@ -88,7 +88,7 @@ struct focus_context { struct focus_context *prev; }; -void initialise_focus_context(); +void initialise_focus_context(void); void push_focus_context(void); void pop_focus_context(void); void clear_focus(void); diff --git a/runtime/libcn/include/cn-executable/utils.h b/runtime/libcn/include/cn-executable/utils.h index 2c01222f6..f01e8aaef 100644 --- a/runtime/libcn/include/cn-executable/utils.h +++ b/runtime/libcn/include/cn-executable/utils.h @@ -576,7 +576,7 @@ CN_GEN_MAP_GET(cn_map) // }; int ownership_ghost_state_get_depth(int64_t address); -ownership_ghost_info* ownership_ghost_state_get(int64_t address); +int ownership_ghost_state_get(int64_t address); void ownership_ghost_state_set(int64_t address, size_t size, diff --git a/runtime/libcn/lib/dune b/runtime/libcn/lib/dune index 3dc95f390..009b9191d 100644 --- a/runtime/libcn/lib/dune +++ b/runtime/libcn/lib/dune @@ -159,7 +159,7 @@ (run mkdir -p cn-smt) (chdir cn-smt - (run %{cc} -I ../../include -c %{src})) + (run %{cc} -Wno-cast-function-type -I ../../include -c %{src})) (run ar -rcs diff --git a/runtime/libcn/src/cn-autoannot/auto_annot.c b/runtime/libcn/src/cn-autoannot/auto_annot.c index 0dfca866e..525fc7445 100644 --- a/runtime/libcn/src/cn-autoannot/auto_annot.c +++ b/runtime/libcn/src/cn-autoannot/auto_annot.c @@ -18,6 +18,6 @@ void initialize_auto_annot(const char *log_file) { initialise_focus_context(); } -void finalize_auto_annot() { +void finalize_auto_annot(void) { fclose(auto_annot_log_file); } diff --git a/runtime/libcn/src/cn-autoannot/focus_ctx.c b/runtime/libcn/src/cn-autoannot/focus_ctx.c index 0cfcff7ba..2f492a99f 100644 --- a/runtime/libcn/src/cn-autoannot/focus_ctx.c +++ b/runtime/libcn/src/cn-autoannot/focus_ctx.c @@ -29,7 +29,7 @@ void push_focus_context(void) { cn_focus_global_context = new_context; } -void initialise_focus_context() { +void initialise_focus_context(void) { push_focus_context(); } @@ -54,7 +54,7 @@ void insert_focus(int64_t index, type_sig sig) { cn_focus_global_context->indices = new_set; } -void clear_focus() { +void clear_focus(void) { focus_set *cur_focus = cn_focus_global_context->indices; while (cur_focus) { focus_set *next = cur_focus->next; @@ -68,34 +68,8 @@ void clear_focus() { /// (i) is in a iterated resource /// (ii) is not focused /// If (i) and (ii), it needs focus, and returns 1. +/// Note: stub — full implementation requires hash_table-based ownership tracking. int needs_focus(uint64_t address, uint64_t size, int64_t *index_out, type_sig *sig_out) { - assert(cn_focus_global_context != NULL); - ownership_ghost_info * info = ownership_ghost_state_get(address); - if (!info) { - return 0; - } - struct cn_res* res_info = info->res_info_stack->top->cn_res_info; - - if (res_info->type != CN_RES_ITER) { - return 0; - } - struct iter_res* res = &res_info->iter_res; - - int64_t offset = address - res->ptr; - uint64_t index = offset / res->size; - - // Case: an appropriate iterated resource is found - // (ii) search for focus - focus_set *cur_focus = cn_focus_global_context->indices; - while (cur_focus) { - if (cur_focus->info.index == index && - strcmp(cur_focus->info.sig, res->sig) == 0) { - return 0; - } - cur_focus = cur_focus->next; - } - // The index is not focused - *index_out = index; - *sig_out = res->sig; - return 1; + (void)address; (void)size; (void)index_out; (void)sig_out; + return 0; }