summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Makefile2
-rw-r--r--src/Contexts.ml11
-rw-r--r--src/Expressions.ml23
-rw-r--r--src/ExtractToFStar.ml3
-rw-r--r--src/FunIdentifier.ml3
-rw-r--r--src/FunsAnalysis.ml1
-rw-r--r--src/Interpreter.ml7
-rw-r--r--src/InterpreterExpressions.ml83
-rw-r--r--src/InterpreterStatements.ml16
-rw-r--r--src/InterpreterUtils.ml2
-rw-r--r--src/LlbcAst.ml27
-rw-r--r--src/LlbcAstUtils.ml1
-rw-r--r--src/LlbcOfJson.ml173
-rw-r--r--src/Modules.ml2
-rw-r--r--src/Print.ml78
-rw-r--r--src/PrintPure.ml7
-rw-r--r--src/Pure.ml3
-rw-r--r--src/PureToExtract.ml13
-rw-r--r--src/Substitute.ml11
-rw-r--r--src/SymbolicToPure.ml27
-rw-r--r--src/Translate.ml36
-rw-r--r--src/TranslateCore.ml10
-rw-r--r--src/main.ml30
-rw-r--r--tests/misc/Constants.fst119
24 files changed, 380 insertions, 308 deletions
diff --git a/Makefile b/Makefile
index 4dc1475b..0fc3fcf4 100644
--- a/Makefile
+++ b/Makefile
@@ -48,7 +48,7 @@ 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-constants: TRANS_OPTIONS += -no-split-files -no-state -no-decreases-clauses
+trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
trans-constants: SUBDIR:=misc
trans-external: TRANS_OPTIONS +=
diff --git a/src/Contexts.ml b/src/Contexts.ml
index bbf5b8f3..1fbc916b 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -1,7 +1,6 @@
open Types
open Values
open LlbcAst
-open FunIdentifier
module V = Values
open ValuesUtils
module M = Modules
@@ -218,7 +217,11 @@ type type_context = {
}
[@@deriving show]
-type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show]
+type fun_context = {
+ fun_decls : fun_decl FunDeclId.Map.t;
+ gid_conv : global_id_converter;
+}
+[@@deriving show]
type eval_ctx = {
type_context : type_context;
@@ -256,6 +259,10 @@ let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
FunDeclId.Map.find fid ctx.fun_context.fun_decls
+(** TODO: make this more efficient with maps *)
+let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : fun_decl =
+ ctx_lookup_fun_decl ctx (global_to_fun_id ctx.fun_context.gid_conv gid)
+
(** Retrieve a variable's value in an environment *)
let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
(* We take care to stop at the end of current frame: different variables
diff --git a/src/Expressions.ml b/src/Expressions.ml
index f1a4a8c3..6645a77f 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -1,6 +1,5 @@
open Types
open Values
-open FunIdentifier
type field_proj_kind =
| ProjAdt of TypeDeclId.id * VariantId.id option
@@ -73,31 +72,11 @@ let all_binops =
Shr;
]
-(** Constant value for an operand
-
- It is a bit annoying, but rustc treats some ADT and tuple instances as
- constants when generating MIR:
- - an enumeration with one variant and no fields is a constant.
- - a structure with no field is a constant.
- - sometimes, Rust stores the initialization of an ADT as a constant
- (if all the fields are constant) rather than as an aggregated value
-
- For our translation, we use the following enumeration to encode those
- special cases in assignments. They are converted to "normal" values
- when evaluating the assignment (which is why we don't put them in the
- [ConstantValue] enumeration).
- *)
-type operand_constant_value =
- | ConstantValue of constant_value
- | ConstantId of FunDeclId.id
- | ConstantAdt of VariantId.id option * operand_constant_value list
-[@@deriving show]
-
(* TODO: symplify the operand constant values *)
type operand =
| Copy of place
| Move of place
- | Constant of ety * operand_constant_value
+ | Constant of ety * constant_value
[@@deriving show]
(** An aggregated ADT.
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index b85c146b..b89579b5 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -6,7 +6,6 @@ open PureUtils
open TranslateCore
open PureToExtract
open StringUtils
-open FunIdentifier
module F = Format
(** A qualifier for a type definition.
@@ -315,7 +314,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
fname ^ suffix
in
- let decreases_clause_name (_fid : FunDeclId.id) (fname : fun_name) : string =
+ let decreases_clause_name (_fid : A.FunDeclId.id) (fname : fun_name) : string =
let fname = fun_name_to_snake_case fname in
(* Compute the suffix *)
let suffix = "_decreases" in
diff --git a/src/FunIdentifier.ml b/src/FunIdentifier.ml
deleted file mode 100644
index 956fce3f..00000000
--- a/src/FunIdentifier.ml
+++ /dev/null
@@ -1,3 +0,0 @@
-open Identifiers
-module FunDeclId = IdGen ()
-module GlobalDeclId = IdGen ()
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index cf2e0bd6..dc205eb9 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -9,7 +9,6 @@
open LlbcAst
open Modules
-open FunIdentifier
type fun_info = {
can_fail : bool;
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 702aeea6..5affea4c 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1,5 +1,4 @@
open Cps
-open FunIdentifier
open InterpreterUtils
open InterpreterProjectors
open InterpreterBorrows
@@ -25,7 +24,7 @@ let compute_type_fun_contexts (m : M.llbc_module) :
TypesAnalysis.analyze_type_declarations type_decls type_decls_list
in
let type_context = { C.type_decls_groups; type_decls; type_infos } in
- let fun_context = { C.fun_decls } in
+ let fun_context = { C.fun_decls; gid_conv = m.gid_conv } in
(type_context, fun_context)
let initialize_eval_context (type_context : C.type_context)
@@ -256,9 +255,9 @@ module Test = struct
environment.
*)
let test_unit_function (config : C.partial_config) (m : M.llbc_module)
- (fid : FunDeclId.id) : unit =
+ (fid : A.FunDeclId.id) : unit =
(* Retrieve the function declaration *)
- let fdef = FunDeclId.nth m.functions fid in
+ let fdef = A.FunDeclId.nth m.functions fid in
let body = Option.get fdef.body in
(* Debug *)
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index ee26d00d..57ee0526 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -71,68 +71,23 @@ let prepare_rplace (config : C.config) (expand_prim_copy : bool)
in
comp cc read_place cf ctx
-(** Convert an operand constant operand value to a typed value *)
-let rec eval_operand_constant_value (ty : T.ety)
- (cv : E.operand_constant_value) (cf : V.typed_value -> m_fun) : m_fun =
- fun ctx ->
- (* Check the type while converting - we actually need some information
- * contained in the type *)
- log#ldebug
- (lazy
- ("eval_operand_constant_value:" ^ "\n- ty: "
- ^ ety_to_string ctx ty ^ "\n- cv: "
- ^ operand_constant_value_to_string ctx cv));
- match (ty, cv) with
- (* Adt *)
- | ( T.Adt (adt_id, region_params, type_params),
- ConstantAdt (variant_id, field_values) ) ->
- assert (region_params = []);
- (* Compute the types of the fields *)
- let field_tys =
- match adt_id with
- | T.AdtId def_id ->
- let def = C.ctx_lookup_type_decl ctx def_id in
- assert (def.region_params = []);
- Subst.type_decl_get_instantiated_field_etypes def variant_id
- type_params
- | T.Tuple -> type_params
- | T.Assumed _ -> failwith "Unreachable"
- in
- let adt_cf = fun fields ctx ->
- let value = V.Adt { variant_id; field_values = fields } in
- cf { value; ty } ctx
- in
- (* Map the field values & types to the continuation above *)
- fold_left_apply_continuation
- (fun (ty, v) cf ctx -> eval_operand_constant_value ty v cf ctx)
- (List.combine field_tys field_values)
- adt_cf ctx
- (* Scalar, boolean... *)
- | T.Bool, ConstantValue (Bool v) -> cf { V.value = V.Concrete (Bool v); ty } ctx
- | T.Char, ConstantValue (Char v) -> cf { V.value = V.Concrete (Char v); ty } ctx
- | T.Str, ConstantValue (String v) -> cf { V.value = V.Concrete (String v); ty } ctx
- | T.Integer int_ty, ConstantValue (V.Scalar v) ->
- (* Check the type and the ranges *)
- assert (int_ty = v.int_ty);
- assert (check_scalar_value_in_range v);
- cf { V.value = V.Concrete (V.Scalar v); ty } ctx
- (* Constant expression identifier *)
- | ty, ConstantId id ->
- let dest = mk_fresh_symbolic_value V.FunCallRet (ety_no_regions_to_rty ty) in
-
- (* Call the continuation *)
- let expr = cf (mk_typed_value_from_symbolic_value dest) ctx in
-
- (* TODO Should it really be a new call ID ? *)
- let call = SA.Fun (LA.Regular id, C.fresh_fun_call_id ()) in
-
- S.synthesize_function_call call [] [] [] []
- dest None(*TODO meta-info*) expr
-
- (* Remaining cases (invalid) - listing as much as we can on purpose
- (allows to catch errors at compilation if the definitions change) *)
- | _, ConstantAdt _ | _, ConstantValue _ ->
- failwith "Improperly typed constant value"
+(** Convert a constant operand value to a typed value *)
+let typecheck_constant_value (ty : T.ety) (cv : V.constant_value) : V.typed_value =
+ (* Check the type while converting -
+ * we actually need some information contained in the type *)
+ match (ty, cv) with
+ (* Scalar, boolean... *)
+ | T.Bool, (Bool v) -> { V.value = V.Concrete (Bool v); ty }
+ | T.Char, (Char v) -> { V.value = V.Concrete (Char v); ty }
+ | T.Str, (String v) -> { V.value = V.Concrete (String v); ty }
+ | T.Integer int_ty, (V.Scalar v) ->
+ (* Check the type and the ranges *)
+ assert (int_ty = v.int_ty);
+ assert (check_scalar_value_in_range v);
+ { V.value = V.Concrete (V.Scalar v); ty }
+ (* Remaining cases (invalid) - listing as much as we can on purpose
+ (allows to catch errors at compilation if the definitions change) *)
+ | _, _ -> failwith "Improperly typed constant value"
(** Prepare the evaluation of an operand.
@@ -172,7 +127,7 @@ let eval_operand_prepare (config : C.config) (op : E.operand)
fun ctx ->
match op with
| Expressions.Constant (ty, cv) ->
- eval_operand_constant_value ty cv cf ctx
+ cf (typecheck_constant_value ty cv) ctx
| Expressions.Copy p ->
(* Access the value *)
let access = Read in
@@ -205,7 +160,7 @@ let eval_operand (config : C.config) (op : E.operand)
^ eval_ctx_to_string ctx ^ "\n"));
(* Evaluate *)
match op with
- | Expressions.Constant (ty, cv) -> eval_operand_constant_value ty cv cf ctx
+ | Expressions.Constant (ty, cv) -> cf (typecheck_constant_value ty cv) ctx
| Expressions.Copy p ->
(* Access the value *)
let access = Read in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index c7308720..e5564d59 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -7,7 +7,6 @@ module A = LlbcAst
module L = Logging
open TypesUtils
open ValuesUtils
-open FunIdentifier
module Inv = Invariants
module S = SynthesizeSymbolic
open Errors
@@ -822,6 +821,15 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
(* Compose and apply *)
comp cf_eval_rvalue cf_assign cf ctx
+ | A.AssignGlobal { dst; global } ->
+ let call : A.call = {
+ func = A.Regular (A.global_to_fun_id ctx.fun_context.gid_conv global);
+ region_args = [];
+ type_args = [];
+ args = [];
+ dest = { var_id = dst; projection = [] };
+ } in
+ eval_function_call config call cf ctx
| A.FakeRead p ->
let expand_prim_copy = false in
let cf_prepare = prepare_rplace config expand_prim_copy Read p in
@@ -1002,7 +1010,7 @@ and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
call.args call.dest
(** Evaluate a local (i.e., non-assumed) function call in concrete mode *)
-and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id)
+and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
(region_args : T.erased_region list) (type_args : T.ety list)
(args : E.operand list) (dest : E.place) : st_cm_fun =
fun cf ctx ->
@@ -1080,7 +1088,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : FunDeclId.id)
cc cf ctx
(** Evaluate a local (i.e., non-assumed) function call in symbolic mode *)
-and eval_local_function_call_symbolic (config : C.config) (fid : FunDeclId.id)
+and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDeclId.id)
(region_args : T.erased_region list) (type_args : T.ety list)
(args : E.operand list) (dest : E.place) : st_cm_fun =
fun cf ctx ->
@@ -1301,7 +1309,7 @@ and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
(** Evaluate a local (i.e, not assumed) function call (auxiliary helper for
[eval_statement]) *)
-and eval_local_function_call (config : C.config) (fid : FunDeclId.id)
+and eval_local_function_call (config : C.config) (fid : A.FunDeclId.id)
(region_args : T.erased_region list) (type_args : T.ety list)
(args : E.operand list) (dest : E.place) : st_cm_fun =
match config.mode with
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 7a2e22f7..47323cc2 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -33,8 +33,6 @@ let typed_value_to_string = PA.typed_value_to_string
let typed_avalue_to_string = PA.typed_avalue_to_string
-let operand_constant_value_to_string = PA.operand_constant_value_to_string
-
let place_to_string = PA.place_to_string
let operand_to_string = PA.operand_to_string
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index 4324586d..16733e20 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -2,7 +2,21 @@ open Names
open Types
open Values
open Expressions
-open FunIdentifier
+open Identifiers
+
+module FunDeclId = IdGen ()
+module GlobalDeclId = IdGen ()
+
+(* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
+type global_id_converter = { fun_count : int }
+[@@deriving show]
+
+(** Converts a global id to its corresponding function id.
+ To do so, it adds the global id to the number of function declarations :
+ We have the bijection `global_id <=> fun_id + fun_id_count`.
+*)
+let global_to_fun_id (conv : global_id_converter) (gid : GlobalDeclId.id) : FunDeclId.id =
+ FunDeclId.of_int ((GlobalDeclId.to_int gid) + conv.fun_count)
type var = {
index : VarId.id; (** Unique variable identifier *)
@@ -34,6 +48,12 @@ type assumed_fun_id =
type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
[@@deriving show, ord]
+type assign_global = {
+ dst : VarId.id;
+ global : GlobalDeclId.id;
+}
+[@@deriving show]
+
type assertion = { cond : operand; expected : bool } [@@deriving show]
type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
@@ -75,6 +95,8 @@ class ['self] iter_statement_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
+ method visit_assign_global : 'env -> assign_global -> unit = fun _ _ -> ()
+
method visit_place : 'env -> place -> unit = fun _ _ -> ()
method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
@@ -97,6 +119,8 @@ 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_place : 'env -> place -> place = fun _ x -> x
method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
@@ -118,6 +142,7 @@ class ['self] map_statement_base =
type statement =
| Assign of place * rvalue
+ | AssignGlobal of assign_global
| FakeRead of place
| SetDiscriminant of place * VariantId.id
| Drop of place
diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml
index bc4236cf..84e8e00f 100644
--- a/src/LlbcAstUtils.ml
+++ b/src/LlbcAstUtils.ml
@@ -1,6 +1,5 @@
open LlbcAst
open Utils
-open FunIdentifier
module T = Types
(** Check if a [statement] contains loops *)
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 14333088..a074ed1e 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -11,7 +11,6 @@
open Yojson.Basic
open Names
open OfJsonBasic
-open FunIdentifier
module T = Types
module V = Values
module S = Scalars
@@ -19,6 +18,7 @@ module M = Modules
module E = Expressions
module A = LlbcAst
module TU = TypesUtils
+module AU = LlbcAstUtils
(* The default logger *)
let log = Logging.llbc_of_json_logger
@@ -227,14 +227,6 @@ let type_decl_of_json (js : json) : (T.type_decl, string) result =
}
| _ -> Error "")
-(* Converts a global ID to its corresponding function ID.
- To do so, it adds the global ID to the number of function declarations.
-*)
-let global_id_of_json (js: json) (fun_count: int) : (FunDeclId.id, string) result =
- combine_error_msgs js "global_id_of_json"
- (let* gid = FunDeclId.id_of_json js in
- Ok (FunDeclId.of_int ((FunDeclId.to_int gid) + fun_count)))
-
let var_of_json (js : json) : (A.var, string) result =
combine_error_msgs js "var_of_json"
(match js with
@@ -308,23 +300,6 @@ let scalar_value_of_json (js : json) : (V.scalar_value, string) result =
raise (Failure ("Scalar value not in range: " ^ V.show_scalar_value sv)));
res
-let constant_value_of_json (js : json) : (V.constant_value, string) result =
- combine_error_msgs js "constant_value_of_json"
- (match js with
- | `Assoc [ ("Scalar", scalar_value) ] ->
- let* scalar_value = scalar_value_of_json scalar_value in
- Ok (V.Scalar scalar_value)
- | `Assoc [ ("Bool", v) ] ->
- let* v = bool_of_json v in
- Ok (V.Bool v)
- | `Assoc [ ("Char", v) ] ->
- let* v = char_of_json v in
- Ok (V.Char v)
- | `Assoc [ ("String", v) ] ->
- let* v = string_of_json v in
- Ok (V.String v)
- | _ -> Error "")
-
let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result =
combine_error_msgs js "field_proj_kind_of_json"
(match js with
@@ -403,25 +378,30 @@ let binop_of_json (js : json) : (E.binop, string) result =
| `String "Shr" -> Ok E.Shr
| _ -> Error ("binop_of_json failed on:" ^ show js)
-let rec operand_constant_value_of_json (js : json) (fun_count : int) :
- (E.operand_constant_value, string) result =
- combine_error_msgs js "operand_constant_value_of_json"
+let constant_value_of_json (js : json) : (V.constant_value, string) result =
+ combine_error_msgs js "constant_value_of_json"
(match js with
+ (* This indirection is because Charon still export the type OperandConstantValue,
+ * which had other variants than ConstantValue before.
+ *)
| `Assoc [ ("ConstantValue", `List [ cv ]) ] ->
- let* cv = constant_value_of_json cv in
- Ok (E.ConstantValue cv)
- | `Assoc [ ("ConstantAdt", `List [ variant_id; field_values ]) ] ->
- let* variant_id = option_of_json T.VariantId.id_of_json variant_id in
- let* field_values =
- list_of_json (fun js -> operand_constant_value_of_json js fun_count) field_values
- in
- Ok (E.ConstantAdt (variant_id, field_values))
- | `Assoc [ ("ConstantIdentifier", `List [gid]) ] ->
- let* id = global_id_of_json gid fun_count in
- Ok (E.ConstantId id)
- | _ -> Error "")
-
-let operand_of_json (js : json) (fun_count : int) : (E.operand, string) result =
+ (match cv with
+ | `Assoc [ ("Scalar", scalar_value) ] ->
+ let* scalar_value = scalar_value_of_json scalar_value in
+ Ok (V.Scalar scalar_value)
+ | `Assoc [ ("Bool", v) ] ->
+ let* v = bool_of_json v in
+ Ok (V.Bool v)
+ | `Assoc [ ("Char", v) ] ->
+ let* v = char_of_json v in
+ Ok (V.Char v)
+ | `Assoc [ ("String", v) ] ->
+ let* v = string_of_json v in
+ Ok (V.String v)
+ | _ -> Error "")
+ | _ -> Error "")
+
+let operand_of_json (js : json) : (E.operand, string) result =
combine_error_msgs js "operand_of_json"
(match js with
| `Assoc [ ("Copy", place) ] ->
@@ -432,7 +412,7 @@ let operand_of_json (js : json) (fun_count : int) : (E.operand, string) result =
Ok (E.Move place)
| `Assoc [ ("Const", `List [ ty; cv ]) ] ->
let* ty = ety_of_json ty in
- let* cv = operand_constant_value_of_json cv fun_count in
+ let* cv = constant_value_of_json cv in
Ok (E.Constant (ty, cv))
| _ -> Error "")
@@ -455,11 +435,11 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result =
Ok (E.AggregatedAdt (id, opt_variant_id, regions, tys))
| _ -> Error "")
-let rvalue_of_json (js : json) (fun_count : int) : (E.rvalue, string) result =
+let rvalue_of_json (js : json) : (E.rvalue, string) result =
combine_error_msgs js "rvalue_of_json"
(match js with
| `Assoc [ ("Use", op) ] ->
- let* op = operand_of_json op fun_count in
+ let* op = operand_of_json op in
Ok (E.Use op)
| `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] ->
let* place = place_of_json place in
@@ -467,19 +447,19 @@ let rvalue_of_json (js : json) (fun_count : int) : (E.rvalue, string) result =
Ok (E.Ref (place, borrow_kind))
| `Assoc [ ("UnaryOp", `List [ unop; op ]) ] ->
let* unop = unop_of_json unop in
- let* op = operand_of_json op fun_count in
+ let* op = operand_of_json op in
Ok (E.UnaryOp (unop, op))
| `Assoc [ ("BinaryOp", `List [ binop; op1; op2 ]) ] ->
let* binop = binop_of_json binop in
- let* op1 = operand_of_json op1 fun_count in
- let* op2 = operand_of_json op2 fun_count in
+ let* op1 = operand_of_json op1 in
+ let* op2 = operand_of_json op2 in
Ok (E.BinaryOp (binop, op1, op2))
| `Assoc [ ("Discriminant", place) ] ->
let* place = place_of_json place in
Ok (E.Discriminant place)
| `Assoc [ ("Aggregate", `List [ aggregate_kind; ops ]) ] ->
let* aggregate_kind = aggregate_kind_of_json aggregate_kind in
- let* ops = list_of_json (fun js -> operand_of_json js fun_count) ops in
+ let* ops = list_of_json operand_of_json ops in
Ok (E.Aggregate (aggregate_kind, ops))
| _ -> Error "")
@@ -502,18 +482,18 @@ let fun_id_of_json (js : json) : (A.fun_id, string) result =
combine_error_msgs js "fun_id_of_json"
(match js with
| `Assoc [ ("Regular", id) ] ->
- let* id = FunDeclId.id_of_json id in
+ let* id = A.FunDeclId.id_of_json id in
Ok (A.Regular id)
| `Assoc [ ("Assumed", fid) ] ->
let* fid = assumed_fun_id_of_json fid in
Ok (A.Assumed fid)
| _ -> Error "")
-let assertion_of_json (js : json) (fun_count : int) : (A.assertion, string) result =
+let assertion_of_json (js : json) : (A.assertion, string) result =
combine_error_msgs js "assertion_of_json"
(match js with
| `Assoc [ ("cond", cond); ("expected", expected) ] ->
- let* cond = operand_of_json cond fun_count in
+ let* cond = operand_of_json cond in
let* expected = bool_of_json expected in
Ok { A.cond; expected }
| _ -> Error "")
@@ -547,7 +527,7 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
}
| _ -> Error "")
-let call_of_json (js : json) (fun_count : int) : (A.call, string) result =
+let call_of_json (js : json) : (A.call, string) result =
combine_error_msgs js "call_of_json"
(match js with
| `Assoc
@@ -561,18 +541,22 @@ let call_of_json (js : json) (fun_count : int) : (A.call, string) result =
let* func = fun_id_of_json func in
let* region_args = list_of_json erased_region_of_json region_args in
let* type_args = list_of_json ety_of_json type_args in
- let* args = list_of_json (fun js -> operand_of_json js fun_count) args in
+ let* args = list_of_json operand_of_json args in
let* dest = place_of_json dest in
Ok { A.func; region_args; type_args; args; dest }
| _ -> Error "")
-let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string) result =
+let rec statement_of_json (js : json) (gid_conv : A.global_id_converter) : (A.statement, string) result =
combine_error_msgs js "statement_of_json"
(match js with
| `Assoc [ ("Assign", `List [ place; rvalue ]) ] ->
let* place = place_of_json place in
- let* rvalue = rvalue_of_json rvalue fun_count in
+ let* rvalue = rvalue_of_json rvalue in
Ok (A.Assign (place, rvalue))
+ | `Assoc [ ("AssignGlobal", `List [ dst; global ]) ] ->
+ let* dst = V.VarId.id_of_json dst in
+ let* global = A.GlobalDeclId.id_of_json global in
+ Ok (A.AssignGlobal { dst; global })
| `Assoc [ ("FakeRead", place) ] ->
let* place = place_of_json place in
Ok (A.FakeRead place)
@@ -584,10 +568,10 @@ let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string)
let* place = place_of_json place in
Ok (A.Drop place)
| `Assoc [ ("Assert", assertion) ] ->
- let* assertion = assertion_of_json assertion fun_count in
+ let* assertion = assertion_of_json assertion in
Ok (A.Assert assertion)
| `Assoc [ ("Call", call) ] ->
- let* call = call_of_json call fun_count in
+ let* call = call_of_json call in
Ok (A.Call call)
| `String "Panic" -> Ok A.Panic
| `String "Return" -> Ok A.Return
@@ -599,48 +583,48 @@ let rec statement_of_json (js : json) (fun_count : int) : (A.statement, string)
Ok (A.Continue i)
| `String "Nop" -> Ok A.Nop
| `Assoc [ ("Sequence", `List [ st1; st2 ]) ] ->
- let* st1 = statement_of_json st1 fun_count in
- let* st2 = statement_of_json st2 fun_count in
+ let* st1 = statement_of_json st1 gid_conv in
+ let* st2 = statement_of_json st2 gid_conv in
Ok (A.Sequence (st1, st2))
| `Assoc [ ("Switch", `List [ op; tgt ]) ] ->
- let* op = operand_of_json op fun_count in
- let* tgt = switch_targets_of_json tgt fun_count in
+ let* op = operand_of_json op in
+ let* tgt = switch_targets_of_json tgt gid_conv in
Ok (A.Switch (op, tgt))
| `Assoc [ ("Loop", st) ] ->
- let* st = statement_of_json st fun_count in
+ let* st = statement_of_json st gid_conv in
Ok (A.Loop st)
| _ -> Error "")
-and switch_targets_of_json (js : json) (fun_count : int) : (A.switch_targets, string) result =
+and switch_targets_of_json (js : json) (gid_conv : A.global_id_converter) : (A.switch_targets, string) result =
combine_error_msgs js "switch_targets_of_json"
(match js with
| `Assoc [ ("If", `List [ st1; st2 ]) ] ->
- let* st1 = statement_of_json st1 fun_count in
- let* st2 = statement_of_json st2 fun_count in
+ let* st1 = statement_of_json st1 gid_conv in
+ let* st2 = statement_of_json st2 gid_conv in
Ok (A.If (st1, st2))
| `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] ->
let* int_ty = integer_type_of_json int_ty in
let* tgts =
list_of_json (pair_of_json
(list_of_json scalar_value_of_json)
- (fun js -> statement_of_json js fun_count))
+ (fun js -> statement_of_json js gid_conv))
tgts
in
- let* otherwise = statement_of_json otherwise fun_count in
+ let* otherwise = statement_of_json otherwise gid_conv in
Ok (A.SwitchInt (int_ty, tgts, otherwise))
| _ -> Error "")
-let fun_body_of_json (js : json) (fun_count : int) : (A.fun_body, string) result =
+let fun_body_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_body, string) result =
combine_error_msgs js "fun_body_of_json"
(match js with
| `Assoc [ ("arg_count", arg_count); ("locals", locals); ("body", body) ] ->
let* arg_count = int_of_json arg_count in
let* locals = list_of_json var_of_json locals in
- let* body = statement_of_json body fun_count in
+ let* body = statement_of_json body gid_conv in
Ok { A.arg_count; locals; body }
| _ -> Error "")
-let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result =
+let fun_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
combine_error_msgs js "fun_decl_of_json"
(match js with
| `Assoc
@@ -650,20 +634,16 @@ let fun_decl_of_json (js : json) (fun_count : int) : (A.fun_decl, string) result
("signature", signature);
("body", body);
] ->
- let* def_id = FunDeclId.id_of_json def_id in
+ let* def_id = A.FunDeclId.id_of_json def_id in
let* name = fun_name_of_json name in
let* signature = fun_sig_of_json signature in
- let* body = option_of_json (fun js -> fun_body_of_json js fun_count) body in
+ let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in
Ok { A.def_id; name; signature; body; is_global = false; }
| _ -> Error "")
-
(* Converts a global declaration to a function declaration.
-
-A.fun_sig
-ety_no_regions_to_rty
-*)
-let global_decl_of_json (js : json) (fun_count: int) : (A.fun_decl, string) result =
+ *)
+let global_decl_of_json (js : json) (gid_conv : A.global_id_converter) : (A.fun_decl, string) result =
combine_error_msgs js "global_decl_of_json"
(match js with
| `Assoc
@@ -673,10 +653,11 @@ let global_decl_of_json (js : json) (fun_count: int) : (A.fun_decl, string) resu
("type_", type_);
("body", body);
] ->
- let* def_id = global_id_of_json def_id fun_count in
+ let* global_id = A.GlobalDeclId.id_of_json def_id in
+ let def_id = A.global_to_fun_id gid_conv global_id in
let* name = fun_name_of_json name in
let* type_ = ety_of_json type_ in
- let* body = option_of_json (fun js -> fun_body_of_json js fun_count) body in
+ let* body = option_of_json (fun js -> fun_body_of_json js gid_conv) body in
let signature : A.fun_sig = {
region_params = [];
num_early_bound_regions = 0;
@@ -708,14 +689,17 @@ let type_declaration_group_of_json (js : json) :
let fun_declaration_group_of_json (js : json) :
(M.fun_declaration_group, string) result =
combine_error_msgs js "fun_declaration_group_of_json"
- (g_declaration_group_of_json FunDeclId.id_of_json js)
+ (g_declaration_group_of_json A.FunDeclId.id_of_json js)
-let global_declaration_group_of_json (js : json) (fun_count: int) :
+let global_declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) :
(M.fun_declaration_group, string) result =
combine_error_msgs js "global_declaration_group_of_json"
- (g_declaration_group_of_json (fun js -> global_id_of_json js fun_count) js)
+ (g_declaration_group_of_json (fun js ->
+ let* id = A.GlobalDeclId.id_of_json js in
+ Ok (A.global_to_fun_id gid_conv id)
+ ) js)
-let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_group, string) result
+let declaration_group_of_json (js : json) (gid_conv : A.global_id_converter) : (M.declaration_group, string) result
=
combine_error_msgs js "declaration_of_json"
(match js with
@@ -726,7 +710,7 @@ let declaration_group_of_json (js : json) (fun_count: int) : (M.declaration_grou
let* decl = fun_declaration_group_of_json decl in
Ok (M.Fun decl)
| `Assoc [ ("Global", `List [ decl ]) ] ->
- let* decl = global_declaration_group_of_json decl fun_count in
+ let* decl = global_declaration_group_of_json decl gid_conv in
Ok (M.Fun decl)
| _ -> Error "")
@@ -748,12 +732,19 @@ let llbc_module_of_json (js : json) : (M.llbc_module, string) result =
("globals", globals);
] ->
let* fun_count = length_of_json_list functions in
+ let gid_conv = { A.fun_count = fun_count } in
let* name = string_of_json name in
let* declarations =
- list_of_json (fun js -> declaration_group_of_json js fun_count) declarations
+ list_of_json (fun js -> declaration_group_of_json js gid_conv) declarations
in
let* types = list_of_json type_decl_of_json types in
- let* functions = list_of_json (fun js -> fun_decl_of_json js fun_count) functions in
- let* globals = list_of_json (fun js -> global_decl_of_json js fun_count) globals in
- Ok { M.name; declarations; types; functions = functions @ globals }
+ let* functions = list_of_json (fun js -> fun_decl_of_json js gid_conv) functions in
+ let* globals = list_of_json (fun js -> global_decl_of_json js gid_conv) globals in
+ Ok {
+ M.name;
+ declarations;
+ types;
+ functions = functions @ globals;
+ gid_conv;
+ }
| _ -> Error "")
diff --git a/src/Modules.ml b/src/Modules.ml
index 6d0cf70c..b0e8878d 100644
--- a/src/Modules.ml
+++ b/src/Modules.ml
@@ -1,6 +1,5 @@
open Types
open LlbcAst
-open FunIdentifier
type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
[@@deriving show]
@@ -21,6 +20,7 @@ type llbc_module = {
declarations : declaration_group list;
types : type_decl list;
functions : fun_decl list;
+ gid_conv : global_id_converter;
}
(** LLBC module - TODO: rename to crate *)
diff --git a/src/Print.ml b/src/Print.ml
index 9e2ff3cd..722f76ce 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -1,5 +1,4 @@
open Names
-open FunIdentifier
module T = Types
module TU = TypesUtils
module V = Values
@@ -686,7 +685,8 @@ module LlbcAst = struct
var_id_to_string : V.VarId.id -> string;
adt_field_names :
T.TypeDeclId.id -> T.VariantId.id option -> string list option;
- fun_decl_id_to_string : FunDeclId.id -> string;
+ fun_decl_id_to_string : A.FunDeclId.id -> string;
+ global_decl_id_to_string : A.GlobalDeclId.id -> string;
}
let ast_to_ctx_formatter (fmt : ast_formatter) : PC.ctx_formatter =
@@ -743,6 +743,9 @@ module LlbcAst = struct
let def = C.ctx_lookup_fun_decl ctx def_id in
fun_name_to_string def.name
in
+ let global_decl_id_to_string def_id =
+ fun_decl_id_to_string (A.global_to_fun_id ctx.fun_context.gid_conv def_id)
+ in
{
rvar_to_string = ctx_fmt.PV.rvar_to_string;
r_to_string = ctx_fmt.PV.r_to_string;
@@ -753,10 +756,14 @@ module LlbcAst = struct
adt_field_names = ctx_fmt.PV.adt_field_names;
adt_field_to_string;
fun_decl_id_to_string;
+ global_decl_id_to_string;
}
- let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t)
- (fun_decls : A.fun_decl FunDeclId.Map.t) (fdef : A.fun_decl) :
+ let fun_decl_to_ast_formatter
+ (type_decls : T.type_decl T.TypeDeclId.Map.t)
+ (fun_decls : A.fun_decl A.FunDeclId.Map.t)
+ (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id)
+ (fdef : A.fun_decl) :
ast_formatter =
let rvar_to_string r =
let rvar = T.RegionVarId.nth fdef.signature.region_params r in
@@ -782,9 +789,12 @@ module LlbcAst = struct
let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_decls in
let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_decls in
let fun_decl_id_to_string def_id =
- let def = FunDeclId.Map.find def_id fun_decls in
+ let def = A.FunDeclId.Map.find def_id fun_decls in
fun_name_to_string def.name
in
+ let global_decl_id_to_string def_id =
+ fun_decl_id_to_string (global_to_fun_id def_id)
+ in
{
rvar_to_string;
r_to_string;
@@ -795,6 +805,7 @@ module LlbcAst = struct
adt_field_names;
adt_field_to_string;
fun_decl_id_to_string;
+ global_decl_id_to_string;
}
let rec projection_to_string (fmt : ast_formatter) (inside : string)
@@ -860,36 +871,13 @@ module LlbcAst = struct
| E.Shl -> "<<"
| E.Shr -> ">>"
- let rec operand_constant_value_to_string (fmt : ast_formatter)
- (cv : E.operand_constant_value) : string =
- match cv with
- | E.ConstantId id -> fmt.fun_decl_id_to_string id
- | E.ConstantValue cv -> PV.constant_value_to_string cv
- | E.ConstantAdt (variant_id, field_values) ->
- (* This is a bit annoying, because we don't have context information
- * to convert the ADT to a value, so we do the best we can in the
- * simplest manner. Anyway, those printing utilitites are only used
- * for debugging, and complex constant values are not common.
- * We might want to store type information in the operand constant values
- * in the future.
- *)
- let variant_id = option_to_string T.VariantId.to_string variant_id in
- let field_values =
- List.map (operand_constant_value_to_string fmt) field_values
- in
- "ConstantAdt " ^ variant_id ^ " {"
- ^ String.concat ", " field_values
- ^ "}"
-
let operand_to_string (fmt : ast_formatter) (op : E.operand) : string =
match op with
| E.Copy p -> "copy " ^ place_to_string fmt p
| E.Move p -> "move " ^ place_to_string fmt p
| E.Constant (ty, cv) ->
- (* For clarity, we also print the typing information: see the comment in
- * [operand_constant_value_to_string] *)
"("
- ^ operand_constant_value_to_string fmt cv
+ ^ PV.constant_value_to_string cv
^ " : "
^ PT.ety_to_string (ast_to_etype_formatter fmt) ty
^ ")"
@@ -950,6 +938,8 @@ module LlbcAst = struct
match st with
| A.Assign (p, rv) ->
indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
+ | A.AssignGlobal { dst; global } ->
+ indent ^ fmt.var_id_to_string dst ^ " := global " ^ fmt.global_decl_id_to_string global
| A.FakeRead p -> "fake_read " ^ place_to_string fmt p
| A.SetDiscriminant (p, variant_id) ->
(* TODO: improve this to lookup the variant name by using the def id *)
@@ -1139,8 +1129,11 @@ module Module = struct
(** Generate an [ast_formatter] by using a definition context in combination
with the variables local to a function's definition *)
- let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t)
- (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) :
+ let def_ctx_to_ast_formatter
+ (type_context : T.type_decl T.TypeDeclId.Map.t)
+ (fun_context : A.fun_decl A.FunDeclId.Map.t)
+ (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id)
+ (def : A.fun_decl) :
PA.ast_formatter =
let rvar_to_string vid =
let var = T.RegionVarId.nth def.signature.region_params vid in
@@ -1159,9 +1152,12 @@ module Module = struct
name_to_string def.name
in
let fun_decl_id_to_string def_id =
- let def = FunDeclId.Map.find def_id fun_context in
+ let def = A.FunDeclId.Map.find def_id fun_context in
fun_name_to_string def.name
in
+ let global_decl_id_to_string def_id =
+ fun_decl_id_to_string (global_to_fun_id def_id)
+ in
let var_id_to_string vid =
let var = V.VarId.nth (Option.get def.body).locals vid in
PA.var_to_string var
@@ -1183,13 +1179,17 @@ module Module = struct
var_id_to_string;
adt_field_names;
fun_decl_id_to_string;
+ global_decl_id_to_string;
}
(** This function pretty-prints a function definition by using a definition
context *)
- let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
- (fun_context : A.fun_decl FunDeclId.Map.t) (def : A.fun_decl) : string =
- let fmt = def_ctx_to_ast_formatter type_context fun_context def in
+ let fun_decl_to_string
+ (type_context : T.type_decl T.TypeDeclId.Map.t)
+ (fun_context : A.fun_decl A.FunDeclId.Map.t)
+ (global_to_fun_id : A.GlobalDeclId.id -> A.FunDeclId.id)
+ (def : A.fun_decl) : string =
+ let fmt = def_ctx_to_ast_formatter type_context fun_context global_to_fun_id def in
PA.fun_decl_to_string fmt "" " " def
let module_to_string (m : M.llbc_module) : string =
@@ -1200,7 +1200,8 @@ module Module = struct
(* The functions *)
let fun_decls =
- List.map (fun_decl_to_string types_defs_map funs_defs_map) m.M.functions
+ let gid_to_fid = fun gid -> A.global_to_fun_id m.gid_conv gid in
+ List.map (fun_decl_to_string types_defs_map funs_defs_map gid_to_fid) m.M.functions
in
(* Put everything together *)
@@ -1257,11 +1258,6 @@ module EvalCtxLlbcAst = struct
let fmt = PC.eval_ctx_to_ctx_formatter ctx in
PV.typed_avalue_to_string fmt v
- let operand_constant_value_to_string (ctx : C.eval_ctx)
- (cv : E.operand_constant_value) : string =
- let fmt = PA.eval_ctx_to_ast_formatter ctx in
- PA.operand_constant_value_to_string fmt cv
-
let place_to_string (ctx : C.eval_ctx) (op : E.place) : string =
let fmt = PA.eval_ctx_to_ast_formatter ctx in
PA.place_to_string fmt op
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 8864dafe..ea9bf2ab 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -2,7 +2,6 @@
open Pure
open PureUtils
-open FunIdentifier
module T = Types
module V = Values
module E = Expressions
@@ -44,7 +43,7 @@ type ast_formatter = {
adt_field_to_string :
TypeDeclId.id -> VariantId.id option -> FieldId.id -> string option;
adt_field_names : TypeDeclId.id -> VariantId.id option -> string list option;
- fun_decl_id_to_string : FunDeclId.id -> string;
+ fun_decl_id_to_string : A.FunDeclId.id -> string;
}
let ast_to_value_formatter (fmt : ast_formatter) : value_formatter =
@@ -86,7 +85,7 @@ let mk_type_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
while we only need those definitions to lookup proper names for the def ids.
*)
let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
- (fun_decls : A.fun_decl FunDeclId.Map.t) (type_params : type_var list) :
+ (fun_decls : A.fun_decl A.FunDeclId.Map.t) (type_params : type_var list) :
ast_formatter =
let type_var_id_to_string vid =
let var = T.TypeVarId.nth type_params vid in
@@ -110,7 +109,7 @@ let mk_ast_formatter (type_decls : T.type_decl TypeDeclId.Map.t)
Print.LlbcAst.type_ctx_to_adt_field_to_string_fun type_decls
in
let fun_decl_id_to_string def_id =
- let def = FunDeclId.Map.find def_id fun_decls in
+ let def = A.FunDeclId.Map.find def_id fun_decls in
fun_name_to_string def.name
in
{
diff --git a/src/Pure.ml b/src/Pure.ml
index 256a872a..42f56fed 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -1,6 +1,5 @@
open Identifiers
open Names
-open FunIdentifier
module T = Types
module V = Values
module E = Expressions
@@ -567,7 +566,7 @@ type fun_body = {
}
type fun_decl = {
- def_id : FunDeclId.id;
+ def_id : A.FunDeclId.id;
back_id : T.RegionGroupId.id option;
basename : fun_name;
(** The "base" name of the function.
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 55a8853a..195eb879 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -6,7 +6,6 @@
open Pure
open TranslateCore
-open FunIdentifier
module C = Contexts
module RegionVarId = T.RegionVarId
module F = Format
@@ -93,7 +92,7 @@ type formatter = {
(`None` if forward function)
TODO: use the fun id for the assumed functions.
*)
- decreases_clause_name : FunDeclId.id -> fun_name -> string;
+ decreases_clause_name : A.FunDeclId.id -> fun_name -> string;
(** Generates the name of the definition used to prove/reason about
termination. The generated code uses this clause where needed,
but its body must be defined by the user.
@@ -357,7 +356,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
let fun_name =
match fid with
| A.Regular fid ->
- Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name
+ Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name
| A.Assumed aid -> A.show_assumed_fun_id aid
in
let fun_kind =
@@ -370,7 +369,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
let fun_name =
match fid with
| A.Regular fid ->
- Print.fun_name_to_string (FunDeclId.Map.find fid fun_decls).name
+ Print.fun_name_to_string (A.FunDeclId.Map.find fid fun_decls).name
| A.Assumed aid -> A.show_assumed_fun_id aid
in
"decreases clause for function: " ^ fun_name
@@ -445,7 +444,7 @@ let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option)
(ctx : extraction_ctx) : string =
ctx_get (FunId (id, rg)) ctx
-let ctx_get_local_function (id : FunDeclId.id) (rg : RegionGroupId.id option)
+let ctx_get_local_function (id : A.FunDeclId.id) (rg : RegionGroupId.id option)
(ctx : extraction_ctx) : string =
ctx_get_function (A.Regular id) rg ctx
@@ -476,7 +475,7 @@ let ctx_get_variant (def_id : type_id) (variant_id : VariantId.id)
(ctx : extraction_ctx) : string =
ctx_get (VariantId (def_id, variant_id)) ctx
-let ctx_get_decreases_clause (def_id : FunDeclId.id) (ctx : extraction_ctx) :
+let ctx_get_decreases_clause (def_id : A.FunDeclId.id) (ctx : extraction_ctx) :
string =
ctx_get (DecreasesClauseId (A.Regular def_id)) ctx
@@ -574,7 +573,7 @@ let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
(* Lookup the LLBC def to compute the region group information *)
let def_id = def.def_id in
let llbc_def =
- FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls
+ A.FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls
in
let sg = llbc_def.signature in
let num_rgs = List.length sg.regions_hierarchy in
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 711e438b..4b0a04ca 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -210,12 +210,6 @@ let place_substitute (_tsubst : T.TypeVarId.id -> T.ety) (p : E.place) : E.place
(* There is nothing to do *)
p
-(** Apply a type substitution to an operand constant value *)
-let operand_constant_value_substitute (_tsubst : T.TypeVarId.id -> T.ety)
- (op : E.operand_constant_value) : E.operand_constant_value =
- (* There is nothing to do *)
- op
-
(** Apply a type substitution to an operand *)
let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) :
E.operand =
@@ -225,9 +219,7 @@ let operand_substitute (tsubst : T.TypeVarId.id -> T.ety) (op : E.operand) :
| E.Move p -> E.Move (p_subst p)
| E.Constant (ety, cv) ->
let rsubst x = x in
- E.Constant
- ( ty_substitute rsubst tsubst ety,
- operand_constant_value_substitute tsubst cv )
+ E.Constant ( ty_substitute rsubst tsubst ety, cv )
(** Apply a type substitution to an rvalue *)
let rvalue_substitute (tsubst : T.TypeVarId.id -> T.ety) (rv : E.rvalue) :
@@ -289,6 +281,7 @@ let rec statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
let p = place_substitute tsubst p in
let rvalue = rvalue_substitute tsubst rvalue in
A.Assign (p, rvalue)
+ | A.AssignGlobal g -> A.AssignGlobal g
| A.FakeRead p ->
let p = place_substitute tsubst p in
A.FakeRead p
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 2b416cc1..927684bc 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -2,7 +2,6 @@ open Errors
open LlbcAstUtils
open Pure
open PureUtils
-open FunIdentifier
module Id = Identifiers
module M = Modules
module S = SymbolicAst
@@ -68,9 +67,10 @@ type fun_sig_named_outputs = {
}
type fun_context = {
- llbc_fun_decls : A.fun_decl FunDeclId.Map.t;
+ llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
fun_sigs : fun_sig_named_outputs RegularFunIdMap.t; (** *)
- fun_infos : FA.fun_info FunDeclId.Map.t;
+ fun_infos : FA.fun_info A.FunDeclId.Map.t;
+ gid_conv : A.global_id_converter;
}
type call_info = {
@@ -134,8 +134,11 @@ let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit =
(* TODO: move *)
let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.LlbcAst.ast_formatter =
- Print.LlbcAst.fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls
- ctx.fun_context.llbc_fun_decls ctx.fun_decl
+ Print.LlbcAst.fun_decl_to_ast_formatter
+ ctx.type_context.llbc_type_decls
+ ctx.fun_context.llbc_fun_decls
+ (A.global_to_fun_id ctx.fun_context.gid_conv)
+ ctx.fun_decl
let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
let type_params = ctx.fun_decl.signature.type_params in
@@ -196,12 +199,12 @@ let bs_ctx_lookup_llbc_type_decl (id : TypeDeclId.id) (ctx : bs_ctx) :
T.type_decl =
TypeDeclId.Map.find id ctx.type_context.llbc_type_decls
-let bs_ctx_lookup_llbc_fun_decl (id : FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
+let bs_ctx_lookup_llbc_fun_decl (id : A.FunDeclId.id) (ctx : bs_ctx) : A.fun_decl
=
- FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls
+ A.FunDeclId.Map.find id ctx.fun_context.llbc_fun_decls
(* TODO: move *)
-let bs_ctx_lookup_local_function_sig (def_id : FunDeclId.id)
+let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id)
(back_id : T.RegionGroupId.id option) (ctx : bs_ctx) : fun_sig =
let id = (A.Regular def_id, back_id) in
(RegularFunIdMap.find id ctx.fun_context.fun_sigs).sg
@@ -472,11 +475,11 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) :
List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids
(** Small utility. *)
-let get_fun_effect_info (fun_infos : FA.fun_info FunDeclId.Map.t)
+let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
(fun_id : A.fun_id) (gid : T.RegionGroupId.id option) : fun_effect_info =
match fun_id with
| A.Regular fid ->
- let info = FunDeclId.Map.find fid fun_infos in
+ let info = A.FunDeclId.Map.find fid fun_infos in
let input_state = info.stateful in
let output_state = input_state && gid = None in
{ can_fail = true; input_state; output_state }
@@ -494,7 +497,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info FunDeclId.Map.t)
name (outputs for backward functions come from borrows in the inputs
of the forward function).
*)
-let translate_fun_sig (fun_infos : FA.fun_info FunDeclId.Map.t)
+let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
(fun_id : A.fun_id) (types_infos : TA.type_infos) (sg : A.fun_sig)
(input_names : string option list) (bid : T.RegionGroupId.id option) :
fun_sig_named_outputs =
@@ -1744,7 +1747,7 @@ let translate_type_decls (type_decls : T.type_decl list) : type_decl list =
- optional names for the outputs values (we derive them for the backward
functions)
*)
-let translate_fun_signatures (fun_infos : FA.fun_info FunDeclId.Map.t)
+let translate_fun_signatures (fun_infos : FA.fun_info A.FunDeclId.Map.t)
(types_infos : TA.type_infos)
(functions : (A.fun_id * string option list * A.fun_sig) list) :
fun_sig_named_outputs RegularFunIdMap.t =
diff --git a/src/Translate.ml b/src/Translate.ml
index 1577753c..d4d79355 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -1,6 +1,5 @@
open InterpreterStatements
open Interpreter
-open FunIdentifier
module L = Logging
module T = Types
module A = LlbcAst
@@ -65,7 +64,10 @@ let translate_function_to_symbolics (config : C.partial_config)
^ Print.fun_name_to_string fdef.A.name));
let { type_context; fun_context } = trans_ctx in
- let fun_context = { C.fun_decls = fun_context.fun_decls } in
+ let fun_context = {
+ C.fun_decls = fun_context.fun_decls;
+ C.gid_conv = fun_context.gid_conv;
+ } in
match fdef.body with
| None -> None
@@ -100,7 +102,8 @@ let translate_function_to_symbolics (config : C.partial_config)
let translate_function_to_pure (config : C.partial_config)
(mp_config : Micro.config) (trans_ctx : trans_ctx)
(fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t)
- (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl)
+ (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t)
+ (fdef : A.fun_decl)
: pure_fun_translation =
(* Debug *)
log#ldebug
@@ -139,6 +142,7 @@ let translate_function_to_pure (config : C.partial_config)
SymbolicToPure.llbc_fun_decls = fun_context.fun_decls;
fun_sigs;
fun_infos = fun_context.fun_infos;
+ gid_conv = fun_context.gid_conv;
}
in
let ctx =
@@ -291,7 +295,11 @@ let translate_module_to_pure (config : C.partial_config)
(* Compute the type and function contexts *)
let type_context, fun_context = compute_type_fun_contexts m in
let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in
- let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in
+ let fun_context = {
+ fun_decls = fun_context.fun_decls;
+ fun_infos;
+ gid_conv = m.gid_conv;
+ } in
let trans_ctx = { type_context; fun_context } in
(* Translate all the type definitions *)
@@ -352,8 +360,8 @@ type gen_ctx = {
m : M.llbc_module;
extract_ctx : PureToExtract.extraction_ctx;
trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
- trans_funs : (bool * pure_fun_translation) FunDeclId.Map.t;
- functions_with_decreases_clause : FunDeclId.Set.t;
+ trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t;
+ functions_with_decreases_clause : A.FunDeclId.Set.t;
}
(** Extraction context *)
@@ -389,7 +397,7 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
ctx.trans_types
in
let has_opaque_funs =
- FunDeclId.Map.exists
+ A.FunDeclId.Map.exists
(fun _ ((_, (t_fwd, _)) : bool * pure_fun_translation) ->
Option.is_none t_fwd.body)
ctx.trans_funs
@@ -428,7 +436,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
(* Utility to check a function has a decrease clause *)
let has_decreases_clause (def : Pure.fun_decl) : bool =
- FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
+ A.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
in
(* In case of (non-mutually) recursive functions, we use a simple procedure to
@@ -524,14 +532,14 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
ids
| Fun (NonRec id) ->
(* Lookup *)
- let pure_fun = FunDeclId.Map.find id ctx.trans_funs in
+ let pure_fun = A.FunDeclId.Map.find id ctx.trans_funs in
(* Translate *)
export_functions false [ pure_fun ]
| Fun (Rec ids) ->
(* General case of mutually recursive functions *)
(* Lookup *)
let pure_funs =
- List.map (fun id -> FunDeclId.Map.find id ctx.trans_funs) ids
+ List.map (fun id -> A.FunDeclId.Map.find id ctx.trans_funs) ids
in
(* Translate *)
export_functions true pure_funs
@@ -623,7 +631,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(* We need to compute which functions are recursive, in order to know
* whether we should generate a decrease clause or not. *)
let rec_functions =
- FunDeclId.Set.of_list
+ A.FunDeclId.Set.of_list
(List.concat
(List.map
(fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> [])
@@ -645,7 +653,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(fun ctx (keep_fwd, def) ->
(* Note that we generate a decrease clause for all the recursive functions *)
let gen_decr_clause =
- FunDeclId.Set.mem (fst def).Pure.def_id rec_functions
+ A.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions
in
ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
gen_decr_clause def)
@@ -675,7 +683,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
in
let trans_funs =
- FunDeclId.Map.of_list
+ A.FunDeclId.Map.of_list
(List.map
(fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) ->
(fd.def_id, (keep_fwd, (fd, bdl))))
@@ -762,7 +770,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
(* Extract the template clauses *)
let needs_clauses_module =
config.extract_decreases_clauses
- && not (FunDeclId.Set.is_empty rec_functions)
+ && not (A.FunDeclId.Set.is_empty rec_functions)
in
(if needs_clauses_module && config.extract_template_decreases_clauses then
let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 3d3887ce..ccaa9e22 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -1,7 +1,6 @@
(** Some utilities for the translation *)
open InterpreterStatements
-open FunIdentifier
module L = Logging
module T = Types
module A = LlbcAst
@@ -15,8 +14,9 @@ let log = L.translate_log
type type_context = C.type_context [@@deriving show]
type fun_context = {
- fun_decls : A.fun_decl FunDeclId.Map.t;
- fun_infos : FA.fun_info FunDeclId.Map.t;
+ fun_decls : A.fun_decl A.FunDeclId.Map.t;
+ fun_infos : FA.fun_info A.FunDeclId.Map.t;
+ gid_conv : A.global_id_converter;
}
[@@deriving show]
@@ -50,6 +50,6 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
PrintPure.fun_decl_to_string fmt def
-let fun_decl_id_to_string (ctx : trans_ctx) (id : FunDeclId.id) : string =
+let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string =
Print.fun_name_to_string
- (FunDeclId.Map.find id ctx.fun_context.fun_decls).name
+ (A.FunDeclId.Map.find id ctx.fun_context.fun_decls).name
diff --git a/src/main.ml b/src/main.ml
index 6b1083f5..93b094fd 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -124,21 +124,21 @@ let () =
* command-line arguments *)
(* By setting a level for the main_logger_handler, we filter everything *)
Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
- main_log#set_level EL.Info;
- llbc_of_json_logger#set_level EL.Info;
- pre_passes_log#set_level EL.Info;
- interpreter_log#set_level EL.Info;
- statements_log#set_level EL.Info;
- paths_log#set_level EL.Info;
- expressions_log#set_level EL.Info;
- expansion_log#set_level EL.Info;
- borrows_log#set_level EL.Info;
- invariants_log#set_level EL.Info;
- pure_utils_log#set_level EL.Info;
- symbolic_to_pure_log#set_level EL.Info;
- pure_micro_passes_log#set_level EL.Info;
- pure_to_extract_log#set_level EL.Info;
- translate_log#set_level EL.Info;
+ main_log#set_level EL.Debug;
+ llbc_of_json_logger#set_level EL.Debug;
+ pre_passes_log#set_level EL.Debug;
+ interpreter_log#set_level EL.Debug;
+ statements_log#set_level EL.Debug;
+ paths_log#set_level EL.Debug;
+ expressions_log#set_level EL.Debug;
+ expansion_log#set_level EL.Debug;
+ borrows_log#set_level EL.Debug;
+ invariants_log#set_level EL.Debug;
+ pure_utils_log#set_level EL.Debug;
+ symbolic_to_pure_log#set_level EL.Debug;
+ pure_micro_passes_log#set_level EL.Debug;
+ pure_to_extract_log#set_level EL.Debug;
+ translate_log#set_level EL.Debug;
(* Load the module *)
let json = Yojson.Basic.from_file filename in
match llbc_module_of_json json with
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
new file mode 100644
index 00000000..9611c778
--- /dev/null
+++ b/tests/misc/Constants.fst
@@ -0,0 +1,119 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [constants] *)
+module Constants
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [constants::X0] *)
+let x0_fwd : result u32 = Return 0
+
+(** [core::num::u32::{8}::MAX] *)
+assume val core_num_u32_max_fwd : result u32
+
+(** [constants::X1] *)
+let x1_fwd : result u32 = Return 4294967295
+
+(** [constants::X2] *)
+let x2_fwd : result u32 = Return 3
+
+(** [constants::incr] *)
+let incr_fwd (n : u32) : result u32 =
+ begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::X3] *)
+let x3_fwd : result u32 =
+ begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::mk_pair0] *)
+let mk_pair0_fwd (x : u32) (y : u32) : result (u32 & u32) = Return (x, y)
+
+(** [constants::Pair] *)
+type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
+
+(** [constants::mk_pair1] *)
+let mk_pair1_fwd (x : u32) (y : u32) : result (pair_t u32 u32) =
+ Return (Mkpair_t x y)
+
+(** [constants::P0] *)
+let p0_fwd : result (u32 & u32) =
+ begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+
+(** [constants::P1] *)
+let p1_fwd : result (pair_t u32 u32) =
+ begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+
+(** [constants::P2] *)
+let p2_fwd : result (u32 & u32) = Return (0, 1)
+
+(** [constants::P3] *)
+let p3_fwd : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
+
+(** [constants::Wrap] *)
+type wrap_t (t : Type0) = { wrap_val : t; }
+
+(** [constants::Wrap::{0}::new] *)
+let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
+ Return (Mkwrap_t val0)
+
+(** [constants::Y] *)
+let y_fwd : result (wrap_t i32) =
+ begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
+
+(** [constants::unwrap_y] *)
+let unwrap_y_fwd : result i32 =
+ begin match y_fwd with | Fail -> Fail | Return w -> Return w.wrap_val end
+
+(** [constants::YVAL] *)
+let yval_fwd : result i32 =
+ begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::get_z1::Z1] *)
+let get_z1_z1_fwd : result i32 = Return 3
+
+(** [constants::get_z1] *)
+let get_z1_fwd : result i32 =
+ begin match get_z1_z1_fwd with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::add] *)
+let add_fwd (a : i32) (b : i32) : result i32 =
+ begin match i32_add a b with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::Q1] *)
+let q1_fwd : result i32 = Return 5
+
+(** [constants::Q2] *)
+let q2_fwd : result i32 =
+ begin match q1_fwd with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::Q3] *)
+let q3_fwd : result i32 =
+ begin match q2_fwd with
+ | Fail -> Fail
+ | Return i ->
+ begin match add_fwd i 3 with | Fail -> Fail | Return i0 -> Return i0 end
+ end
+
+(** [constants::get_z2] *)
+let get_z2_fwd : result i32 =
+ begin match get_z1_fwd with
+ | Fail -> Fail
+ | Return i ->
+ begin match q3_fwd with
+ | Fail -> Fail
+ | Return i0 ->
+ begin match add_fwd i i0 with
+ | Fail -> Fail
+ | Return i1 ->
+ begin match q1_fwd with
+ | Fail -> Fail
+ | Return i2 ->
+ begin match add_fwd i2 i1 with
+ | Fail -> Fail
+ | Return i3 -> Return i3
+ end
+ end
+ end
+ end
+ end
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 17:49:16 +0000