Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Big cleanup #45

Merged
merged 42 commits into from
Nov 22, 2023
Merged

Big cleanup #45

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
42 commits
Select commit Hold shift + click to select a range
b9f33bd
Remove the 'r type variable from the ty type definition
sonmarcho Nov 12, 2023
0a5859f
Rename some variants
sonmarcho Nov 12, 2023
6ef68fa
Prefix variants related to types with "T"
sonmarcho Nov 12, 2023
746239e
Add the "V" prefix to most variants related to values
sonmarcho Nov 12, 2023
6c88d30
Add RegionsHierarchy.ml
sonmarcho Nov 13, 2023
cb179ba
Make minor modifications
sonmarcho Nov 13, 2023
4192258
Normalize the types when computing the regions hierarchies
sonmarcho Nov 13, 2023
21e3b71
Start updating the name type, cleanup the names and the module abbrevs
sonmarcho Nov 15, 2023
15f1349
Do more cleanup
sonmarcho Nov 15, 2023
e0351ad
Do more cleanup
sonmarcho Nov 15, 2023
a27efd1
Finish propagating the changes to the names and cleaning
sonmarcho Nov 16, 2023
4972f21
Rename Driver.ml to Main.ml
sonmarcho Nov 16, 2023
9ab6a03
Update SymbolicToPure.eliminate_box_functions
sonmarcho Nov 16, 2023
0757cde
Do more cleanup
sonmarcho Nov 16, 2023
4a3779d
Fix a minor issue
sonmarcho Nov 16, 2023
672ceef
Use the name matcher implemented in Charon
sonmarcho Nov 20, 2023
5aa37b3
Fix minor issues
sonmarcho Nov 20, 2023
db58a6b
Fix minor issues
sonmarcho Nov 20, 2023
dcd34ce
Fix issues with the builtin names
sonmarcho Nov 21, 2023
c3b6ad3
Update the standard libraries
sonmarcho Nov 21, 2023
1dbdd9e
Update more names
sonmarcho Nov 21, 2023
00882b8
Make a minor modification
sonmarcho Nov 21, 2023
5e92ae6
Regenerate most of the test files
sonmarcho Nov 21, 2023
46ab0fc
Regenerate the Traits files
sonmarcho Nov 21, 2023
753f7e7
Regenerate the betree files
sonmarcho Nov 21, 2023
f852e1a
Rename PrimitiveValues to Values
sonmarcho Nov 21, 2023
e94cd72
Add an `is_local` field to declarations
sonmarcho Nov 21, 2023
77ba13b
Add span information to the generated code
sonmarcho Nov 21, 2023
d564a01
Make minor updates to the extraction of spans
sonmarcho Nov 21, 2023
137cc73
Regenerate the files
sonmarcho Nov 21, 2023
b916f69
Reorganize the "Extract" files
sonmarcho Nov 21, 2023
42a0a49
Update the generation of names for the parent trait clauses
sonmarcho Nov 21, 2023
66e0535
Improve the generation of parent clause names
sonmarcho Nov 21, 2023
184e27b
Regenerate the files
sonmarcho Nov 21, 2023
ba66f35
Improve further the generation of parent clause/trait clause names
sonmarcho Nov 22, 2023
84a505e
Regenerate the test files
sonmarcho Nov 22, 2023
724ff98
Use NameMatcher.NameMatcherMap instead of associative lists
sonmarcho Nov 22, 2023
4caed6d
Make a minor modification
sonmarcho Nov 22, 2023
5c3a798
Cleanup a bit
sonmarcho Nov 22, 2023
138ba20
Update the flake.lock
sonmarcho Nov 22, 2023
d163bb8
Fix an issue with the nix flake and update the flake.lock
sonmarcho Nov 22, 2023
01cfd89
Update the flake.lock
sonmarcho Nov 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,21 +58,21 @@ build-tests-verify: build tests verify

# Build the project
.PHONY: build
build: build-driver build-lib build-bin-dir doc
build: build-bin build-lib build-bin-dir doc

.PHONY: build-driver
build-driver:
cd compiler && dune build $(AENEAS_DRIVER)
.PHONY: build-bin
build-bin:
cd compiler && dune build

.PHONY: build-lib
build-lib:
cd compiler && dune build aeneas.cmxs

.PHONY: build-bin-dir
build-bin-dir: build-driver build-lib
build-bin-dir: build-bin build-lib
mkdir -p bin
cp -f compiler/_build/default/driver.exe bin/aeneas
cp -f compiler/_build/default/driver.exe bin/aeneas.cmxs
cp -f compiler/_build/default/main.exe bin/aeneas
cp -f compiler/_build/default/main.exe bin/aeneas.cmxs
mkdir -p bin/backends/fstar
mkdir -p bin/backends/coq
cp -rf backends/fstar/*.fst* bin/backends/fstar/
Expand Down
88 changes: 48 additions & 40 deletions backends/coq/Primitives.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -467,14 +467,14 @@ Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result T := Return x.
Definition alloc_boxed_Box_deref_mut_back (T : Type) (_ : T) (x : T) : result T := Return x.

(* Trait instance *)
Definition alloc_boxed_Box_coreOpsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {|
core_ops_deref_Deref_target := Self;
core_ops_deref_Deref_deref := alloc_boxed_Box_deref Self;
|}.

(* Trait instance *)
Definition alloc_boxed_Box_coreOpsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {|
core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreOpsDerefInst Self;
Definition alloc_boxed_Box_coreopsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {|
core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreopsDerefInst Self;
core_ops_deref_DerefMut_deref_mut := alloc_boxed_Box_deref_mut Self;
core_ops_deref_DerefMut_deref_mut_back := alloc_boxed_Box_deref_mut_back Self;
|}.
Expand Down Expand Up @@ -576,7 +576,7 @@ Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T)
else Fail_ Failure).

(* Helper *)
Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result T.
Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize), result T.

(* Helper *)
Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result (alloc_vec_Vec T).
Expand Down Expand Up @@ -620,42 +620,42 @@ Definition core_slice_index_Slice_index
end.

(* [core::slice::index::Range:::get]: forward function *)
Axiom core_slice_index_Range_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)).
Axiom core_slice_index_RangeUsize_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)).

(* [core::slice::index::Range::get_mut]: forward function *)
Axiom core_slice_index_Range_get_mut :
Axiom core_slice_index_RangeUsize_get_mut :
forall (T : Type), core_ops_range_Range usize -> slice T -> result (option (slice T)).

(* [core::slice::index::Range::get_mut]: backward function 0 *)
Axiom core_slice_index_Range_get_mut_back :
Axiom core_slice_index_RangeUsize_get_mut_back :
forall (T : Type), core_ops_range_Range usize -> slice T -> option (slice T) -> result (slice T).

(* [core::slice::index::Range::get_unchecked]: forward function *)
Definition core_slice_index_Range_get_unchecked
Definition core_slice_index_RangeUsize_get_unchecked
(T : Type) :
core_ops_range_Range usize -> const_raw_ptr (slice T) -> result (const_raw_ptr (slice T)) :=
(* Don't know what the model should be - for now we always fail to make
sure code which uses it fails *)
fun _ _ => Fail_ Failure.

(* [core::slice::index::Range::get_unchecked_mut]: forward function *)
Definition core_slice_index_Range_get_unchecked_mut
Definition core_slice_index_RangeUsize_get_unchecked_mut
(T : Type) :
core_ops_range_Range usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr (slice T)) :=
(* Don't know what the model should be - for now we always fail to make
sure code which uses it fails *)
fun _ _ => Fail_ Failure.

(* [core::slice::index::Range::index]: forward function *)
Axiom core_slice_index_Range_index :
Axiom core_slice_index_RangeUsize_index :
forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T).

(* [core::slice::index::Range::index_mut]: forward function *)
Axiom core_slice_index_Range_index_mut :
Axiom core_slice_index_RangeUsize_index_mut :
forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T).

(* [core::slice::index::Range::index_mut]: backward function 0 *)
Axiom core_slice_index_Range_index_mut_back :
Axiom core_slice_index_RangeUsize_index_mut_back :
forall (T : Type), core_ops_range_Range usize -> slice T -> slice T -> result (slice T).

(* [core::slice::index::[T]::index_mut]: forward function *)
Expand Down Expand Up @@ -683,55 +683,55 @@ Axiom core_array_Array_index_mut_back :
forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx)
(a : array T N) (i : Idx) (x : inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output)), result (array T N).

(* Trait implementation: [core::slice::index::[T]] *)
Definition core_slice_index_Slice_coreopsindexIndexInst (T Idx : Type)
(inst : core_slice_index_SliceIndex Idx (slice T)) :
core_ops_index_Index (slice T) Idx := {|
core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output);
core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst;
|}.

(* Trait implementation: [core::slice::index::private_slice_index::Range] *)
Definition core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst
Definition core_slice_index_private_slice_index_SealedRangeUsizeInst
: core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt.

(* Trait implementation: [core::slice::index::Range] *)
Definition core_slice_index_Range_coresliceindexSliceIndexInst (T : Type) :
Definition core_slice_index_SliceIndexRangeUsizeSliceTInst (T : Type) :
core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) := {|
core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst;
core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst;
core_slice_index_SliceIndex_Output := slice T;
core_slice_index_SliceIndex_get := core_slice_index_Range_get T;
core_slice_index_SliceIndex_get_mut := core_slice_index_Range_get_mut T;
core_slice_index_SliceIndex_get_mut_back := core_slice_index_Range_get_mut_back T;
core_slice_index_SliceIndex_get_unchecked := core_slice_index_Range_get_unchecked T;
core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_Range_get_unchecked_mut T;
core_slice_index_SliceIndex_index := core_slice_index_Range_index T;
core_slice_index_SliceIndex_index_mut := core_slice_index_Range_index_mut T;
core_slice_index_SliceIndex_index_mut_back := core_slice_index_Range_index_mut_back T;
core_slice_index_SliceIndex_get := core_slice_index_RangeUsize_get T;
core_slice_index_SliceIndex_get_mut := core_slice_index_RangeUsize_get_mut T;
core_slice_index_SliceIndex_get_mut_back := core_slice_index_RangeUsize_get_mut_back T;
core_slice_index_SliceIndex_get_unchecked := core_slice_index_RangeUsize_get_unchecked T;
core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_RangeUsize_get_unchecked_mut T;
core_slice_index_SliceIndex_index := core_slice_index_RangeUsize_index T;
core_slice_index_SliceIndex_index_mut := core_slice_index_RangeUsize_index_mut T;
core_slice_index_SliceIndex_index_mut_back := core_slice_index_RangeUsize_index_mut_back T;
|}.

(* Trait implementation: [core::slice::index::[T]] *)
Definition core_ops_index_IndexSliceTIInst (T Idx : Type)
(inst : core_slice_index_SliceIndex Idx (slice T)) :
core_ops_index_Index (slice T) Idx := {|
core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output);
core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst;
|}.

(* Trait implementation: [core::slice::index::[T]] *)
Definition core_slice_index_Slice_coreopsindexIndexMutInst (T Idx : Type)
Definition core_ops_index_IndexMutSliceTIInst (T Idx : Type)
(inst : core_slice_index_SliceIndex Idx (slice T)) :
core_ops_index_IndexMut (slice T) Idx := {|
core_ops_index_IndexMut_indexInst := core_slice_index_Slice_coreopsindexIndexInst T Idx inst;
core_ops_index_IndexMut_indexInst := core_ops_index_IndexSliceTIInst T Idx inst;
core_ops_index_IndexMut_index_mut := core_slice_index_Slice_index_mut T Idx inst;
core_ops_index_IndexMut_index_mut_back := core_slice_index_Slice_index_mut_back T Idx inst;
|}.

(* Trait implementation: [core::array::[T; N]] *)
Definition core_array_Array_coreopsindexIndexInst (T Idx : Type) (N : usize)
Definition core_ops_index_IndexArrayInst (T Idx : Type) (N : usize)
(inst : core_ops_index_Index (slice T) Idx) :
core_ops_index_Index (array T N) Idx := {|
core_ops_index_Index_Output := inst.(core_ops_index_Index_Output);
core_ops_index_Index_index := core_array_Array_index T Idx N inst;
|}.

(* Trait implementation: [core::array::[T; N]] *)
Definition core_array_Array_coreopsindexIndexMutInst (T Idx : Type) (N : usize)
Definition core_ops_index_IndexMutArrayInst (T Idx : Type) (N : usize)
(inst : core_ops_index_IndexMut (slice T) Idx) :
core_ops_index_IndexMut (array T N) Idx := {|
core_ops_index_IndexMut_indexInst := core_array_Array_coreopsindexIndexInst T Idx N inst.(core_ops_index_IndexMut_indexInst);
core_ops_index_IndexMut_indexInst := core_ops_index_IndexArrayInst T Idx N inst.(core_ops_index_IndexMut_indexInst);
core_ops_index_IndexMut_index_mut := core_array_Array_index_mut T Idx N inst;
core_ops_index_IndexMut_index_mut_back := core_array_Array_index_mut_back T Idx N inst;
|}.
Expand Down Expand Up @@ -765,13 +765,13 @@ Axiom core_slice_index_usize_index_mut_back :
forall (T : Type), usize -> slice T -> T -> result (slice T).

(* Trait implementation: [core::slice::index::private_slice_index::usize] *)
Definition core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst
Definition core_slice_index_private_slice_index_SealedUsizeInst
: core_slice_index_private_slice_index_Sealed usize := tt.

(* Trait implementation: [core::slice::index::usize] *)
Definition core_slice_index_usize_coresliceindexSliceIndexInst (T : Type) :
Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) :
core_slice_index_SliceIndex usize (slice T) := {|
core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst;
core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
core_slice_index_SliceIndex_Output := T;
core_slice_index_SliceIndex_get := core_slice_index_usize_get T;
core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut T;
Expand Down Expand Up @@ -815,8 +815,16 @@ Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type)

(*** Theorems *)

Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_usize v i.

Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_usize v i.

Axiom alloc_vec_Vec_index_mut_back_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x =
alloc_vec_Vec_index_mut_back a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i x =
alloc_vec_Vec_update_usize v i x.

End Primitives.
Loading