From fe7949c350bb3c5e2b9990ab3594b256194c3f0b Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Mon, 25 Jul 2022 14:22:52 +0200
Subject: Apply minor changes from PR comments
---
src/FunsAnalysis.ml | 9 +--------
src/LlbcAst.ml | 8 ++++----
src/PureToExtract.ml | 4 ++--
src/PureTypeCheck.ml | 7 ++++++-
src/SymbolicToPure.ml | 12 ++++++++++--
5 files changed, 23 insertions(+), 17 deletions(-)
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index 034575c0..427175de 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -56,12 +56,6 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
inherit [_] iter_statement as super
method may_fail b =
- (* The fail flag is disabled for globals : the global body is
- * normalised into its declaration, which is always successful.
- * (we check that it is successful in the extracted code: if it is
- * not, it leads to a type-checking error in the generated files)
- *)
- if f.is_global_body then () else
can_fail := !can_fail || b
method! visit_Assert env a =
@@ -104,11 +98,10 @@ let analyze_module (m : llbc_module) (funs_map : fun_decl FunDeclId.Map.t)
(* Opaque function *)
obj#may_fail true;
stateful := use_state
- | Some body -> obj#visit_statement () body.body);
+ | Some body -> obj#visit_statement () body.body)
(* We ignore on purpose functions that cannot fail: the result of the analysis
* is not used yet to adjust the translation so that the functions which
* syntactically can't fail don't use an error monad. *)
- can_fail := not f.is_global_body
in
List.iter visit_fun d;
{ can_fail = !can_fail; stateful = !stateful; divergent = !divergent }
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index aa9b0665..94566f9b 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -37,7 +37,7 @@ type assumed_fun_id =
type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
[@@deriving show, ord]
-type assign_global = {
+type global_assignment = {
dst : VarId.id;
global : GlobalDeclId.id;
}
@@ -84,7 +84,7 @@ class ['self] iter_statement_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
- method visit_assign_global : 'env -> assign_global -> unit = fun _ _ -> ()
+ method visit_global_assignment : 'env -> global_assignment -> unit = fun _ _ -> ()
method visit_place : 'env -> place -> unit = fun _ _ -> ()
@@ -108,7 +108,7 @@ class ['self] map_statement_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
- method visit_assign_global : 'env -> assign_global -> assign_global = fun _ x -> x
+ method visit_global_assignment : 'env -> global_assignment -> global_assignment = fun _ x -> x
method visit_place : 'env -> place -> place = fun _ x -> x
@@ -131,7 +131,7 @@ class ['self] map_statement_base =
type statement =
| Assign of place * rvalue
- | AssignGlobal of assign_global
+ | AssignGlobal of global_assignment
| FakeRead of place
| SetDiscriminant of place * VariantId.id
| Drop of place
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 7a10bb6b..2d76f348 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -671,7 +671,7 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
TODO: move all those helpers.
*)
let default_fun_suffix
- (is_global : bool)
+ (is_global_body : bool)
(num_region_groups : int)
(rg : region_group_info option)
((keep_fwd, num_backs) : bool * int)
@@ -691,7 +691,7 @@ let default_fun_suffix
we could not add the "_fwd" suffix) to prevent name clashes between
definitions (in particular between type and function definitions).
*)
- if is_global then "_c" else
+ if is_global_body then "_body" else
match rg with
| None -> "_fwd"
| Some rg ->
diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml
index 90b9ab09..c63814eb 100644
--- a/src/PureTypeCheck.ml
+++ b/src/PureTypeCheck.ml
@@ -40,6 +40,7 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
type tc_ctx = {
type_decls : type_decl TypeDeclId.Map.t; (** The type declarations *)
+ global_decls : A.global_decl A.GlobalDeclId.Map.t; (** The global declarations *)
env : ty VarId.Map.t; (** Environment from variables to types *)
}
@@ -111,7 +112,11 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
check_texpression ctx body
| Qualif qualif -> (
match qualif.id with
- | Func _ | Global _ -> () (* TODO *)
+ | Func _ -> () (* TODO *)
+ | Global id ->
+ let global = A.GlobalDeclId.Map.find id ctx.global_decls in
+ (* TODO: something like assert (global.ty = e.ty) *)
+ failwith "PureTypeCheck.ml:118"
| Proj { adt_id = proj_adt_id; field_id } ->
(* Note we can only project fields of structures (not enumerations) *)
(* Deconstruct the projector type *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 7d9e2906..83cce3e9 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -127,13 +127,21 @@ type bs_ctx = {
let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
let env = VarId.Map.empty in
- let ctx = { PureTypeCheck.type_decls = ctx.type_context.type_decls; env } in
+ let ctx = {
+ PureTypeCheck.type_decls = ctx.type_context.type_decls;
+ global_decls = ctx.global_context.llbc_global_decls;
+ env
+ } in
let _ = PureTypeCheck.check_typed_pattern ctx v in
()
let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
let env = VarId.Map.empty in
- let ctx = { PureTypeCheck.type_decls = ctx.type_context.type_decls; env } in
+ let ctx = {
+ PureTypeCheck.type_decls = ctx.type_context.type_decls;
+ global_decls = ctx.global_context.llbc_global_decls;
+ env
+ } in
PureTypeCheck.check_texpression ctx e
(* TODO: move *)
--
cgit v1.2.3