summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore4
-rw-r--r--Makefile35
-rw-r--r--TODO.md2
-rw-r--r--src/Collections.ml14
-rw-r--r--src/Contexts.ml5
-rw-r--r--src/Crates.ml (renamed from src/Modules.ml)12
-rw-r--r--src/FunsAnalysis.ml4
-rw-r--r--src/Interpreter.ml31
-rw-r--r--src/InterpreterPaths.ml1
-rw-r--r--src/InterpreterStatements.ml20
-rw-r--r--src/LlbcOfJson.ml27
-rw-r--r--src/PrePasses.ml3
-rw-r--r--src/Print.ml11
-rw-r--r--src/PrintSymbolicAst.ml1
-rw-r--r--src/SymbolicToPure.ml1
-rw-r--r--src/Translate.ml51
-rw-r--r--src/TranslateCore.ml1
-rw-r--r--src/TypesAnalysis.ml2
-rw-r--r--src/main.ml2
-rw-r--r--tests/betree/BetreeMain.Clauses.Template.fst2
-rw-r--r--tests/betree/BetreeMain.Funs.fst2
-rw-r--r--tests/betree/BetreeMain.Types.fsti2
-rw-r--r--tests/hashmap/Hashmap.Clauses.Template.fst2
-rw-r--r--tests/hashmap/Hashmap.Funs.fst2
-rw-r--r--tests/hashmap/Hashmap.Types.fst2
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst2
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Funs.fst2
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Types.fsti2
-rw-r--r--tests/misc/BetreePolonius.fst (renamed from tests/misc/BetreeNll.fst)10
-rw-r--r--tests/misc/Constants.fst2
30 files changed, 145 insertions, 112 deletions
diff --git a/.gitignore b/.gitignore
index a90aa1fc..8713e6e4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -34,6 +34,10 @@ rust-tests/target/
# F*
.depend
*.hints
+tests/betree/obj/
+tests/hashmap/obj/
+tests/hashmap_on_disk/obj/
+tests/misc/obj/
# Misc
/fstar-tests
diff --git a/Makefile b/Makefile
index e92b2b9b..c59aec01 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@ ifeq (3.81,$(MAKE_VERSION))
install make, then invoke gmake instead of make)
endif
-all: build-test-verify
+all: build-tests-verify
CHARON_HOME = ../charon
CHARON_EXEC = $(CHARON_HOME)/charon
@@ -25,7 +25,7 @@ SUBDIR :=
# Build the project, test it and verify the generated files
.PHONY: build-test-verify
-build-test-verify: build test verify
+build-tests-verify: build tests verify
# Build the project
.PHONY: build
@@ -33,15 +33,15 @@ build:
dune build src/main.exe
# Test the project by translating test files to F*
-.PHONY: test
-test: build trans-no_nested_borrows trans-paper \
+.PHONY: tests
+tests: build trans-no_nested_borrows trans-paper \
trans-hashmap trans-hashmap_main \
trans-external trans-constants \
- trans-nll-betree_nll trans-nll-betree_main
+ trans-polonius-betree_polonius trans-polonius-betree_main
# Verify the F* files generated by the translation
.PHONY: verify
-verify: build test
+verify: build tests
cd tests && $(MAKE) all
# Reformat the project
@@ -60,8 +60,8 @@ trans-hashmap: SUBDIR:=hashmap
trans-hashmap_main: TRANS_OPTIONS += -template-clauses
trans-hashmap_main: SUBDIR:=hashmap_on_disk
-trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
-trans-nll-betree_nll: SUBDIR:=misc
+trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
+trans-polonius-betree_polonius: SUBDIR:=misc
trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
trans-constants: SUBDIR:=misc
@@ -69,26 +69,31 @@ trans-constants: SUBDIR:=misc
trans-external: TRANS_OPTIONS +=
trans-external: SUBDIR:=misc
-trans-nll-betree_main: TRANS_OPTIONS += -template-clauses
-trans-nll-betree_main: SUBDIR:=betree
+trans-polonius-betree_main: TRANS_OPTIONS += -template-clauses
+trans-polonius-betree_main: SUBDIR:=betree
# Generic rules to extract the LLBC from a rust file
# We use the rules in Charon's Makefile to generate the .llbc files: the options
# vary with the test files.
+.PHONY: gen-llbc-polonius-%
+gen-llbc-polonius-%: build
+ cd $(CHARON_HOME)/tests-polonius && $(MAKE) test-$*
+
.PHONY: gen-llbc-%
gen-llbc-%: build
- cd $(CHARON_HOME) && $(MAKE) test-$*
+ cd $(CHARON_HOME)/tests && $(MAKE) test-$*
# Generic rule to test the translation of an LLBC file.
-# Note that the non-linear lifetime files are generated in the tests-nll subdirectory.
+# Note that the files requiring the Polonius borrow-checker are generated
+# in the tests-polonius subdirectory.
.PHONY: trans-%
trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
-trans-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc
+trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
-trans-%: gen-llbc-%
+trans-polonius-%: gen-llbc-polonius-%
dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
-trans-nll-%: gen-llbc-nll-%
+trans-%: gen-llbc-%
dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
.PHONY: doc
diff --git a/TODO.md b/TODO.md
index 37d35138..39a16cdd 100644
--- a/TODO.md
+++ b/TODO.md
@@ -78,7 +78,7 @@
6. add `mvalue` (meta values) stored in abstractions when ending loans
-8. The following doesn't work:
+8. The following doesn't work (if we don't expand the symbolic values):
```
fn f1<'c, T>(p : (&'c mut T, &'c mut T)) -> (&'c mut T, &'c mut T)
diff --git a/src/Collections.ml b/src/Collections.ml
index 2cb298a7..351b6523 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -184,6 +184,7 @@ module type Set = sig
val pp : Format.formatter -> t -> unit
val show : t -> string
+ val pairwise_distinct : elt list -> bool
end
module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
@@ -218,6 +219,19 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
pp_string "}"
let show s = to_string None s
+
+ let pairwise_distinct ls =
+ let s = ref empty in
+ let rec check ls =
+ match ls with
+ | [] -> true
+ | x :: ls' ->
+ if mem x !s then false
+ else (
+ s := add x !s;
+ check ls')
+ in
+ check ls
end
(** A map where the bindings are injective (i.e., if two keys are distinct,
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 716326cf..07535e06 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -3,7 +3,6 @@ open Values
open LlbcAst
module V = Values
open ValuesUtils
-module M = Modules
(** Some global counters.
*
@@ -210,7 +209,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) :
}
type type_context = {
- type_decls_groups : M.type_declaration_group TypeDeclId.Map.t;
+ type_decls_groups : Crates.type_declaration_group TypeDeclId.Map.t;
type_decls : type_decl TypeDeclId.Map.t;
type_infos : TypesAnalysis.type_infos;
}
@@ -391,7 +390,7 @@ let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs =
let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
let decl_group = TypeDeclId.Map.find id ctx.type_context.type_decls_groups in
- match decl_group with M.Rec _ -> true | M.NonRec _ -> false
+ match decl_group with Crates.Rec _ -> true | Crates.NonRec _ -> false
(** Visitor to iterate over the values in the *current* frame *)
class ['self] iter_frame =
diff --git a/src/Modules.ml b/src/Crates.ml
index 7f372d09..844afb94 100644
--- a/src/Modules.ml
+++ b/src/Crates.ml
@@ -16,33 +16,33 @@ type declaration_group =
| Global of GlobalDeclId.id
[@@deriving show]
-type llbc_module = {
+type llbc_crate = {
name : string;
declarations : declaration_group list;
types : type_decl list;
functions : fun_decl list;
globals : global_decl list;
}
-(** LLBC module - TODO: rename to crate *)
+(** LLBC crate *)
-let compute_defs_maps (m : llbc_module) :
+let compute_defs_maps (c : llbc_crate) :
type_decl TypeDeclId.Map.t
* fun_decl FunDeclId.Map.t
* global_decl GlobalDeclId.Map.t =
let types_map =
List.fold_left
(fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
- TypeDeclId.Map.empty m.types
+ TypeDeclId.Map.empty c.types
in
let funs_map =
List.fold_left
(fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m)
- FunDeclId.Map.empty m.functions
+ FunDeclId.Map.empty c.functions
in
let globals_map =
List.fold_left
(fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m)
- GlobalDeclId.Map.empty m.globals
+ GlobalDeclId.Map.empty c.globals
in
(types_map, funs_map, globals_map)
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index 615f45b3..248ad8b3 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -8,7 +8,7 @@
*)
open LlbcAst
-open Modules
+open Crates
module EU = ExpressionsUtils
type fun_info = {
@@ -26,7 +26,7 @@ type fun_info = {
type modules_funs_info = fun_info FunDeclId.Map.t
(** Various information about a module's functions *)
-let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
+let analyze_module (m : llbc_crate) (funs_map : fun_decl FunDeclId.Map.t)
(globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) :
modules_funs_info =
let infos = ref FunDeclId.Map.empty in
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 3a2939ef..9308fa16 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -7,18 +7,17 @@ open LlbcAstUtils
module L = Logging
module T = Types
module A = LlbcAst
-module M = Modules
module SA = SymbolicAst
(** The local logger *)
let log = L.interpreter_log
-let compute_type_fun_global_contexts (m : M.llbc_module) :
+let compute_type_fun_global_contexts (m : Crates.llbc_crate) :
C.type_context * C.fun_context * C.global_context =
- let type_decls_list, _, _ = M.split_declarations m.declarations in
- let type_decls, fun_decls, global_decls = M.compute_defs_maps m in
+ let type_decls_list, _, _ = Crates.split_declarations m.declarations in
+ let type_decls, fun_decls, global_decls = Crates.compute_defs_maps m in
let type_decls_groups, _funs_defs_groups, _globals_defs_groups =
- M.split_declarations_to_group_maps m.declarations
+ Crates.split_declarations_to_group_maps m.declarations
in
let type_infos =
TypesAnalysis.analyze_type_declarations type_decls type_decls_list
@@ -277,10 +276,10 @@ module Test = struct
(** Test a unit function (taking no arguments) by evaluating it in an empty
environment.
*)
- let test_unit_function (config : C.partial_config) (m : M.llbc_module)
+ let test_unit_function (config : C.partial_config) (crate : Crates.llbc_crate)
(fid : A.FunDeclId.id) : unit =
(* Retrieve the function declaration *)
- let fdef = A.FunDeclId.nth m.functions fid in
+ let fdef = A.FunDeclId.nth crate.functions fid in
let body = Option.get fdef.body in
(* Debug *)
@@ -294,7 +293,7 @@ module Test = struct
(* Create the evaluation context *)
let type_context, fun_context, global_context =
- compute_type_fun_global_contexts m
+ compute_type_fun_global_contexts crate
in
let ctx =
initialize_eval_context type_context fun_context global_context []
@@ -332,11 +331,11 @@ module Test = struct
&& List.length def.A.signature.inputs = 0
(** Test all the unit functions in a list of function definitions *)
- let test_unit_functions (config : C.partial_config) (m : M.llbc_module) : unit
- =
- let unit_funs = List.filter fun_decl_is_transparent_unit m.functions in
+ let test_unit_functions (config : C.partial_config)
+ (crate : Crates.llbc_crate) : unit =
+ let unit_funs = List.filter fun_decl_is_transparent_unit crate.functions in
let test_unit_fun (def : A.fun_decl) : unit =
- test_unit_function config m def.A.def_id
+ test_unit_function config crate def.A.def_id
in
List.iter test_unit_fun unit_funs
@@ -374,15 +373,17 @@ module Test = struct
they are not supported by the symbolic interpreter.
*)
let test_functions_symbolic (config : C.partial_config) (synthesize : bool)
- (m : M.llbc_module) : unit =
+ (crate : Crates.llbc_crate) : unit =
(* Filter the functions which contain loops *)
let no_loop_funs =
- List.filter (fun f -> not (LlbcAstUtils.fun_decl_has_loops f)) m.functions
+ List.filter
+ (fun f -> not (LlbcAstUtils.fun_decl_has_loops f))
+ crate.functions
in
(* Filter the opaque functions *)
let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in
let type_context, fun_context, global_context =
- compute_type_fun_global_contexts m
+ compute_type_fun_global_contexts crate
in
let test_fun (def : A.fun_decl) : unit =
(* Execute the function - note that as the symbolic interpreter explores
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index edd27138..16ab9aad 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -771,6 +771,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
[end_borrows]: if false, we only end the outer loans we find. If true, we
end all the loans and the borrows we find.
+ TODO: end_borrows is not necessary anymore.
*)
let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place)
(cf : V.typed_value -> m_fun) : m_fun =
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 34310ea1..ae9e59fe 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -20,20 +20,32 @@ open InterpreterExpressions
(** The local logger *)
let log = L.statements_log
-(** Drop a value at a given place *)
+(** Drop a value at a given place - TODO: factorize this with [assign_to_place] *)
let drop_value (config : C.config) (p : E.place) : cm_fun =
fun cf ctx ->
- log#ldebug (lazy ("drop_value: place: " ^ place_to_string ctx p));
- (* Prepare the place (by ending the outer loans and the borrows).
+ log#ldebug
+ (lazy
+ ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n"
+ ^ eval_ctx_to_string ctx));
+ (* Prepare the place (by ending the outer loans).
* Note that [prepare_lplace] will use the `Write` access kind:
* it is ok, because when updating the value with [Bottom] below,
* we will use the `Move` access *)
- let end_borrows = true in
+ let end_borrows = false in
let prepare = prepare_lplace config end_borrows p in
(* Replace the value with [Bottom] *)
let replace cf (v : V.typed_value) ctx =
+ (* Move the value at destination (that we will overwrite) to a dummy variable
+ * to preserve the borrows *)
+ let mv = read_place_unwrap config Write p ctx in
+ let ctx = C.ctx_push_dummy_var ctx mv in
+ (* Update the destination to ⊥ *)
let nv = { v with value = V.Bottom } in
let ctx = write_place_unwrap config Move p nv ctx in
+ log#ldebug
+ (lazy
+ ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Final context:\n"
+ ^ eval_ctx_to_string ctx));
cf ctx
in
(* Compose and apply *)
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 4e10c642..44abedf2 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -14,7 +14,6 @@ open OfJsonBasic
module T = Types
module V = Values
module S = Scalars
-module M = Modules
module E = Expressions
module A = LlbcAst
module TU = TypesUtils
@@ -680,24 +679,24 @@ let global_decl_of_json (js : json) (gid_conv : global_id_converter) :
| _ -> Error "")
let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
- (js : json) : ('id M.g_declaration_group, string) result =
+ (js : json) : ('id Crates.g_declaration_group, string) result =
combine_error_msgs js "g_declaration_group_of_json"
(match js with
| `Assoc [ ("NonRec", `List [ id ]) ] ->
let* id = id_of_json id in
- Ok (M.NonRec id)
+ Ok (Crates.NonRec id)
| `Assoc [ ("Rec", `List [ ids ]) ] ->
let* ids = list_of_json id_of_json ids in
- Ok (M.Rec ids)
+ Ok (Crates.Rec ids)
| _ -> Error "")
let type_declaration_group_of_json (js : json) :
- (M.type_declaration_group, string) result =
+ (Crates.type_declaration_group, string) result =
combine_error_msgs js "type_declaration_group_of_json"
(g_declaration_group_of_json T.TypeDeclId.id_of_json js)
let fun_declaration_group_of_json (js : json) :
- (M.fun_declaration_group, string) result =
+ (Crates.fun_declaration_group, string) result =
combine_error_msgs js "fun_declaration_group_of_json"
(g_declaration_group_of_json A.FunDeclId.id_of_json js)
@@ -711,19 +710,19 @@ let global_declaration_group_of_json (js : json) :
| `Assoc [ ("Rec", `List [ _ ]) ] -> Error "got mutually dependent globals"
| _ -> Error "")
-let declaration_group_of_json (js : json) : (M.declaration_group, string) result
- =
+let declaration_group_of_json (js : json) :
+ (Crates.declaration_group, string) result =
combine_error_msgs js "declaration_of_json"
(match js with
| `Assoc [ ("Type", `List [ decl ]) ] ->
let* decl = type_declaration_group_of_json decl in
- Ok (M.Type decl)
+ Ok (Crates.Type decl)
| `Assoc [ ("Fun", `List [ decl ]) ] ->
let* decl = fun_declaration_group_of_json decl in
- Ok (M.Fun decl)
+ Ok (Crates.Fun decl)
| `Assoc [ ("Global", `List [ decl ]) ] ->
let* id = global_declaration_group_of_json decl in
- Ok (M.Global id)
+ Ok (Crates.Global id)
| _ -> Error "")
let length_of_json_list (js : json) : (int, string) result =
@@ -732,8 +731,8 @@ let length_of_json_list (js : json) : (int, string) result =
| `List jsl -> Ok (List.length jsl)
| _ -> Error ("not a list: " ^ show js))
-let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
- combine_error_msgs js "llbc_module_of_json"
+let llbc_crate_of_json (js : json) : (Crates.llbc_crate, string) result =
+ combine_error_msgs js "llbc_crate_of_json"
(match js with
| `Assoc
[
@@ -763,7 +762,7 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
let globals, global_bodies = List.split globals in
Ok
{
- M.name;
+ Crates.name;
declarations;
types;
functions = functions @ global_bodies;
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index c9d496ea..3159907e 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -7,7 +7,6 @@ module V = Values
module E = Expressions
module C = Contexts
module A = LlbcAst
-module M = Modules
module L = Logging
let log = L.pre_passes_log
@@ -50,6 +49,6 @@ let filter_drop_assigns (f : A.fun_decl) : A.fun_decl =
in
{ f with body }
-let apply_passes (m : M.llbc_module) : M.llbc_module =
+let apply_passes (m : Crates.llbc_crate) : Crates.llbc_crate =
let functions = List.map filter_drop_assigns m.functions in
{ m with functions }
diff --git a/src/Print.ml b/src/Print.ml
index c10c5989..1439a74d 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -6,7 +6,6 @@ module VU = ValuesUtils
module E = Expressions
module A = LlbcAst
module C = Contexts
-module M = Modules
let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
@@ -1194,19 +1193,21 @@ module Module = struct
in
PA.fun_decl_to_string fmt "" " " def
- let module_to_string (m : M.llbc_module) : string =
+ let module_to_string (m : Crates.llbc_crate) : string =
let types_defs_map, funs_defs_map, globals_defs_map =
- M.compute_defs_maps m
+ Crates.compute_defs_maps m
in
(* The types *)
- let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in
+ let type_decls =
+ List.map (type_decl_to_string types_defs_map) m.Crates.types
+ in
(* The functions *)
let fun_decls =
List.map
(fun_decl_to_string types_defs_map funs_defs_map globals_defs_map)
- m.M.functions
+ m.Crates.functions
in
(* Put everything together *)
diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml
index e44b422a..37b7555e 100644
--- a/src/PrintSymbolicAst.ml
+++ b/src/PrintSymbolicAst.ml
@@ -14,7 +14,6 @@ module V = Values
module E = Expressions
module A = LlbcAst
module C = Contexts
-module M = Modules
open SymbolicAst
module P = Print
module PT = Print.Types
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index f321ce8c..77c5e0e8 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -3,7 +3,6 @@ open LlbcAstUtils
open Pure
open PureUtils
module Id = Identifiers
-module M = Modules
module S = SymbolicAst
module TA = TypesAnalysis
module L = Logging
diff --git a/src/Translate.ml b/src/Translate.ml
index 61300ed8..8024d910 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -3,7 +3,6 @@ open Interpreter
module L = Logging
module T = Types
module A = LlbcAst
-module M = Modules
module SA = SymbolicAst
module Micro = PureMicroPasses
open PureUtils
@@ -286,24 +285,24 @@ let translate_function_to_pure (config : C.partial_config)
(pure_forward, pure_backwards)
let translate_module_to_pure (config : C.partial_config)
- (mp_config : Micro.config) (use_state : bool) (m : M.llbc_module) :
+ (mp_config : Micro.config) (use_state : bool) (crate : Crates.llbc_crate) :
trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
(* Debug *)
log#ldebug (lazy "translate_module_to_pure");
(* Compute the type and function contexts *)
let type_context, fun_context, global_context =
- compute_type_fun_global_contexts m
+ compute_type_fun_global_contexts crate
in
let fun_infos =
- FA.analyze_module m fun_context.C.fun_decls global_context.C.global_decls
- use_state
+ FA.analyze_module crate fun_context.C.fun_decls
+ global_context.C.global_decls use_state
in
let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in
let trans_ctx = { type_context; fun_context; global_context } in
(* Translate all the type definitions *)
- let type_decls = SymbolicToPure.translate_type_decls m.types in
+ let type_decls = SymbolicToPure.translate_type_decls crate.types in
(* Compute the type definition map *)
let type_decls_map =
@@ -330,7 +329,7 @@ let translate_module_to_pure (config : C.partial_config)
(LlbcAstUtils.fun_body_get_input_vars body)
in
(A.Regular fdef.def_id, input_names, fdef.signature))
- m.functions
+ crate.functions
in
let sigs = List.append assumed_sigs local_sigs in
let fun_sigs =
@@ -343,7 +342,7 @@ let translate_module_to_pure (config : C.partial_config)
List.map
(translate_function_to_pure config mp_config trans_ctx fun_sigs
type_decls_map)
- m.functions
+ crate.functions
in
(* Apply the micro-passes *)
@@ -357,7 +356,7 @@ let translate_module_to_pure (config : C.partial_config)
(trans_ctx, type_decls, pure_translations)
type gen_ctx = {
- m : M.llbc_module;
+ crate : Crates.llbc_crate;
extract_ctx : PureToExtract.extraction_ctx;
trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t;
@@ -534,7 +533,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
ExtractToFStar.extract_state_type fmt ctx.extract_ctx qualif
in
- let export_decl (decl : M.declaration_group) : unit =
+ let export_decl (decl : Crates.declaration_group) : unit =
match decl with
| Type (NonRec id) ->
if config.extract_types then export_type ExtractToFStar.Type id
@@ -574,7 +573,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
*)
if config.extract_state_type && config.extract_fun_decls then
export_state_type ();
- List.iter export_decl ctx.m.declarations;
+ List.iter export_decl ctx.crate.declarations;
if config.extract_state_type && not config.extract_fun_decls then
export_state_type ()
@@ -628,11 +627,11 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
TODO: rename to translate_crate
*)
let translate_module (filename : string) (dest_dir : string) (config : config)
- (m : M.llbc_module) : unit =
+ (crate : Crates.llbc_crate) : unit =
(* Translate the module to the pure AST *)
let trans_ctx, trans_types, trans_funs =
translate_module_to_pure config.eval_config config.mp_config
- config.use_state m
+ config.use_state crate
in
(* Initialize the extraction context - for now we extract only to F* *)
@@ -641,7 +640,8 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
in
let variant_concatenate_type_name = true in
let fstar_fmt =
- ExtractToFStar.mk_formatter trans_ctx m.name variant_concatenate_type_name
+ ExtractToFStar.mk_formatter trans_ctx crate.name
+ variant_concatenate_type_name
in
let ctx =
{ PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
@@ -653,8 +653,9 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
A.FunDeclId.Set.of_list
(List.concat
(List.map
- (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> [])
- m.declarations))
+ (fun decl ->
+ match decl with Crates.Fun (Rec ids) -> ids | _ -> [])
+ crate.declarations))
in
(* Register unique names for all the top-level types, globals and functions.
@@ -686,7 +687,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
let ctx =
List.fold_left ExtractToFStar.extract_global_decl_register_names ctx
- m.globals
+ crate.globals
in
(* Open the output file *)
@@ -746,7 +747,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(* Extract the file(s) *)
let gen_ctx =
{
- m;
+ crate;
extract_ctx = ctx;
trans_types;
trans_funs;
@@ -793,8 +794,8 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
interface = has_opaque_types;
}
in
- extract_file types_config gen_ctx types_filename m.M.name types_module
- ": type definitions" [] [];
+ extract_file types_config gen_ctx types_filename crate.Crates.name
+ types_module ": type definitions" [] [];
(* Extract the template clauses *)
let needs_clauses_module =
@@ -807,7 +808,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
let clauses_config =
{ base_gen_config with extract_template_decreases_clauses = true }
in
- extract_file clauses_config gen_ctx clauses_filename m.M.name
+ extract_file clauses_config gen_ctx clauses_filename crate.Crates.name
clauses_module ": templates for the decreases clauses" [ types_module ]
[]);
@@ -825,7 +826,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
interface = true;
}
in
- extract_file opaque_config gen_ctx opaque_filename m.M.name
+ extract_file opaque_config gen_ctx opaque_filename crate.Crates.name
opaque_module ": opaque function definitions" [] [ types_module ];
[ opaque_module ])
else []
@@ -844,7 +845,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
let clauses_module =
if needs_clauses_module then [ module_name ^ ".Clauses" ] else []
in
- extract_file fun_config gen_ctx fun_filename m.M.name fun_module
+ extract_file fun_config gen_ctx fun_filename crate.Crates.name fun_module
": function definitions" []
([ types_module ] @ opaque_funs_module @ clauses_module))
else
@@ -866,5 +867,5 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
in
(* Add the extension for F* *)
let extract_filename = extract_filebasename ^ ".fst" in
- extract_file gen_config gen_ctx extract_filename m.M.name module_name "" []
- []
+ extract_file gen_config gen_ctx extract_filename crate.Crates.name
+ module_name "" [] []
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 326bb05f..a658147d 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -4,7 +4,6 @@ open InterpreterStatements
module L = Logging
module T = Types
module A = LlbcAst
-module M = Modules
module SA = SymbolicAst
module FA = FunsAnalysis
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml
index e84b4f58..0d23e92b 100644
--- a/src/TypesAnalysis.ml
+++ b/src/TypesAnalysis.ml
@@ -1,5 +1,5 @@
open Types
-open Modules
+open Crates
type subtype_info = {
under_borrow : bool; (** Are we inside a borrow? *)
diff --git a/src/main.ml b/src/main.ml
index 6b1083f5..b7868722 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -141,7 +141,7 @@ let () =
translate_log#set_level EL.Info;
(* Load the module *)
let json = Yojson.Basic.from_file filename in
- match llbc_module_of_json json with
+ match llbc_crate_of_json json with
| Error s ->
main_log#error "error: %s\n" s;
exit 1
diff --git a/tests/betree/BetreeMain.Clauses.Template.fst b/tests/betree/BetreeMain.Clauses.Template.fst
index c2412775..d48213d3 100644
--- a/tests/betree/BetreeMain.Clauses.Template.fst
+++ b/tests/betree/BetreeMain.Clauses.Template.fst
@@ -6,7 +6,7 @@ open BetreeMain.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [core::num::u64::{9}::MAX] *)
+(** [core::num::u64::{10}::MAX] *)
let core_num_u64_max_body : result u64 = Return 18446744073709551615
let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst
index e80e96a6..9ba5d3e7 100644
--- a/tests/betree/BetreeMain.Funs.fst
+++ b/tests/betree/BetreeMain.Funs.fst
@@ -80,7 +80,7 @@ let betree_node_id_counter_fresh_id_back
| Return i -> Return (Mkbetree_node_id_counter_t i)
end
-(** [core::num::u64::{9}::MAX] *)
+(** [core::num::u64::{10}::MAX] *)
let core_num_u64_max_body : result u64 = Return 18446744073709551615
let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
diff --git a/tests/betree/BetreeMain.Types.fsti b/tests/betree/BetreeMain.Types.fsti
index f0ca1d9e..c81e3302 100644
--- a/tests/betree/BetreeMain.Types.fsti
+++ b/tests/betree/BetreeMain.Types.fsti
@@ -55,7 +55,7 @@ type betree_be_tree_t =
betree_be_tree_root : betree_node_t;
}
-(** [core::num::u64::{9}::MAX] *)
+(** [core::num::u64::{10}::MAX] *)
let core_num_u64_max_body : result u64 = Return 18446744073709551615
let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/hashmap/Hashmap.Clauses.Template.fst
index 2a3d9cb9..3e51c6f1 100644
--- a/tests/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/hashmap/Hashmap.Clauses.Template.fst
@@ -24,7 +24,7 @@ let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t)
(ls : list_t t) : nat =
admit ()
-(** [core::num::u32::{8}::MAX] *)
+(** [core::num::u32::{9}::MAX] *)
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 397ee720..6e67fca4 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -188,7 +188,7 @@ let hash_map_insert_no_resize_fwd_back
end
end
-(** [core::num::u32::{8}::MAX] *)
+(** [core::num::u32::{9}::MAX] *)
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
diff --git a/tests/hashmap/Hashmap.Types.fst b/tests/hashmap/Hashmap.Types.fst
index f81f4185..d53b8a42 100644
--- a/tests/hashmap/Hashmap.Types.fst
+++ b/tests/hashmap/Hashmap.Types.fst
@@ -19,7 +19,7 @@ type hash_map_t (t : Type0) =
hash_map_slots : vec (list_t t);
}
-(** [core::num::u32::{8}::MAX] *)
+(** [core::num::u32::{9}::MAX] *)
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
diff --git a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
index 0cf876d9..55685114 100644
--- a/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Clauses.Template.fst
@@ -24,7 +24,7 @@ let hashmap_hash_map_insert_in_list_decreases (t : Type0) (key : usize)
(value : t) (ls : hashmap_list_t t) : nat =
admit ()
-(** [core::num::u32::{8}::MAX] *)
+(** [core::num::u32::{9}::MAX] *)
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index 83bf80d1..82b44dbd 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -198,7 +198,7 @@ let hashmap_hash_map_insert_no_resize_fwd_back
end
end
-(** [core::num::u32::{8}::MAX] *)
+(** [core::num::u32::{9}::MAX] *)
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
diff --git a/tests/hashmap_on_disk/HashmapMain.Types.fsti b/tests/hashmap_on_disk/HashmapMain.Types.fsti
index 370844db..ce4d6485 100644
--- a/tests/hashmap_on_disk/HashmapMain.Types.fsti
+++ b/tests/hashmap_on_disk/HashmapMain.Types.fsti
@@ -19,7 +19,7 @@ type hashmap_hash_map_t (t : Type0) =
hashmap_hash_map_slots : vec (hashmap_list_t t);
}
-(** [core::num::u32::{8}::MAX] *)
+(** [core::num::u32::{9}::MAX] *)
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreePolonius.fst
index b548a18b..2bac07b6 100644
--- a/tests/misc/BetreeNll.fst
+++ b/tests/misc/BetreePolonius.fst
@@ -1,16 +1,16 @@
(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_nll] *)
-module BetreeNll
+(** [betree_polonius] *)
+module BetreePolonius
open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-(** [betree_nll::List] *)
+(** [betree_polonius::List] *)
type list_t (t : Type0) =
| ListCons : t -> list_t t -> list_t t
| ListNil : list_t t
-(** [betree_nll::get_list_at_x] *)
+(** [betree_polonius::get_list_at_x] *)
let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
begin match ls with
| ListCons hd tl ->
@@ -24,7 +24,7 @@ let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
| ListNil -> Return ListNil
end
-(** [betree_nll::get_list_at_x] *)
+(** [betree_polonius::get_list_at_x] *)
let rec get_list_at_x_back
(ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
begin match ls with
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index 4a9a0e48..884d1778 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -9,7 +9,7 @@ open Primitives
let x0_body : result u32 = Return 0
let x0_c : u32 = eval_global x0_body
-(** [core::num::u32::{8}::MAX] *)
+(** [core::num::u32::{9}::MAX] *)
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body