diff --git a/asllib/Typing.ml b/asllib/Typing.ml index 7f25c1529d..b3d80f3d81 100644 --- a/asllib/Typing.ml +++ b/asllib/Typing.ml @@ -154,9 +154,42 @@ let min_max_constraints m_constraint m = let min_constraints = min_max_constraints min_constraint min and max_constraints = min_max_constraints max_constraint max +let disjoint_slices_to_diet loc env slices = + let eval env e = + match reduce_constants env e with + | L_Int z -> Z.to_int z + | _ -> fatal_from e @@ Error.UnsupportedExpr e + in + let module DI = Diet.Int in + let one_slice loc env diet slice = + let interval = + let make x y = + if x > y then fatal_from loc @@ Error.OverlappingSlices [ slice ] + else DI.Interval.make x y + in + match slice with + | Slice_Single e -> + let x = eval env e in + make x x + | Slice_Range (e1, e2) -> + let x = eval env e2 and y = eval env e1 in + make x y + | Slice_Length (e1, e2) -> + let x = eval env e1 and y = eval env e2 in + make x (x + y - 1) + | Slice_Star (e1, e2) -> + let x = eval env e1 and y = eval env e2 in + make (x * y) ((x * (y + 1)) - 1) + in + let new_diet = DI.add interval DI.empty in + if DI.is_empty (Diet.Int.inter new_diet diet) then DI.add interval diet + else fatal_from loc Error.(OverlappingSlices slices) + in + List.fold_left (one_slice loc env) Diet.Int.empty slices + (* --------------------------------------------------------------------------- - Main type-checking module + Properties handling ---------------------------------------------------------------------------*) @@ -166,7 +199,7 @@ module type ANNOTATE_CONFIG = sig val check : strictness end -module Annotate (C : ANNOTATE_CONFIG) = struct +module Property (C : ANNOTATE_CONFIG) = struct exception TypingAssumptionFailed type ('a, 'b) property = 'a -> 'b @@ -185,17 +218,18 @@ module Annotate (C : ANNOTATE_CONFIG) = struct fun f () -> try f () with Error.ASLException e -> Error.eprintln e) | `Silence -> fun _f () -> () - let best_effort : 'a -> ('a -> 'a) -> 'a = + let best_effort' : ('a, 'a) property -> ('a, 'a) property = match C.check with - | `TypeCheck -> fun x f -> f x + | `TypeCheck -> fun f x -> f x | `Warn -> ( - fun x f -> + fun f x -> try f x with Error.ASLException e -> Error.eprintln e; x) - | `Silence -> ( fun x f -> try f x with Error.ASLException _ -> x) + | `Silence -> ( fun f x -> try f x with Error.ASLException _ -> x) + let best_effort : 'a -> ('a, 'a) property -> 'a = fun x f -> best_effort' f x let[@inline] ( let+ ) m f = check m () |> f let[@inline] both (p1 : prop) (p2 : prop) () = @@ -207,7 +241,6 @@ module Annotate (C : ANNOTATE_CONFIG) = struct try p1 x with TypingAssumptionFailed | Error.ASLException _ -> p2 x let ( &&& ) = both - let all (li : prop list) : prop = fun () -> List.iter (fun f -> f ()) li let map_all (f : 'a -> prop) (li : 'a list) : prop = fun () -> List.iter (fun x -> f x ()) li @@ -228,146 +261,149 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let assumption_failed () = raise_notrace TypingAssumptionFailed [@@inline] let check_true b fail () = if b then () else fail () [@@inline] let check_true' b = check_true b assumption_failed [@@inline] +end - (* ------------------------------------------------------------------------- - - Functional polymorphism - - ------------------------------------------------------------------------- *) - - module FunctionRenaming = struct - (* Returns true iff type lists type-clash element-wise. *) - let has_arg_clash env caller callee = - List.compare_lengths caller callee == 0 - && List.for_all2 - (fun t_caller (_, t_callee) -> - Types.type_clashes env t_caller t_callee) - caller callee - - (* Return true if two subprogram are forbidden with the same argument types. *) - let has_subprogram_type_clash s1 s2 = - match (s1, s2) with - | ST_Function, _ | _, ST_Function | ST_Procedure, _ | _, ST_Procedure -> - true - | ST_Getter, ST_Getter | ST_Setter, ST_Setter -> true - | ST_Getter, ST_Setter | ST_Setter, ST_Getter -> false - - (* Deduce renamings from match between calling and callee types. *) - let deduce_eqs env = - (* Here we assume [has_arg_clash env caller callee] *) - (* Thus [List.length caller == List.length callee]. *) - let folder prev_eqs caller (_name, callee) = - match callee.desc with - | T_Bits ({ desc = E_Var x; _ }, _) -> ( - match (Types.get_structure env caller).desc with - | T_Bits (e_caller, _) -> (x, e_caller) :: prev_eqs - | _ -> - (* We know that callee type_clashes with caller, and that it - cannot be a name. *) - assert false) - | _ -> prev_eqs - in - List.fold_left2 folder [] - - let add_new_func loc env name arg_types subpgm_type = - match IMap.find_opt name env.global.subprogram_renamings with - | None -> - let env = set_renamings name (ISet.singleton name) env in - (env, name) - | Some set -> - let name' = name ^ "-" ^ string_of_int (ISet.cardinal set) in - let clash = - let arg_types = List.map snd arg_types in - (not (ISet.is_empty set)) - && ISet.exists - (fun name'' -> - let other_func_sig = - IMap.find name'' env.global.subprograms - in - has_subprogram_type_clash subpgm_type - other_func_sig.subprogram_type - && has_arg_clash env arg_types other_func_sig.args) - set - in - let+ () = - fun () -> - if clash then - let () = - if false then - Format.eprintf - "Function %s@[(%a)@] is declared multiple times.@." name - Format.( - pp_print_list - ~pp_sep:(fun f () -> fprintf f ",@ ") - PP.pp_typed_identifier) - arg_types - in - Error.fatal_from loc (Error.AlreadyDeclaredIdentifier name) - in - let env = set_renamings name (ISet.add name' set) env in - (env, name') +(* ------------------------------------------------------------------------- + + Functional polymorphism + + ------------------------------------------------------------------------- *) + +module FunctionRenaming (C : ANNOTATE_CONFIG) = struct + open Property (C) + + (* Returns true iff type lists type-clash element-wise. *) + let has_arg_clash env caller callee = + List.compare_lengths caller callee == 0 + && List.for_all2 + (fun t_caller (_, t_callee) -> + Types.type_clashes env t_caller t_callee) + caller callee + + (* Return true if two subprogram are forbidden with the same argument types. *) + let has_subprogram_type_clash s1 s2 = + match (s1, s2) with + | ST_Function, _ | _, ST_Function | ST_Procedure, _ | _, ST_Procedure -> + true + | ST_Getter, ST_Getter | ST_Setter, ST_Setter -> true + | ST_Getter, ST_Setter | ST_Setter, ST_Getter -> false + + (* Deduce renamings from match between calling and callee types. *) + let deduce_eqs env = + (* Here we assume [has_arg_clash env caller callee] *) + (* Thus [List.length caller == List.length callee]. *) + let folder prev_eqs caller (_name, callee) = + match callee.desc with + | T_Bits ({ desc = E_Var x; _ }, _) -> ( + match (Types.get_structure env caller).desc with + | T_Bits (e_caller, _) -> (x, e_caller) :: prev_eqs + | _ -> + (* We know that callee type_clashes with caller, and that it + cannot be a name. *) + assert false) + | _ -> prev_eqs + in + List.fold_left2 folder [] + + let add_new_func loc env name arg_types subpgm_type = + match IMap.find_opt name env.global.subprogram_renamings with + | None -> + let env = set_renamings name (ISet.singleton name) env in + (env, name) + | Some set -> + let name' = name ^ "-" ^ string_of_int (ISet.cardinal set) in + let clash = + let arg_types = List.map snd arg_types in + (not (ISet.is_empty set)) + && ISet.exists + (fun name'' -> + let other_func_sig = IMap.find name'' env.global.subprograms in + has_subprogram_type_clash subpgm_type + other_func_sig.subprogram_type + && has_arg_clash env arg_types other_func_sig.args) + set + in + let+ () = + fun () -> + if clash then + let () = + if false then + Format.eprintf + "Function %s@[(%a)@] is declared multiple times.@." name + Format.( + pp_print_list + ~pp_sep:(fun f () -> fprintf f ",@ ") + PP.pp_typed_identifier) + arg_types + in + Error.fatal_from loc (Error.AlreadyDeclaredIdentifier name) + in + let env = set_renamings name (ISet.add name' set) env in + (env, name') - let find_name loc env name caller_arg_types = - let () = - if false then Format.eprintf "Trying to rename call to %S@." name - in - match IMap.find_opt name env.global.subprogram_renamings with - | None -> ( - match IMap.find_opt name env.global.subprograms with - | Some func_sig -> - let callee_arg_types = func_sig.args in - if has_arg_clash env caller_arg_types callee_arg_types then - let () = - if false then - Format.eprintf "Found already translated name: %S.@." name - in - ( deduce_eqs env caller_arg_types callee_arg_types, - name, - callee_arg_types, - func_sig.return_type ) - else - fatal_from loc (Error.NoCallCandidate (name, caller_arg_types)) - | None -> undefined_identifier loc name) - | Some set -> ( - let finder name' acc = - let func_sig = IMap.find name' env.global.subprograms in + let find_name loc env name caller_arg_types = + let () = + if false then Format.eprintf "Trying to rename call to %S@." name + in + match IMap.find_opt name env.global.subprogram_renamings with + | None -> ( + match IMap.find_opt name env.global.subprograms with + | Some func_sig -> let callee_arg_types = func_sig.args in if has_arg_clash env caller_arg_types callee_arg_types then + let () = + if false then + Format.eprintf "Found already translated name: %S.@." name + in ( deduce_eqs env caller_arg_types callee_arg_types, - name', + name, callee_arg_types, func_sig.return_type ) - :: acc - else acc - in - match ISet.fold finder set [] with - | [] -> - fatal_from loc (Error.NoCallCandidate (name, caller_arg_types)) - | [ (eqs, name', callee_arg_types, ret_type) ] -> - (eqs, name', callee_arg_types, ret_type) - | _ :: _ -> - fatal_from loc - (Error.TooManyCallCandidates (name, caller_arg_types))) - - let try_find_name loc env name caller_arg_types = - try find_name loc env name caller_arg_types - with Error.ASLException _ as error -> ( - try - match IMap.find_opt name env.global.subprograms with - | None -> undefined_identifier loc ("function " ^ name) - | Some { args = callee_arg_types; return_type; _ } -> - if false then - Format.eprintf "@[<2>%a:@ No extra arguments for %s@]@." - PP.pp_pos loc name; - ([], name, callee_arg_types, return_type) - with Error.ASLException _ -> raise error) - end + else fatal_from loc (Error.NoCallCandidate (name, caller_arg_types)) + | None -> undefined_identifier loc name) + | Some set -> ( + let finder name' acc = + let func_sig = IMap.find name' env.global.subprograms in + let callee_arg_types = func_sig.args in + if has_arg_clash env caller_arg_types callee_arg_types then + ( deduce_eqs env caller_arg_types callee_arg_types, + name', + callee_arg_types, + func_sig.return_type ) + :: acc + else acc + in + match ISet.fold finder set [] with + | [] -> fatal_from loc (Error.NoCallCandidate (name, caller_arg_types)) + | [ (eqs, name', callee_arg_types, ret_type) ] -> + (eqs, name', callee_arg_types, ret_type) + | _ :: _ -> + fatal_from loc + (Error.TooManyCallCandidates (name, caller_arg_types))) + + let try_find_name loc env name caller_arg_types = + try find_name loc env name caller_arg_types + with Error.ASLException _ as error -> ( + try + match IMap.find_opt name env.global.subprograms with + | None -> undefined_identifier loc ("function " ^ name) + | Some { args = callee_arg_types; return_type; _ } -> + if false then + Format.eprintf "@[<2>%a:@ No extra arguments for %s@]@." PP.pp_pos + loc name; + ([], name, callee_arg_types, return_type) + with Error.ASLException _ -> raise error) +end + +(* --------------------------------------------------------------------------- - (* ------------------------------------------------------------------------- + Main type-checking module - Handling of Getters and Setters + ---------------------------------------------------------------------------*) - -------------------------------------------------------------------------- *) +module Annotate (C : ANNOTATE_CONFIG) = struct + open Property (C) + module Fn = FunctionRenaming (C) let should_reduce_to_call env name = IMap.mem name env.global.subprogram_renamings @@ -381,44 +417,6 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | None -> None | Some args -> if should_reduce_to_call env name then Some args else None - let disjoint_slices_to_diet loc env slices = - let eval env e = - match reduce_constants env e with - | L_Int z -> Z.to_int z - | _ -> fatal_from e @@ Error.UnsupportedExpr e - in - let module DI = Diet.Int in - let one_slice loc env diet slice = - let interval = - let make x y = - if x > y then fatal_from loc @@ Error.OverlappingSlices [ slice ] - else DI.Interval.make x y - in - match slice with - | Slice_Single e -> - let x = eval env e in - make x x - | Slice_Range (e1, e2) -> - let x = eval env e2 and y = eval env e1 in - make x y - | Slice_Length (e1, e2) -> - let x = eval env e1 and y = eval env e2 in - make x (x + y - 1) - | Slice_Star (e1, e2) -> - let x = eval env e1 and y = eval env e2 in - make (x * y) ((x * (y + 1)) - 1) - in - let new_diet = DI.add interval DI.empty in - if DI.is_empty (Diet.Int.inter new_diet diet) then DI.add interval diet - else fatal_from loc Error.(OverlappingSlices slices) - in - List.fold_left (one_slice loc env) Diet.Int.empty slices - - (* ------------------------------------------------------------------------- - - Annotate AST - - -------------------------------------------------------------------------- *) let check_type_satisfies' env t1 t2 () = let () = if false then @@ -497,8 +495,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let check_bits_equal_width' env t1 t2 () = let n = get_bitvector_width' env t1 and m = get_bitvector_width' env t2 in - if bitwidth_equal (StaticInterpreter.equal_in_env env) n m then - (* TODO: Check statically evaluable? *) () + if bitwidth_equal (StaticInterpreter.equal_in_env env) n m then () else assumption_failed () let check_bits_equal_width loc env t1 t2 () = @@ -509,10 +506,6 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let has_bitvector_structure env t = match (Types.get_structure env t).desc with T_Bits _ -> true | _ -> false - let t_bool = T_Bool |> __POS_OF__ |> add_pos_from_pos_of - let t_int = T_Int UnConstrained |> __POS_OF__ |> add_pos_from_pos_of - let t_real = T_Real |> __POS_OF__ |> add_pos_from_pos_of - let expr_is_strict_positive e = match e.desc with | E_Literal (L_Int i) -> Z.sign i = 1 @@ -551,8 +544,8 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (fun () -> match op with | BAND | BOR | BEQ | IMPL -> - let+ () = check_type_satisfies' env t1 t_bool in - let+ () = check_type_satisfies' env t2 t_bool in + let+ () = check_type_satisfies' env t1 boolean in + let+ () = check_type_satisfies' env t2 boolean in T_Bool |> with_loc | AND | OR | EOR (* when has_bitvector_structure env t1 ? *) -> (* Rule KXMR: If the operands of a primitive operation are @@ -568,7 +561,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let+ () = either (check_bits_equal_width' env t1 t2) - (check_type_satisfies' env t2 t_int) + (check_type_satisfies' env t2 integer) in let w = get_bitvector_width' env t1 in T_Bits (w, []) |> with_loc @@ -583,16 +576,16 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* If an argument of a comparison operation is a constrained integer then it is treated as an unconstrained integer. *) both - (check_type_satisfies' env t1 t_int) - (check_type_satisfies' env t2 t_int); + (check_type_satisfies' env t1 integer) + (check_type_satisfies' env t2 integer); (* If the arguments of a comparison operation are bitvectors then they must have the same determined width. *) check_bits_equal_width' env t1 t2; (* The rest are redundancies from the first equal types cases, but provided for completeness. *) both - (check_type_satisfies' env t1 t_bool) - (check_type_satisfies' env t2 t_bool); + (check_type_satisfies' env t1 boolean) + (check_type_satisfies' env t2 boolean); (fun () -> match (t1.desc, t2.desc) with | T_Enum li1, T_Enum li2 -> @@ -605,16 +598,14 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let+ () = either (both - (check_type_satisfies' env t1 t_int) - (check_type_satisfies' env t2 t_int)) + (check_type_satisfies' env t1 integer) + (check_type_satisfies' env t2 integer)) (both - (check_type_satisfies' env t1 t_real) - (check_type_satisfies' env t2 t_real)) + (check_type_satisfies' env t1 real) + (check_type_satisfies' env t2 real)) in T_Bool |> with_loc | MUL | DIV | DIVRM | MOD | SHL | SHR | POW | PLUS | MINUS -> ( - (* TODO: ensure that we mean "has the structure of" instead of - "is" *) let struct1 = Types.get_structure env t1 and struct2 = Types.get_structure env t2 in let struct1' = @@ -640,7 +631,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let+ () = match op with | DIV -> - (* TODO cs1 divides cs1 ? How is it expressable in term of constraints? *) + (* TODO cs1 divides cs2 ? How is it expressable in term of constraints? *) check_true' (constraints_is_strict_positive cs2) | DIVRM | MOD -> (* assert cs2 strict-positive *) @@ -750,13 +741,13 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let check_unop loc env op t1 = match op with | BNOT -> - let+ () = check_type_satisfies loc env t1 t_bool in + let+ () = check_type_satisfies loc env t1 boolean in T_Bool |> add_pos_from loc | NEG -> ( let+ () = either - (check_type_satisfies loc env t1 t_int) - (check_type_satisfies loc env t1 t_real) + (check_type_satisfies loc env t1 integer) + (check_type_satisfies loc env t1 real) in let t1' = Types.UnderConstrainedInteger.to_well_constrained t1 in match (Types.get_structure env t1').desc with @@ -786,7 +777,6 @@ module Annotate (C : ANNOTATE_CONFIG) = struct structure of the under-constrained integer type, may only be assigned or initialized with a value of type T if T type-satisfies S *) - (* TODO: incomplete. *) (* Begin CanAssignTo *) let can_assign_to env s t = let s_struct = Types.get_structure env s @@ -808,13 +798,6 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Rules: - Rule WZCS: The width of a bitslice must be any non-negative, statically evaluable integer expression (including zero). - - Rule KTBG: It is an error if any bits selected by a bitslice are not - in range for the expression being sliced. If the offset of a bitslice - depends on a statically evaluable expression then this shall be - checked at compile time. Otherwise a bounds check will occur at - execution-time and an implementation defined exception shall be thrown - if it fails. - TODO: check them *) let rec tr_one = function (* Begin SliceSingle *) @@ -831,8 +814,6 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let+ () = check_structure_integer offset' env t_offset in let+ () = check_structure_integer length' env t_length in let+ () = check_statically_evaluable env length in - (* TODO: if offset is statically evaluable, check that it is less - than sliced expression width. *) Slice_Length (offset', length') |: TypingRule.SliceLength (* End *) (* Begin SliceRange *) @@ -876,8 +857,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let t_struct = Types.get_structure env t and t_e_struct = Types.get_structure env t_e in match (t_struct.desc, t_e_struct.desc) with - | T_Bool, T_Bool | T_Real, T_Real -> () - | T_Int _, T_Int _ -> () + | T_Bool, T_Bool | T_Real, T_Real | T_Int _, T_Int _ -> () | T_Bits _, T_Bits _ -> check_bits_equal_width loc env t_struct t_e_struct () (* TODO: Multiple discriminants can be matched at once by forming @@ -895,9 +875,12 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let t_e, e' = annotate_expr env e in let+ () = check_statically_evaluable env e' in let+ () = - both (* TODO: case where they are both real *) - (check_structure_integer loc env t) - (check_structure_integer loc env t_e) + fun () -> + let t_struct = Types.get_structure env t + and t_e_struct = Types.get_structure env t_e in + match (t_struct.desc, t_e_struct.desc) with + | T_Real, T_Real | T_Int _, T_Int _ -> () + | _ -> fatal_from loc (Error.BadTypesForBinop (GEQ, t, t_e)) in Pattern_Geq e' |: TypingRule.PGeq (* End *) @@ -917,12 +900,15 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let t_e1, e1' = annotate_expr env e1 and t_e2, e2' = annotate_expr env e2 in let+ () = - all - [ - check_structure_integer loc env t; - check_structure_integer loc env t_e1; - check_structure_integer loc env t_e2; - ] + fun () -> + let t_struct = Types.get_structure env t + and t_e1_struct = Types.get_structure env t_e1 + and t_e2_struct = Types.get_structure env t_e2 in + match (t_struct.desc, t_e1_struct.desc, t_e2_struct.desc) with + | T_Real, T_Real, T_Real | T_Int _, T_Int _, T_Int _ -> () + | _, T_Int _, T_Int _ | _, T_Real, T_Real -> + fatal_from loc (Error.BadTypesForBinop (GEQ, t, t_e1)) + | _ -> fatal_from loc (Error.BadTypesForBinop (GEQ, t_e1, t_e2)) in Pattern_Range (e1', e2') |: TypingRule.PRange (* End *) @@ -964,7 +950,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let caller_arg_typed = List.map (annotate_expr env) args in let caller_arg_types, args1 = List.split caller_arg_typed in let extra_nargs, name1, callee_arg_types, ret_ty = - FunctionRenaming.try_find_name loc env name caller_arg_types + Fn.try_find_name loc env name caller_arg_types in let () = if false then @@ -1061,6 +1047,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct the required type, an execution-time check that the expression evaluates to a value in the domain of the required type is required. *) + let+ () = check_is_valid_type e env t' in best_effort (t', E_CTC (e'', t') |> here) (fun res -> @@ -1243,6 +1230,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Begin EUnknown *) | E_Unknown ty -> let ty' = Types.get_structure env ty in + let+ () = check_is_valid_type e env ty in (ty, E_Unknown ty' |> here) |: TypingRule.EUnknown (* End *) | E_Slice (e', slices) -> ( @@ -1277,7 +1265,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Begin EGetArray *) | T_Array (size, ty') -> ( let wanted_t_index = - let t_int = + let integer = T_Int (WellConstrained [ Constraint_Range (!$0, binop MINUS size !$1) ]) @@ -1287,8 +1275,8 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | E_Var name -> ( match IMap.find_opt name env.global.declared_types with | Some t -> t (* TODO check that this is an enum *) - | None -> t_int) - | _ -> t_int + | None -> integer) + | _ -> integer in match slices with | [ Slice_Single e_index ] -> @@ -1473,7 +1461,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let le2 = annotate_lexpr env le1 t_le1 in let+ () = check_can_assign_to le2 env t t_e in let wanted_t_index = - let t_int = + let integer = T_Int (WellConstrained [ Constraint_Range (!$0, binop MINUS size !$1) ]) @@ -1483,8 +1471,8 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | E_Var name -> ( match IMap.find_opt name env.global.declared_types with | Some t -> t - | None -> t_int) - | _ -> t_int + | None -> integer) + | _ -> integer in match slices with | [ Slice_Single e_index ] -> @@ -1630,6 +1618,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* End *) (* Begin LDDiscardSome *) | LDI_Discard (Some t) -> + let+ () = check_is_valid_type loc env t in let+ () = check_can_be_initialized_with loc env t ty in (env, ldi) |: TypingRule.LDDiscardSome (* End *) @@ -1640,6 +1629,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct match ty_opt with | None -> ty | Some t -> + let+ () = check_is_valid_type loc env t in let+ () = check_can_be_initialized_with loc env t ty in t in @@ -1683,12 +1673,16 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Here implicitly ldk=LDK_Var *) let here s = add_pos_from loc s in match ldi with - | LDI_Discard _ -> (env, S_Pass |> here) + | LDI_Discard (Some t) -> + let+ () = check_is_valid_type loc env t in + (env, S_Pass |> here) + | LDI_Discard None -> (env, S_Pass |> here) | LDI_Var (_, None) -> fatal_from loc (Error.NotYetImplemented "Variable declaration needs a type.") |: TypingRule.LDUninitialisedVar | LDI_Var (x, Some t) -> + let+ () = check_is_valid_type loc env t in let+ () = check_var_not_in_env loc env x in ( add_local x t LDK_Var env, S_Decl (LDK_Var, LDI_Var (x, Some t), None) |> here ) @@ -1699,6 +1693,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct in (env, stmt_from_list ss) |: TypingRule.LDUninitialisedTuple | LDI_Tuple (ldis, Some t) -> + let+ () = check_is_valid_type loc env t in let env, les = list_fold_left_map (fun env' -> annotate_local_decl_item loc env' t LDK_Var) @@ -1793,7 +1788,6 @@ module Annotate (C : ANNOTATE_CONFIG) = struct annotate_call (to_pos s) env name args eqs ST_Procedure in let () = assert (ty = None) in - (* TODO: check that call does not returns anything. *) (S_Call (new_name, new_args, new_eqs) |> here, env) |: TypingRule.SCall (* End *) | S_Return e_opt -> @@ -1827,7 +1821,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Begin SCond *) | S_Cond (e, s1, s2) -> let t_cond, e_cond = annotate_expr env e in - let+ () = check_type_satisfies e_cond env t_cond t_bool in + let+ () = check_type_satisfies e_cond env t_cond boolean in let s1' = try_annotate_block env s1 in let s2' = try_annotate_block env s2 in (S_Cond (e_cond, s1', s2') |> here, env) |: TypingRule.SCond @@ -1847,13 +1841,13 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Begin SAssert *) | S_Assert e -> let t_e', e' = annotate_expr env e in - let+ () = check_type_satisfies s env t_e' t_bool in + let+ () = check_type_satisfies s env t_e' boolean in (S_Assert e' |> here, env) |: TypingRule.SAssert (* End *) (* Begin SWhile *) | S_While (e1, s1) -> let t, e2 = annotate_expr env e1 in - let+ () = check_type_satisfies e2 env t t_bool in + let+ () = check_type_satisfies e2 env t boolean in let s2 = try_annotate_block env s1 in (S_While (e2, s2) |> here, env) |: TypingRule.SWhile (* End *) @@ -1861,7 +1855,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | S_Repeat (s1, e1) -> let s2 = try_annotate_block env s1 in let t, e2 = annotate_expr env e1 in - let+ () = check_type_satisfies e2 env t t_bool in + let+ () = check_type_satisfies e2 env t boolean in (S_Repeat (s2, e2) |> here, env) |: TypingRule.SRepeat (* End *) (* Begin SFor *) @@ -1950,6 +1944,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (S_Debug e' |> here, env) |: TypingRule.SDebug and annotate_catcher env (name_opt, ty, stmt) = + let+ () = check_is_valid_type ty env ty in let+ () = check_structure_exception ty env ty in let env' = match name_opt with @@ -2111,18 +2106,19 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let try_annotate_subprogram loc env f = best_effort f (annotate_subprogram loc env) - let annotate_gsd env gsd = + let annotate_gsd loc env gsd = match gsd with | { initial_value = Some e; ty = None; _ } -> let t, e = annotate_expr env e in { gsd with initial_value = Some e; ty = Some t } | { initial_value = Some e; ty = Some t; _ } -> let t', e = annotate_expr env e in - let+ () = check_can_be_initialized_with e env t t' in + let+ () = check_is_valid_type loc env t in + let+ () = check_can_be_initialized_with loc env t t' in { gsd with initial_value = Some e; ty = Some t } | _ -> gsd - let try_annotate_gsd env gsd = best_effort gsd (annotate_gsd env) + let try_annotate_gsd loc env gsd = best_effort gsd (annotate_gsd loc env) (******************************************************************************) (* *) @@ -2133,7 +2129,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let declare_one_func loc (func_sig : func) env = let env, name' = best_effort (env, func_sig.name) @@ fun _ -> - FunctionRenaming.add_new_func loc env func_sig.name func_sig.args + Fn.add_new_func loc env func_sig.name func_sig.args func_sig.subprogram_type in let () = @@ -2261,7 +2257,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct in declare_one_func d f' env | D_GlobalStorage gsd -> - let gsd' = try_annotate_gsd env gsd in + let gsd' = try_annotate_gsd d env gsd in declare_global_storage d gsd' env | D_TypeDecl (x, ty, s) -> declare_type d x ty s env