diff options
Diffstat (limited to '')
| -rw-r--r-- | src/FunsAnalysis.ml | 9 | ||||
| -rw-r--r-- | src/LlbcAst.ml | 8 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 4 | ||||
| -rw-r--r-- | src/PureTypeCheck.ml | 7 | ||||
| -rw-r--r-- | 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 *) |