diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Logging.ml | 3 | ||||
| -rw-r--r-- | src/PureUtils.ml | 18 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 44 | ||||
| -rw-r--r-- | src/main.ml | 2 |
4 files changed, 53 insertions, 14 deletions
diff --git a/src/Logging.ml b/src/Logging.ml index f4fa9309..55b07ed4 100644 --- a/src/Logging.ml +++ b/src/Logging.ml @@ -15,6 +15,9 @@ let pre_passes_log = L.get_logger "MainLogger.PrePasses" (** Logger for Translate *) let translate_log = L.get_logger "MainLogger.Translate" +(** Logger for PureUtils *) +let pure_utils_log = L.get_logger "MainLogger.PureUtils" + (** Logger for SymbolicToPure *) let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure" diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 662902e6..1ed072e9 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -1,5 +1,8 @@ open Pure +(** Default logger *) +let log = Logging.pure_utils_log + type regular_fun_id = A.fun_id * T.RegionGroupId.id option [@@deriving show, ord] (** We use this type as a key for lookups *) @@ -270,7 +273,6 @@ module TypeCheck = struct let check_adt_g_value (ctx : tc_ctx) (check_value : ty -> 'v -> unit) (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) : unit = - (* let field_values = List.map value_to_string field_values in *) (* Retrieve the field types *) let field_tys = match ty with @@ -312,17 +314,23 @@ module TypeCheck = struct (List.combine field_tys field_values) let rec check_typed_lvalue (ctx : tc_ctx) (v : typed_lvalue) : unit = + log#ldebug (lazy ("check_typed_lvalue: " ^ show_typed_lvalue v)); match v.value with | LvConcrete cv -> check_constant_value v.ty cv | LvVar _ -> () | LvAdt av -> check_adt_g_value ctx (fun ty (v : typed_lvalue) -> - assert (ty = v.ty); + if ty <> v.ty then ( + log#serror + ("check_typed_lvalue: not the same types:" ^ "\n- ty: " + ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty); + raise (Failure "Inconsistent types")); check_typed_lvalue ctx v) av.variant_id av.field_values v.ty let rec check_typed_rvalue (ctx : tc_ctx) (v : typed_rvalue) : unit = + log#ldebug (lazy ("check_typed_rvalue: " ^ show_typed_rvalue v)); match v.value with | RvConcrete cv -> check_constant_value v.ty cv | RvPlace _ -> @@ -331,7 +339,11 @@ module TypeCheck = struct | RvAdt av -> check_adt_g_value ctx (fun ty (v : typed_rvalue) -> - assert (ty = v.ty); + if ty <> v.ty then ( + log#serror + ("check_typed_rvalue: not the same types:" ^ "\n- ty: " + ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty); + raise (Failure "Inconsistent types")); check_typed_rvalue ctx v) av.variant_id av.field_values v.ty end diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 0a4d0176..1967732d 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -200,7 +200,10 @@ let rec translate_sty (ty : T.sty) : ty = | T.Tuple -> mk_simpl_tuple_ty tys | T.Assumed aty -> ( match aty with - | T.Box | T.Vec | T.Option -> ( + | T.Vec -> Adt (Assumed Vec, tys) + | T.Option -> Adt (Assumed Option, tys) + | T.Box -> ( + (* Eliminate the boxes *) match tys with | [ ty ] -> ty | _ -> @@ -265,17 +268,25 @@ let rec translate_fwd_ty (types_infos : TA.type_infos) (ty : 'r T.ty) : ty = assert (regions = []); (* Translate the type parameters *) let t_tys = List.map translate tys in - (* Eliminate boxes *) + (* Eliminate boxes and simplify tuples *) match type_id with - | AdtId adt_id -> + | AdtId _ | T.Assumed (T.Vec | T.Option) -> (* No general parametricity for now *) assert (not (List.exists (TypesUtils.ty_has_borrows types_infos) tys)); - Adt (AdtId adt_id, t_tys) + let type_id = + match type_id with + | AdtId adt_id -> AdtId adt_id + | T.Assumed T.Vec -> Assumed Vec + | T.Assumed T.Option -> Assumed Option + | _ -> raise (Failure "Unreachable") + in + Adt (type_id, t_tys) | Tuple -> (* Note that if there is exactly one type, [mk_simpl_tuple_ty] is the identity *) mk_simpl_tuple_ty t_tys - | T.Assumed (T.Box | T.Vec | T.Option) -> ( + | T.Assumed T.Box -> ( + (* We eliminate boxes *) (* No general parametricity for now *) assert (not (List.exists (TypesUtils.ty_has_borrows types_infos) tys)); match t_tys with @@ -317,20 +328,21 @@ let rec translate_back_ty (types_infos : TA.type_infos) match ty with | T.Adt (type_id, _, tys) -> ( match type_id with - | T.AdtId _ -> + | T.AdtId _ | Assumed (T.Vec | T.Option) -> (* Don't accept ADTs (which are not tuples) with borrows for now *) assert (not (TypesUtils.ty_has_borrows types_infos ty)); let type_id = match type_id with | T.AdtId id -> AdtId id - | T.Tuple | T.Assumed (T.Box | T.Vec | T.Option) -> - failwith "Unreachable" + | T.Assumed T.Vec -> Assumed Vec + | T.Assumed T.Option -> Assumed Option + | T.Tuple | T.Assumed T.Box -> failwith "Unreachable" in if inside_mut then let tys_t = List.filter_map translate tys in Some (Adt (type_id, tys_t)) else None - | Assumed (T.Box | T.Vec | T.Option) -> ( + | Assumed T.Box -> ( (* Don't accept ADTs (which are not tuples) with borrows for now *) assert (not (TypesUtils.ty_has_borrows types_infos ty)); (* Eliminate the box *) @@ -576,10 +588,15 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue let value = match v.value with | V.Concrete cv -> RvConcrete cv - | Adt av -> + | Adt av -> ( let variant_id = av.variant_id in let field_values = List.map translate av.field_values in - RvAdt { variant_id; field_values } + (* Eliminate the tuple wrapper if it is a tuple with exactly one field *) + match v.ty with + | T.Adt (T.Tuple, _, _) -> + assert (variant_id = None); + (mk_simpl_tuple_rvalue field_values).value + | _ -> RvAdt { variant_id; field_values }) | Bottom -> failwith "Unreachable" | Loan lc -> ( match lc with @@ -601,6 +618,11 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue in let ty = ctx_translate_fwd_ty ctx v.ty in let value = { value; ty } in + (* Debugging *) + log#ldebug + (lazy + ("typed_value_to_rvalue: result:" ^ "\n- input:\n" ^ V.show_typed_value v + ^ "\n- typed rvalue:\n" ^ show_typed_rvalue value)); (* Sanity check *) type_check_rvalue ctx value; (* Return *) diff --git a/src/main.ml b/src/main.ml index ca05ba78..193b20c2 100644 --- a/src/main.ml +++ b/src/main.ml @@ -92,6 +92,7 @@ let () = * command-line arguments *) Easy_logging.Handlers.set_level main_logger_handler EL.Debug; main_log#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; @@ -99,6 +100,7 @@ let () = expansion_log#set_level EL.Debug; borrows_log#set_level EL.Debug; invariants_log#set_level EL.Warning; + 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; |