From 064eab3a0e281499fbf639801553c37dab5fa2c1 Mon Sep 17 00:00:00 2001 From: Hadrien Renaud Date: Mon, 8 Jan 2024 09:36:12 +0000 Subject: [PATCH 1/5] [asl] Check type validity on user input --- asllib/AST.mli | 9 +- asllib/ASTUtils.ml | 13 +- asllib/Interpreter.ml | 46 +- asllib/PP.ml | 4 +- asllib/Parser.mly | 14 +- asllib/Serialize.ml | 8 +- asllib/StaticEnv.ml | 3 + asllib/StaticInterpreter.ml | 44 +- asllib/Typing.ml | 1092 +++++++++++--------- asllib/libdir/stdlib.asl | 2 +- asllib/tests/ASLSemanticsReference.t/run.t | 2 +- asllib/tests/asl.t/enum-array.asl | 20 + asllib/tests/asl.t/run.t | 8 +- asllib/tests/bad-types.t | 6 +- asllib/tests/recursive.t/run.t | 3 + asllib/types.ml | 16 +- 16 files changed, 756 insertions(+), 534 deletions(-) create mode 100644 asllib/tests/asl.t/enum-array.asl diff --git a/asllib/AST.mli b/asllib/AST.mli index cf1f8b529..9fdb15500 100644 --- a/asllib/AST.mli +++ b/asllib/AST.mli @@ -174,7 +174,7 @@ and type_desc = | T_Bool | T_Enum of identifier list | T_Tuple of ty list - | T_Array of expr * ty + | T_Array of array_index * ty | T_Record of field list | T_Exception of field list | T_Named of identifier (** A type variable. *) @@ -208,6 +208,13 @@ and bitfield = | BitField_Type of identifier * slice list * ty (** A name, its corresponding slice and the type of the bitfield. *) +(** The type of indexes for an array. *) +and array_index = + | ArrayLength_Expr of expr + (** An integer expression giving the length of the array. *) + | ArrayLength_Enum of identifier * int + (** An enumeration name and its length. *) + and field = identifier * ty (** A field of a record-like structure. *) diff --git a/asllib/ASTUtils.ml b/asllib/ASTUtils.ml index efc7df1f7..d4fc3f6c5 100644 --- a/asllib/ASTUtils.ml +++ b/asllib/ASTUtils.ml @@ -203,7 +203,8 @@ and use_ty acc t = | T_Int (WellConstrained cs) -> use_constraints acc cs | T_Tuple li -> List.fold_left use_ty acc li | T_Record fields | T_Exception fields -> fold_named_list use_ty acc fields - | T_Array (e, t') -> use_ty (use_e acc e) t' + | T_Array (ArrayLength_Expr e, t') -> use_ty (use_e acc e) t' + | T_Array (ArrayLength_Enum (s, _), t') -> use_ty (ISet.add s acc) t' | T_Bits (e, bit_fields) -> use_bitfields (use_e acc e) bit_fields and use_bitfields acc bitfields = List.fold_left use_bitfield acc bitfields @@ -381,6 +382,14 @@ and constraint_equal eq c1 c2 = and constraints_equal eq cs1 cs2 = cs1 == cs2 || list_equal (constraint_equal eq) cs1 cs2 +and array_length_equal eq l1 l2 = + match (l1, l2) with + | ArrayLength_Expr e1, ArrayLength_Expr e2 -> expr_equal eq e1 e2 + | ArrayLength_Enum (s1, _), ArrayLength_Enum (s2, _) -> String.equal s1 s2 + | ArrayLength_Enum (_, _), ArrayLength_Expr _ + | ArrayLength_Expr _, ArrayLength_Enum (_, _) -> + false + and type_equal eq t1 t2 = t1.desc == t2.desc || @@ -397,7 +406,7 @@ and type_equal eq t1 t2 = | T_Bits (w1, bf1), T_Bits (w2, bf2) -> bitwidth_equal eq w1 w2 && bitfields_equal eq bf1 bf2 | T_Array (l1, t1), T_Array (l2, t2) -> - expr_equal eq l1 l2 && type_equal eq t1 t2 + array_length_equal eq l1 l2 && type_equal eq t1 t2 | T_Named s1, T_Named s2 -> String.equal s1 s2 | T_Enum li1, T_Enum li2 -> (* TODO: order of fields? *) list_equal String.equal li1 li2 diff --git a/asllib/Interpreter.ml b/asllib/Interpreter.ml index 56620b515..1d37545de 100644 --- a/asllib/Interpreter.ml +++ b/asllib/Interpreter.ml @@ -594,23 +594,26 @@ module Make (B : Backend.S) (C : Config) = struct let* v' = B.get_index i v in let* here = in_values v' ty' in and' prev here - and i = i + 1 in - (i, m) + in + (i + 1, m) in List.fold_left fold (0, m_true) tys |> snd - | T_Array (e, ty') -> - let* v = eval_expr_sef env e in - let n = - match B.v_to_int v with - | Some i -> i - | None -> fatal_from loc @@ Error.UnsupportedExpr e + | T_Array (index, ty') -> + let* length = + match index with + | ArrayLength_Enum (_, i) -> return i + | ArrayLength_Expr e -> ( + let* v_length = eval_expr_sef env e in + match B.v_to_int v_length with + | Some i -> return i + | None -> fatal_from loc @@ Error.UnsupportedExpr e) in let rec loop i prev = - if i = n then prev + if i >= length then prev else let* v' = B.get_index i v in let* here = in_values v' ty' in - loop (succ i) (and' prev here) + loop (i + 1) (and' prev here) in loop 0 m_true | T_Named _ -> assert false @@ -1340,21 +1343,18 @@ module Make (B : Backend.S) (C : Config) = struct (Error.NotYetImplemented "Base value of string types.") | T_Tuple li -> List.map (base_value env) li |> sync_list >>= B.create_vector - | T_Array (e_length, ty) -> + | T_Array (length, ty) -> let* v = base_value env ty in - let* length = - match e_length.desc with - | E_Var x when IMap.mem x env.global.static.declared_types -> - IMap.find x env.global.static.constants_values - |> B.v_of_literal |> return - | _ -> eval_expr_sef env e_length + let* i_length = + match length with + | ArrayLength_Enum (_, i) -> return i + | ArrayLength_Expr e -> ( + let* length = eval_expr_sef env e in + match B.v_to_int length with + | None -> Error.fatal_from t (Error.UnsupportedExpr e) + | Some i -> return i) in - let length = - match B.v_to_int length with - | None -> Error.fatal_from t (Error.UnsupportedExpr e_length) - | Some i -> i - in - List.init length (Fun.const v) |> B.create_vector + List.init i_length (Fun.const v) |> B.create_vector (* Begin TopLevel *) let run_typed_env env (ast : AST.t) (static_env : StaticEnv.env) : B.value m = diff --git a/asllib/PP.ml b/asllib/PP.ml index 7a41060b9..b67a9da4a 100644 --- a/asllib/PP.ml +++ b/asllib/PP.ml @@ -174,8 +174,10 @@ and pp_ty f t = (pp_comma_list pp_print_string) enum_ty | T_Tuple ty_list -> fprintf f "@[(%a)@]" (pp_comma_list pp_ty) ty_list - | T_Array (e, elt_type) -> + | T_Array (ArrayLength_Expr e, elt_type) -> fprintf f "@[array [%a] of %a@]" pp_expr e pp_ty elt_type + | T_Array (ArrayLength_Enum (s, _), elt_type) -> + fprintf f "@[array [%s] of %a@]" s pp_ty elt_type | T_Record record_ty -> fprintf f "@[record {@ %a@;<1 -2>}@]" pp_fields record_ty | T_Exception record_ty -> diff --git a/asllib/Parser.mly b/asllib/Parser.mly index 173e0b916..f7be9084d 100644 --- a/asllib/Parser.mly +++ b/asllib/Parser.mly @@ -376,12 +376,16 @@ let ty := | STRING; { T_String } | BIT; { t_bit } | BITS; ~=pared(expr); ~=bitfields_opt; < T_Bits > - | ENUMERATION; l=braced(tclist(IDENTIFIER)); < T_Enum > | l=plist(ty); < T_Tuple > - | ARRAY; e=bracketed(expr); OF; t=ty; < T_Array > + | name=IDENTIFIER; < T_Named > + | ARRAY; e=bracketed(expr); OF; t=ty; { T_Array (ArrayLength_Expr e, t) } + ) + +let ty_decl := ty | + annotated ( + | ENUMERATION; l=braced(tclist(IDENTIFIER)); < T_Enum > | RECORD; l=fields_opt; < T_Record > | EXCEPTION; l=fields_opt; < T_Exception > - | name=IDENTIFIER; < T_Named > ) (* Constructs on ty *) @@ -568,8 +572,8 @@ let decl == } | terminated_by(SEMI_COLON, - | TYPE; x=IDENTIFIER; OF; t=ty; ~=subtype_opt; < D_TypeDecl > - | TYPE; x=IDENTIFIER; s=annotated(subtype); < make_ty_decl_subtype > + | TYPE; x=IDENTIFIER; OF; t=ty_decl; ~=subtype_opt; < D_TypeDecl > + | TYPE; x=IDENTIFIER; s=annotated(subtype); < make_ty_decl_subtype > | keyword=storage_keyword; name=ignored_or_identifier; ty=ioption(as_ty); EQ; initial_value=some(expr); diff --git a/asllib/Serialize.ml b/asllib/Serialize.ml index 107c79a47..6f2829592 100644 --- a/asllib/Serialize.ml +++ b/asllib/Serialize.ml @@ -170,8 +170,8 @@ and pp_ty = | T_Tuple li -> addb f "T_Tuple "; pp_list pp_ty f li - | T_Array (e, elt_type) -> - bprintf f "T_Array (%a, %a)" pp_expr e pp_ty elt_type + | T_Array (length, elt_type) -> + bprintf f "T_Array (%a, %a)" pp_array_length length pp_ty elt_type | T_Record li -> addb f "T_Record "; pp_id_assoc pp_ty f li @@ -182,6 +182,10 @@ and pp_ty = in fun f s -> pp_annotated pp_desc f s +and pp_array_length f = function + | ArrayLength_Expr e -> bprintf f "ArrayLength_Expr (%a)" pp_expr e + | ArrayLength_Enum (s, i) -> bprintf f "ArrayLength_Enum (%S, %i)" s i + and pp_bitfield f = function | BitField_Simple (name, slices) -> bprintf f "BitField_Simple (%S, %a)" name pp_slice_list slices diff --git a/asllib/StaticEnv.ml b/asllib/StaticEnv.ml index b5224977d..03dc26c4c 100644 --- a/asllib/StaticEnv.ml +++ b/asllib/StaticEnv.ml @@ -174,6 +174,9 @@ let add_global_storage x ty gdk env = } let add_type x ty env = + let () = + if false then Format.eprintf "Adding type %s as %a.@." x PP.pp_ty ty + in { env with global = diff --git a/asllib/StaticInterpreter.ml b/asllib/StaticInterpreter.ml index bcd3c3c3b..66200f5f6 100644 --- a/asllib/StaticInterpreter.ml +++ b/asllib/StaticInterpreter.ml @@ -390,6 +390,13 @@ module Normalize = struct | StrictPositive -> Negative | StrictNegative -> Positive + let sign_minus = function + | (NotNull | Null) as s -> s + | Positive -> Negative + | Negative -> Positive + | StrictPositive -> StrictNegative + | StrictNegative -> StrictPositive + exception ConjunctionBottomInterrupt let sign_and _p s1 s2 = @@ -644,24 +651,51 @@ module Normalize = struct if e1 == e_true then e2 else if e2 == e_true then e1 else binop BAND e1 e2 let e_cond e1 e2 e3 = E_Cond (e1, e2, e3) |> add_pos_from loc + let unop op e = E_Unop (op, e) |> add_pos_from loc let monomial_to_expr (Prod map) = let ( ** ) e1 e2 = - if e1 = one then e2 else if e2 = one then e1 else binop MUL e1 e2 + if e1 == one then e2 else if e2 == one then e1 else binop MUL e1 e2 in let ( ^^ ) e = function | 0 -> one | 1 -> e | 2 -> e ** e - | p -> if e = one then one else binop POW e (expr_of_int p) + | p -> binop POW e (expr_of_int p) in AMap.fold (fun s p e -> (e_var s ^^ p) ** e) map + let sign_of_z c = + match Z.sign c with + | 1 -> StrictPositive + | 0 -> Null + | -1 -> StrictNegative + | _ -> assert false + let polynomial_to_expr (Sum map) = - let ( ++ ) e1 e2 = - if e1 == zero then e2 else if e2 == zero then e1 else binop PLUS e1 e2 + let add s1 e1 s2 e2 = + match (s1, s2) with + | _, Null -> e1 + | Null, _ -> e2 + | StrictPositive, StrictPositive | StrictNegative, StrictNegative -> + binop PLUS e1 e2 + | StrictPositive, StrictNegative | StrictNegative, StrictPositive -> + binop MINUS e1 e2 + | _ -> assert false + in + let res, sign = + MMap.fold + (fun m c (e, sign) -> + let c' = Z.abs c and sign' = sign_of_z c in + let m' = monomial_to_expr m (expr_of_z c') in + (add sign' m' sign e, sign')) + map (zero, Null) in - MMap.fold (fun m c e -> monomial_to_expr m (expr_of_z c) ++ e) map zero + match sign with + | Null -> zero + | StrictPositive -> res + | StrictNegative -> unop NEG res + | _ -> assert false let sign_to_binop = function | Null -> EQ_OP diff --git a/asllib/Typing.ml b/asllib/Typing.ml index 7723aced9..765f2d54d 100644 --- a/asllib/Typing.ml +++ b/asllib/Typing.ml @@ -155,9 +155,21 @@ 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 get_first_duplicate extractor li = + let exception Duplicate of identifier in + let folder acc elt = + let x = extractor elt in + let acc' = ISet.add x acc in + if acc' == acc then raise (Duplicate x) else acc' + in + try + let _ = List.fold_left folder ISet.empty li in + None + with Duplicate x -> Some x + (* --------------------------------------------------------------------------- - Main type-checking module + Properties handling ---------------------------------------------------------------------------*) @@ -167,195 +179,200 @@ 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 + type prop = (unit, unit) property + let strictness_string = match C.check with | `TypeCheck -> "type-checking-strict" | `Warn -> "type-checking-warn" | `Silence -> "type-inference" - let check = + let check : prop -> prop = match C.check with - | `TypeCheck -> fun f x -> f x + | `TypeCheck -> fun f () -> f () | `Warn -> ( - fun f x -> - try f x - with Error.ASLException e -> - Error.eprintln e; - x) - | `Silence -> fun _f x -> x + fun f () -> try f () with Error.ASLException e -> Error.eprintln e) + | `Silence -> fun _f () -> () - let best_effort = + 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 f1 f2 x = - let _ = f1 x in - f2 x + let[@inline] both (p1 : prop) (p2 : prop) () = + let () = p1 () in + let () = p2 () in + () - let either f1 f2 x = - try f1 x with TypingAssumptionFailed | Error.ASLException _ -> f2 x + let either (p1 : ('a, 'b) property) (p2 : ('a, 'b) property) x = + try p1 x with TypingAssumptionFailed | Error.ASLException _ -> p2 x - let rec any li x = + let rec any (li : prop list) : prop = match li with | [] -> raise (Invalid_argument "any") - | [ f ] -> f x - | f :: li -> either f (any li) x + | [ f ] -> f + | p :: li -> either p (any li) let assumption_failed () = raise_notrace TypingAssumptionFailed [@@inline] + let ok () = () [@@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 (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') - 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 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 - "Function %s@[(%a)@] is declared multiple times.@." name - Format.( - pp_print_list - ~pp_sep:(fun f () -> fprintf f ",@ ") - PP.pp_typed_identifier) - arg_types + Format.eprintf "Found already translated name: %S.@." name 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 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', + 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 - (* ------------------------------------------------------------------------- +(* --------------------------------------------------------------------------- - Handling of Getters and Setters + Main type-checking module - -------------------------------------------------------------------------- *) + ---------------------------------------------------------------------------*) + +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 @@ -534,8 +551,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 () = @@ -546,10 +562,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 @@ -576,6 +588,13 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let constraint_binop env op cs1 cs2 = constraint_binop op cs1 cs2 |> reduce_constraints env + let type_of_array_length ~loc env = function + | ArrayLength_Enum (s, _) -> T_Named s |> add_pos_from loc + | ArrayLength_Expr e -> + let m = binop MINUS e !$1 |> reduce_expr env in + let c = Constraint_Range (!$0, m) in + T_Int (WellConstrained [ c ]) |> add_pos_from loc + (* Begin CheckBinop *) let check_binop loc env op t1 t2 : ty = let () = @@ -588,8 +607,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 @@ -605,7 +624,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 @@ -614,15 +633,12 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let+ () = any [ - (* Optimisation. *) - check_true' - (type_equal (StaticInterpreter.equal_in_env env) t1 t2); (* 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. *) @@ -630,8 +646,11 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* 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); + both + (check_type_satisfies' env t1 real) + (check_type_satisfies' env t2 real); (fun () -> match (t1.desc, t2.desc) with | T_Enum li1, T_Enum li2 -> @@ -644,11 +663,11 @@ 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 -> ( @@ -674,7 +693,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 *) @@ -710,13 +729,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 struct1 = Types.get_well_constrained_structure env t1 in match struct1.desc with @@ -738,17 +757,193 @@ module Annotate (C : ANNOTATE_CONFIG) = struct t1 |: TypingRule.CheckUnop (* End *) - let rec annotate_slices env = + let check_var_not_in_env ?(local = true) loc env x () = + if + (local && IMap.mem x env.local.storage_types) + || IMap.mem x env.global.storage_types + || IMap.mem x env.global.subprograms + || IMap.mem x env.global.declared_types + then fatal_from loc (Error.AlreadyDeclaredIdentifier x) + else () + + let check_var_not_in_genv loc = check_var_not_in_env ~local:false loc + + let get_variable_enum' env e = + match e.desc with + | E_Var x -> ( + match IMap.find_opt x env.global.declared_types with + | Some t -> ( + match (Types.make_anonymous env t).desc with + | T_Enum li -> Some (x, List.length li) + | _ -> None) + | None -> None) + | _ -> None + + let check_diet_in_width loc slices width diet () = + let x = Diet.Int.min_elt diet |> Diet.Int.Interval.x + and y = Diet.Int.max_elt diet |> Diet.Int.Interval.y in + if 0 <= x && y < width then () + else fatal_from loc (BadSlices (slices, width)) + + let check_slices_in_width loc env width slices () = + let diet = disjoint_slices_to_diet loc env slices in + check_diet_in_width loc slices width diet () + + (* Begin TBitField *) + let rec annotate_bitfield ~loc env width bitfield : bitfield = + match bitfield with + | BitField_Simple (name, slices) -> + let slices = annotate_slices env slices in + let+ () = check_slices_in_width loc env width slices in + BitField_Simple (name, slices) + | BitField_Nested (name, slices, bitfields') -> + let slices = annotate_slices env slices in + let diet = disjoint_slices_to_diet loc env slices in + let+ () = check_diet_in_width loc slices width diet in + let width' = Diet.Int.cardinal diet |> expr_of_int in + let bitfields'' = annotate_bitfields ~loc env width' bitfields' in + BitField_Nested (name, slices, bitfields'') + | BitField_Type (name, slices, ty) -> + let ty' = annotate_type ~loc env ty in + let slices = annotate_slices env slices in + let diet = disjoint_slices_to_diet loc env slices in + let+ () = check_diet_in_width loc slices width diet in + let width' = Diet.Int.cardinal diet |> expr_of_int in + let+ () = + t_bits_bitwidth width' |> add_dummy_pos + |> check_bits_equal_width loc env ty + in + BitField_Type (name, slices, ty') + (* End *) + + and annotate_bitfields ~loc env e_width bitfields = + let+ () = + match get_first_duplicate bitfield_get_name bitfields with + | None -> ok + | Some x -> fun () -> fatal_from loc (Error.AlreadyDeclaredIdentifier x) + in + let width = + let v = reduce_constants env e_width in + match v with L_Int i -> Z.to_int i | _ -> assert false + in + List.map (annotate_bitfield ~loc env width) bitfields + + and annotate_type ?(decl = false) ~(loc : 'a annotated) env ty : ty = + let () = + if false then + Format.eprintf "Annotating@ %a@ in env:@ %a@." PP.pp_ty ty + StaticEnv.pp_env env + in + let here t = add_pos_from ty t in + match ty.desc with + (* Begin TString *) + | T_String -> ty + (* Begin TReal *) + | T_Real -> ty + (* Begin TBool *) + | T_Bool -> ty + (* Begin TNamed *) + | T_Named x -> + let+ () = + if IMap.mem x env.global.declared_types then ok + else fun () -> undefined_identifier loc x + in + ty + (* Begin TInt *) + | T_Int constraints -> ( + match constraints with + | WellConstrained constraints -> + let constraints = + List.map (annotate_constraint ~loc env) constraints + in + T_Int (WellConstrained constraints) |> here + | UnderConstrained _ | UnConstrained -> ty) + (* Begin TBits *) + | T_Bits (e_width, bitfields) -> + let e_width' = annotate_static_integer ~loc env e_width in + let bitfields' = + if bitfields = [] then bitfields + else annotate_bitfields ~loc env e_width' bitfields + in + T_Bits (e_width', bitfields') |> here + (* Begin TTuple *) + | T_Tuple tys -> + let tys' = List.map (annotate_type ~loc env) tys in + T_Tuple tys' |> here + (* Begin TArray *) + | T_Array (index, t) -> + let t' = annotate_type ~loc env t + and index' = + match index with + | ArrayLength_Expr e -> ( + match get_variable_enum' env e with + | Some (s, i) -> ArrayLength_Enum (s, i) + | None -> + let e' = annotate_static_integer ~loc env e in + ArrayLength_Expr e') + | ArrayLength_Enum (s, i) -> ( + let ty = T_Named s |> here in + match (Types.make_anonymous env ty).desc with + | T_Enum li when List.length li = i -> index + | _ -> conflict loc [ T_Enum [] ] ty) + in + T_Array (index', t') |> here + (* Begin TRecordExceptionDecl *) + | (T_Record fields | T_Exception fields) when decl -> ( + let+ () = + match get_first_duplicate fst fields with + | None -> ok + | Some x -> + fun () -> fatal_from loc (Error.AlreadyDeclaredIdentifier x) + in + let fields' = + List.map (fun (x, ty) -> (x, annotate_type ~loc env ty)) fields + in + match ty.desc with + | T_Record _ -> T_Record fields' |> here + | T_Exception _ -> T_Exception fields' |> here + | _ -> assert false + (* Begin TEnumDecl *)) + | T_Enum li when decl -> + let+ () = + match get_first_duplicate Fun.id li with + | None -> ok + | Some x -> + fun () -> fatal_from loc (Error.AlreadyDeclaredIdentifier x) + in + let+ () = + fun () -> List.iter (fun s -> check_var_not_in_genv ty env s ()) li + in + ty + (* Begin TNonDecl *) + | T_Enum _ | T_Record _ | T_Exception _ -> + if decl then assert false + else + fatal_from loc + (Error.NotYetImplemented + " Cannot use non anonymous form of enumerations, record, or \ + exception here.") + (* End *) + + and annotate_static_integer ~(loc : 'a annotated) env e = + let t, e' = annotate_expr env e in + let+ () = check_structure_integer loc env t in + let+ () = check_statically_evaluable env e' in + reduce_expr env e' + + and annotate_constraint ~loc env = function + | Constraint_Exact e -> + let e' = annotate_static_integer ~loc env e in + Constraint_Exact e' + | Constraint_Range (e1, e2) -> + let e1' = annotate_static_integer ~loc env e1 + and e2' = annotate_static_integer ~loc env e2 in + Constraint_Range (e1', e2') + + and annotate_slices env = (* 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 s = let () = @@ -766,12 +961,10 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Begin SliceLength *) | Slice_Length (offset, length) -> let t_offset, offset' = annotate_expr env offset - and t_length, length' = annotate_expr env length in + and length' = + annotate_static_integer ~loc:(to_pos length) env length + in 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 *) @@ -815,8 +1008,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 @@ -835,9 +1027,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 *) @@ -857,11 +1052,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+ () = - both (* TODO: case where they are both real *) - (check_structure_integer loc env t) - (both - (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 *) @@ -902,7 +1101,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 @@ -984,14 +1183,14 @@ module Annotate (C : ANNOTATE_CONFIG) = struct and annotate_expr env (e : expr) : ty * expr = let () = if false then Format.eprintf "@[Annotating %a@]@." PP.pp_expr e in - let here x = add_pos_from e x in + let here x = add_pos_from e x and loc = to_pos e in match e.desc with (* Begin ELit *) | E_Literal v -> (annotate_literal v |> here, e) |: TypingRule.ELit (* End *) (* Begin CTC *) - | E_CTC (e', t') -> - let t'', e'' = annotate_expr env e' in + | E_CTC (e', ty) -> + let t, e'' = annotate_expr env e' in (* - If type-checking determines that the expression type-satisfies the required type, then no further check is required. @@ -1001,18 +1200,18 @@ module Annotate (C : ANNOTATE_CONFIG) = struct an execution-time check that the expression evaluates to a value in the domain of the required type is required. *) + let ty' = annotate_type ~loc env ty in best_effort - (t', E_CTC (e'', t') |> here) + (ty', E_CTC (e'', ty') |> here) (fun res -> - let env' = env in - if Types.structural_subtype_satisfies env' t'' t' then - if Types.domain_subtype_satisfies env' t'' t' then + if Types.structural_subtype_satisfies env t ty' then + if Types.domain_subtype_satisfies env t ty' then (* disabling the optimization here as long as the type system is not sound. *) (* (t', e'') *) res else res - else conflict e [ t'.desc ] t'') + else conflict e [ ty'.desc ] t) |: TypingRule.CTC (* End *) | E_Var x -> ( @@ -1184,8 +1383,9 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* End *) (* Begin EUnknown *) | E_Unknown ty -> - let ty' = Types.get_structure env ty in - (ty, E_Unknown ty' |> here) |: TypingRule.EUnknown + let ty1 = annotate_type ~loc env ty in + let ty2 = Types.get_structure env ty1 in + (ty1, E_Unknown ty2 |> here) |: TypingRule.EUnknown (* End *) | E_Slice (e', slices) -> ( let reduced = @@ -1219,23 +1419,10 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* End *) (* Begin EGetArray *) | T_Array (size, ty') -> ( - let wanted_t_index = - let t_int = - T_Int - (WellConstrained - [ Constraint_Range (!$0, binop MINUS size !$1) ]) - |> here - in - match size.desc with - | 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 - in match slices with | [ Slice_Single e_index ] -> let t_index', e_index' = annotate_expr env e_index in + let wanted_t_index = type_of_array_length ~loc:e env size in let+ () = check_type_satisfies e env t_index' wanted_t_index in @@ -1441,23 +1628,10 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | T_Array (size, t) -> ( let le2 = annotate_lexpr env le1 t_le1 in let+ () = check_type_satisfies le2 env t_e t in - let wanted_t_index = - let t_int = - T_Int - (WellConstrained - [ Constraint_Range (!$0, binop MINUS size !$1) ]) - |> here - in - match size.desc with - | E_Var name -> ( - match IMap.find_opt name env.global.declared_types with - | Some t -> t - | None -> t_int) - | _ -> t_int - in match slices with | [ Slice_Single e_index ] -> let t_index', e_index' = annotate_expr env e_index in + let wanted_t_index = type_of_array_length ~loc:le env size in let+ () = check_type_satisfies le2 env t_index' wanted_t_index in @@ -1585,14 +1759,6 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let check_can_be_initialized_with loc env s t () = if can_be_initialized_with env s t then () else conflict loc [ s.desc ] t - let check_var_not_in_env loc env x () = - if - IMap.mem x env.local.storage_types - || IMap.mem x env.global.storage_types - || IMap.mem x env.global.subprograms - then fatal_from loc (Error.AlreadyDeclaredIdentifier x) - else () - let rec annotate_local_decl_item loc (env : env) ty ldk ldi = match ldi with (* Begin LDDiscard *) @@ -1600,10 +1766,10 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* End *) (* Begin LDTyped *) | LDI_Typed (ldi', t) -> - (* check is t is valid *) - let+ () = check_can_be_initialized_with loc env t ty in - let new_env, new_ldi' = annotate_local_decl_item loc env t ldk ldi' in - (new_env, LDI_Typed (new_ldi', t)) |: TypingRule.LDTyped + let t' = annotate_type ~loc env t in + let+ () = check_can_be_initialized_with loc env t' ty in + let new_env, new_ldi' = annotate_local_decl_item loc env t' ldk ldi' in + (new_env, LDI_Typed (new_ldi', t')) |: TypingRule.LDTyped (* End *) (* Begin LDVar *) | LDI_Var x -> @@ -1643,11 +1809,11 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | LDI_Tuple _ldis -> fatal_from loc (Error.BadLDI ldi) |: TypingRule.LDUninitialisedTuple | LDI_Typed (ldi', t) -> - (* TODO check that t is valid *) + let t' = annotate_type ~loc env t in let new_env, new_ldi' = - annotate_local_decl_item loc env t LDK_Var ldi' + annotate_local_decl_item loc env t' LDK_Var ldi' in - (new_env, LDI_Typed (new_ldi', t)) |: TypingRule.LDUninitialisedTyped + (new_env, LDI_Typed (new_ldi', t')) |: TypingRule.LDUninitialisedTyped let declare_local_constant loc env t_e v ldi = let rec add_constants env ldi = @@ -1667,7 +1833,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | S_Seq _ -> () | _ -> Format.eprintf "@[<3>Annotating@ @[%a@]@]@." PP.pp_stmt s in - let here x = add_pos_from s x in + let here x = add_pos_from s x and loc = to_pos s in match s.desc with (* Begin SPass *) | S_Pass -> (s, env) |: TypingRule.SPass @@ -1720,7 +1886,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct in let ldk = LDK_Var in let env2, _ldi = - annotate_local_decl_item s env t_e ldk ldi + annotate_local_decl_item loc env t_e ldk ldi in env2 else env) @@ -1732,10 +1898,9 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Begin SCall *) | S_Call (name, args, eqs) -> let new_name, new_args, new_eqs, ty = - annotate_call (to_pos s) env name args eqs ST_Procedure + annotate_call loc 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 -> @@ -1747,7 +1912,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (match (env.local.return_type, e_opt) with (* Begin SReturnOne *) | None, Some _ | Some _, None -> - fatal_from s (Error.BadReturnStmt env.local.return_type) + fatal_from loc (Error.BadReturnStmt env.local.return_type) |: TypingRule.SReturnOne (* End *) (* Begin SReturnNone *) @@ -1769,7 +1934,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 @@ -1789,13 +1954,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 *) @@ -1803,7 +1968,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 *) @@ -1852,14 +2017,14 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let env', ldi' = if ldk = LDK_Constant then let v = reduce_constants env e in - declare_local_constant s env t_e v ldi - else annotate_local_decl_item s env t_e ldk ldi + declare_local_constant loc env t_e v ldi + else annotate_local_decl_item loc env t_e ldk ldi in (S_Decl (ldk, ldi', Some e') |> here, env') |: TypingRule.SDeclSome (* End *) (* Begin SDeclNone *) | LDK_Var, None -> - let env', ldi' = annotate_local_decl_item_uninit s env ldi in + let env', ldi' = annotate_local_decl_item_uninit loc env ldi in (S_Decl (LDK_Var, ldi', None) |> here, env') |: TypingRule.SDeclNone | (LDK_Constant | LDK_Let), None -> fatal_from s UnrespectedParserInvariant) @@ -1879,15 +2044,16 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | S_Try (s', catchers, otherwise) -> let s'' = try_annotate_block env s' in let otherwise' = Option.map (try_annotate_block env) otherwise in - let catchers' = List.map (annotate_catcher env) catchers in + let catchers' = List.map (annotate_catcher loc env) catchers in (S_Try (s'', catchers', otherwise') |> here, env) |: TypingRule.STry (* End *) | S_Print { args; debug } -> let args' = List.map (fun e -> annotate_expr env e |> snd) args in (S_Print { args = args'; debug } |> here, env) |: TypingRule.SDebug - and annotate_catcher env (name_opt, ty, stmt) = - let+ () = check_structure_exception ty env ty in + and annotate_catcher loc env (name_opt, ty, stmt) = + let ty' = annotate_type ~loc env ty in + let+ () = check_structure_exception ty' env ty' in let env' = match name_opt with (* Begin CatcherNone *) @@ -1928,7 +2094,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct else let ( let* ) = Option.bind in let _, _, _, ty_opt = - try FunctionRenaming.try_find_name le env x [] + try Fn.try_find_name le env x [] with Error.ASLException _ -> assert false in let* ty = ty_opt in @@ -1999,94 +2165,102 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | LE_Concat (_les, _) -> None | LE_SetArray _ -> assert false - (* Begin Subprogram *) - let annotate_subprogram loc (env : env) (f : AST.func) : AST.func = - let () = if false then Format.eprintf "Annotating %s.@." f.name in - (* Build typing local environment. *) - let env1 = { env with local = empty_local_return_type f.return_type } in - let env2 = - let one_arg env1 (x, ty) = - let+ () = check_var_not_in_env loc env1 x in - add_local x ty LDK_Let env1 - in - List.fold_left one_arg env1 f.args + let annotate_func_sig ~loc env (f : AST.func) : env * AST.func = + let () = + if false then + Format.eprintf "Annotating %s in env:@ %a.@." f.name StaticEnv.pp_env + env in + (* Build typing local environment. *) + let env1 = { env with local = empty_local } in (* Add explicit parameters *) - let env3 = - let one_param env2 (x, ty_opt) = + let env2, parameters = + let one_param env1' (x, ty_opt) = let ty = match ty_opt with - | Some ty -> ty + | Some ty -> annotate_type ~loc env1 ty | None -> Types.under_constrained_ty x in - let+ () = check_var_not_in_env loc env2 x in - add_local x ty LDK_Let env2 + let+ () = check_var_not_in_env loc env1' x in + (* Subtility here: the type should be valid in the env with nothing declared, i.e. [env1]. *) + (add_local x ty LDK_Let env1', (x, Some ty)) in - List.fold_left one_param env2 f.parameters + list_fold_left_map one_param env1 f.parameters in - (* Add dependently typed identifiers. *) - let add_dependently_typed_from_ty env'' ty = - match ty.desc with - | T_Bits ({ desc = E_Var x; _ }, _) -> ( - match StaticEnv.type_of_opt env x with - | Some { desc = T_Int UnConstrained; _ } -> - let ty = Types.under_constrained_ty x in - add_local x ty LDK_Let env'' - | Some _ -> env'' - | None -> - let ty = Types.under_constrained_ty x in - add_local x ty LDK_Let env'') - | _ -> env'' + let () = if false then Format.eprintf "Parameters added.@." in + (* Add dependently typed identifiers, from arguments. *) + let env3 = + let add_dependently_typed_from_ty env2' (_, ty) = + let () = + if false then Format.eprintf "Seeing arg of type %a@." PP.pp_ty ty + in + match ty.desc with + | T_Bits ({ desc = E_Var x; _ }, _) -> ( + match StaticEnv.type_of_opt env2' x with + | Some t -> + let () = + if false then + Format.eprintf "%S Already typed: %a@." x PP.pp_ty t + in + env2' + | None -> add_local x (Types.under_constrained_ty x) LDK_Let env2') + | _ -> env2' + in + List.fold_left add_dependently_typed_from_ty env2 f.args in - (* Resolve dependently typed identifiers in the arguments. *) - let env4 = - let one_arg env3 (_, ty) = add_dependently_typed_from_ty env3 ty in - List.fold_left one_arg env3 f.args + let () = + if false then + Format.eprintf "@[Annotating arguments in env:@ %a@]@." + StaticEnv.pp_env env3 in - (* Resolve dependently typed identifiers in the result type. *) - let env5 = env4 in - (* - let env5 = + (* Add arguments. *) + let env4, args = + let one_arg env3' (x, ty) = + let () = if false then Format.eprintf "Adding argument %s.@." x in + let+ () = check_var_not_in_env loc env3' x in + (* Subtility here: the type should be valid in the env with parameters declared, i.e. [env3]. *) + let ty' = annotate_type ~loc env3 ty in + let env3'' = add_local x ty' LDK_Let env3' in + (env3'', (x, ty')) + in + list_fold_left_map one_arg env3 f.args + in + let () = + if false then + Format.eprintf "@[Annotating return-type in env:@ %a@]@." + StaticEnv.pp_env env4 + in + (* Check return type. *) + let env5, return_type = match f.return_type with - | None -> env4 - | Some { desc = T_Bits ({ desc = E_Var x; _ }, _); _ } -> ( - match StaticEnv.type_of_opt env x with - | Some { desc = T_Int UnConstrained; _ } -> - let ty = new_under_constrained_integer x in - add_local x ty LDK_Let env4 - | _ -> env4) - | _ -> env4 + | None -> (env4, None) + | Some ty -> + (* Subtility here: the type should be valid in the env with arguments declared, i.e. [env4]. *) + let ty' = annotate_type ~loc env4 ty in + let return_type = Some ty' in + let env4' = + StaticEnv.{ env4 with local = { env4.local with return_type } } + in + (env4', Some ty') + in + (env5, { f with parameters; args; return_type }) + + (* Begin Subprogram *) + let annotate_subprogram (env : env) (f : AST.func) : AST.func = + let () = + if false then + Format.eprintf "@[Annotating body in env:@ %a@]@." StaticEnv.pp_env + env in - *) (* Annotate body *) let body = match f.body with SB_ASL body -> body | SB_Primitive -> assert false in - let new_body = try_annotate_block env5 body in - (* Optionnally rename the function if needs be *) - let name = - let args = List.map snd f.args in - let _, name, _, _ = FunctionRenaming.try_find_name loc env5 f.name args in - name - in - { f with body = SB_ASL new_body; name } |: TypingRule.Subprogram + let new_body = try_annotate_block env body in + { f with body = SB_ASL new_body } |: TypingRule.Subprogram (* End *) - let try_annotate_subprogram loc env f = - best_effort f (annotate_subprogram loc env) - - let annotate_gsd 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 - { 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_subprogram env f = best_effort f (annotate_subprogram env) (******************************************************************************) (* *) @@ -2098,7 +2272,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 () = @@ -2111,93 +2285,29 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (pp_print_list ~pp_sep:pp_print_space PP.pp_typed_identifier) func_sig.args in - add_subprogram name' func_sig env + let+ () = check_var_not_in_genv loc env name' in + let func_sig = { func_sig with name = name' } in + (add_subprogram name' func_sig env, func_sig) + + let annotate_and_declare_func ~loc func env = + let env, func = annotate_func_sig ~loc env func in + declare_one_func loc func env let add_global_storage loc name keyword env ty = - if IMap.mem name env.global.storage_types then - Error.fatal_from loc (Error.AlreadyDeclaredIdentifier name) - else if is_global_ignored name then env - else add_global_storage name ty keyword env + if is_global_ignored name then env + else + let+ () = check_var_not_in_genv loc env name in + add_global_storage name ty keyword env let declare_const loc name t v env = add_global_storage loc name GDK_Constant env t |> add_global_constant name v - let rec check_is_valid_bitfield loc env width bitfield () = - let slices = bitfield_get_slices bitfield in - let diet = disjoint_slices_to_diet loc env slices in - let+ () = - fun () -> - let x = Diet.Int.min_elt diet |> Diet.Int.Interval.x - and y = Diet.Int.max_elt diet |> Diet.Int.Interval.y in - if 0 <= x && y < width then () - else fatal_from loc (BadSlices (slices, width)) - in - match bitfield with - | BitField_Simple _ -> () - | BitField_Nested (_name, _slices, bitfields') -> - let width' = Diet.Int.cardinal diet in - check_is_valid_bitfields loc env width' bitfields' - | BitField_Type (_name, _slices, ty) -> - let+ () = check_is_valid_type loc env ty in - let+ () = - Diet.Int.cardinal diet |> expr_of_int |> t_bits_bitwidth - |> add_dummy_pos - |> check_bits_equal_width loc env ty - in - () - - and check_is_valid_bitfields loc env width bitfields = - let check_one declared_names bitfield = - let x = bitfield_get_name bitfield in - if ISet.mem x declared_names then - fatal_from loc (Error.AlreadyDeclaredIdentifier x) - else - let+ () = check_is_valid_bitfield loc env width bitfield in - ISet.add x declared_names - in - let _declared_names : ISet.t = - List.fold_left check_one ISet.empty bitfields - in - () - - and check_is_valid_type loc env ty () = - match ty.desc with - (* TODO: - - check integer constraints are compile-time constants - - check array-length are correctly defined - *) - | T_Record fields | T_Exception fields -> - let+ () = - fun () -> - let _ = - List.fold_left - (fun declared_names (x, ty) -> - if ISet.mem x declared_names then - fatal_from loc (Error.AlreadyDeclaredIdentifier x) - else - let+ () = check_is_valid_type loc env ty in - ISet.add x declared_names) - ISet.empty fields - in - () - in - () - | T_Bits (e_width, bitfields) -> - let width = - match reduce_constants env e_width with - | L_Int z -> Z.to_int z - | _ -> fatal_from loc (UnsupportedExpr e_width) - in - let+ () = fun () -> check_is_valid_bitfields loc env width bitfields in - () - | _ -> () - (* Begin DeclareType *) let declare_type loc name ty s env = let () = if false then Format.eprintf "Declaring type %s of %a@." name PP.pp_ty ty in - let+ () = check_var_not_in_env loc env name in + let+ () = check_var_not_in_genv loc env name in let env, ty = match s with | None -> (env, ty) @@ -2221,21 +2331,18 @@ module Annotate (C : ANNOTATE_CONFIG) = struct and env = add_subtype name s env in (env, ty) in - let+ () = check_is_valid_type loc env ty in + let ty' = annotate_type ~decl:true ~loc env ty in + let env = add_type name ty' env in let res = - match ty.desc with + match ty'.desc with | T_Enum ids -> - let env = add_type name ty env in let t = T_Named name |> add_pos_from ty in - let add_one_id (env, counter) x = - let v = L_Int (Z.of_int counter) in - (declare_const loc x t v env, counter + 1) + let declare_one (env, i) x = + (declare_const loc x t (L_Int (Z.of_int i)) env, succ i) in - let env, counter = List.fold_left add_one_id (env, 0) ids in - let l_counter = L_Int (Z.of_int counter) in - let env = declare_const loc name integer l_counter env in + let env, _ = List.fold_left declare_one (env, 0) ids in env - | _ -> add_type name ty env + | _ -> env in let () = if false then Format.eprintf "Declared %s.@." name in res @@ -2250,47 +2357,52 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Begin DeclareGlobalStorage *) let declare_global_storage loc gsd env = let () = if false then Format.eprintf "Declaring %s@." gsd.name in - best_effort env @@ fun _ -> + best_effort (gsd, env) @@ fun _ -> let { keyword; initial_value; ty; name } = gsd in - match (keyword, initial_value, ty) with - | GDK_Constant, Some e, Some ty -> - let t, e = annotate_expr env e in - (* let+ () = check_statically_evaluable env e in *) - let+ () = check_type_satisfies loc env t ty in - let env = try_add_global_constant name env e in - add_global_storage loc name keyword env ty - | GDK_Constant, Some e, None -> - let t, e = annotate_expr env e in - (* let+ () = check_statically_evaluable env e in *) - let env = try_add_global_constant name env e in - add_global_storage loc name keyword env t - | (GDK_Constant | GDK_Let), None, _ -> - (* Shouldn't happen because of parser construction. *) - Error.fatal_from loc - (Error.NotYetImplemented - "Constants or let-bindings must be initialized.") - | (GDK_Var | GDK_Config), None, Some ty -> - add_global_storage loc name keyword env ty - | _, Some e, Some ty -> - let t, _e = annotate_expr env e in - let+ () = check_type_satisfies loc env t ty in - add_global_storage loc name keyword env ty - | _, Some e, None -> - let t, _e = annotate_expr env e in - add_global_storage loc name keyword env t - | _, None, None -> - (* Shouldn't happen because of parser construction. *) - Error.fatal_from loc - (Error.NotYetImplemented - "Global storage declaration must have an initial value or a type.") + let+ () = check_var_not_in_genv loc env name in + let ty' = + match ty with Some ty -> Some (annotate_type ~loc env ty) | None -> ty + in + let typed_initial_value = + match initial_value with + | Some e -> Some (annotate_expr env e) + | None -> None + in + let declared_t = + match (typed_initial_value, ty') with + | Some (t, _), Some ty -> + let+ () = check_type_satisfies loc env t ty in + ty + | None, Some ty -> ty + | Some (t, _), None -> t + | None, None -> + (* Shouldn't happen because of parser construction. *) + Error.fatal_from loc + (Error.NotYetImplemented + "Global storage declaration must have an initial value or a \ + type.") + in + let env1 = add_global_storage loc name keyword env declared_t in + let env2 = + match (keyword, typed_initial_value) with + | GDK_Constant, Some (_t, e) -> try_add_global_constant name env1 e + | (GDK_Constant | GDK_Let), None -> + (* Shouldn't happen because of parser construction. *) + Error.fatal_from loc + (Error.NotYetImplemented + "Constants or let-bindings must be initialized.") + | _ -> env1 + in + let initial_value' = + match typed_initial_value with None -> None | Some (_t, e) -> Some e + in + ({ gsd with ty = ty'; initial_value = initial_value' }, env2) (* End *) let rename_primitive loc env (f : AST.func) = let name = best_effort f.name @@ fun _ -> - let _, name, _, _ = - FunctionRenaming.find_name loc env f.name (List.map snd f.args) - in + let _, name, _, _ = Fn.find_name loc env f.name (List.map snd f.args) in name in { f with name } @@ -2302,56 +2414,68 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (******************************************************************************) let type_check_decl d (acc, env) = - let here = ASTUtils.add_pos_from_st d in + let here = add_pos_from_st d and loc = to_pos d in let () = if false then Format.eprintf "@[Typing with %s in env:@ %a@]@." strictness_string StaticEnv.pp_env env + else if false then Format.eprintf "@[Typing %a.@]@." PP.pp_t [ d ] in match d.desc with | D_Func ({ body = SB_ASL _; _ } as f) -> - let env = declare_one_func d f env in - let d = D_Func (try_annotate_subprogram d env f) |> here in + let env, f = annotate_and_declare_func ~loc f env in + let d = D_Func (try_annotate_subprogram env f) |> here in (d :: acc, env) | D_Func ({ body = SB_Primitive; _ } as f) -> - let env = declare_one_func d f env in - let d = D_Func (rename_primitive d env f) |> here in + let env, f = annotate_and_declare_func ~loc f env in + let d = D_Func f |> here in (d :: acc, env) | D_GlobalStorage gsd -> - let d = D_GlobalStorage (try_annotate_gsd env gsd) |> here in - let env = declare_global_storage d gsd env in - (d :: acc, env) + let gsd', env' = declare_global_storage loc gsd env in + let d' = D_GlobalStorage gsd' |> here in + (d' :: acc, env') | D_TypeDecl (x, ty, s) -> - let env = declare_type d x ty s env in + let env = declare_type loc x ty s env in (d :: acc, env) let type_check_mutually_rec ds (acc, env) = - let env = - List.fold_left - (fun env d -> + let env_and_fs = + List.map + (fun d -> match d.desc with - | D_Func f -> declare_one_func d f env + | D_Func f -> + let loc = to_pos d in + let env', f = annotate_func_sig ~loc env f in + (env'.local, f, loc) | _ -> fatal_from d (Error.BadRecursiveDecls (List.map ASTUtils.identifier_of_decl ds))) - env ds + ds + in + let genv, fs = + list_fold_left_map + (fun genv (lenv, f, loc) -> + let env = { global = genv; local = lenv } in + let env', f = declare_one_func loc f env in + (env'.global, (env'.local, f, loc))) + env.global env_and_fs in let ds = List.map - (fun d -> - match d.desc with - | D_Func ({ body = SB_ASL _; name; _ } as f) -> + (fun (lenv, f, loc) -> + let here = add_pos_from loc in + let env' = { local = lenv; global = genv } in + match f.body with + | SB_ASL _ -> let () = - if false then Format.eprintf "@[Analysing decl %s.@]@." name + if false then Format.eprintf "@[Analysing decl %s.@]@." f.name in - D_Func (try_annotate_subprogram d env f) |> add_pos_from d - | D_Func ({ body = SB_Primitive; _ } as f) -> - D_Func (rename_primitive d env f) |> add_pos_from d - | _ -> assert false) - ds + D_Func (try_annotate_subprogram env' f) |> here + | SB_Primitive -> D_Func (rename_primitive loc env' f) |> here) + fs in - (List.rev_append ds acc, env) + (List.rev_append ds acc, { env with global = genv }) (* Begin Specification *) let type_check_ast = diff --git a/asllib/libdir/stdlib.asl b/asllib/libdir/stdlib.asl index 66882385c..4d6c0f2e9 100644 --- a/asllib/libdir/stdlib.asl +++ b/asllib/libdir/stdlib.asl @@ -157,7 +157,7 @@ begin return x == Ones(N); end -func SignExtend(x::bits(M), N::integer) => bits(N) +func SignExtend {M} (x::bits(M), N::integer) => bits(N) begin return [Replicate(x[M-1], N - M), x]; end diff --git a/asllib/tests/ASLSemanticsReference.t/run.t b/asllib/tests/ASLSemanticsReference.t/run.t index 21aee5b7c..9a93e0259 100644 --- a/asllib/tests/ASLSemanticsReference.t/run.t +++ b/asllib/tests/ASLSemanticsReference.t/run.t @@ -31,7 +31,7 @@ ASL Semantics Reference: $ aslref SemanticsRule.EGetArray.asl $ aslref SemanticsRule.EGetArrayTooSmall.asl File SemanticsRule.EGetArrayTooSmall.asl, line 7, characters 8 to 19: - ASL Typing error: a subtype of integer {0..(3 - 1)} was expected, + ASL Typing error: a subtype of integer {0..2} was expected, provided integer {3}. [1] $ aslref SemanticsRule.ERecord.asl diff --git a/asllib/tests/asl.t/enum-array.asl b/asllib/tests/asl.t/enum-array.asl new file mode 100644 index 000000000..8c52904cf --- /dev/null +++ b/asllib/tests/asl.t/enum-array.asl @@ -0,0 +1,20 @@ +type MyEnum of enumeration { A, B, C }; + +type MyArray of array [ MyEnum ] of integer; + +func main () => integer +begin + var my_array: MyArray; + print (my_array); + + my_array[A] = 1; + my_array[B] = 2; + my_array[C] = 3; + + assert (my_array[A] == 1); + assert (my_array[B] == 2); + assert (my_array[C] == 3); + + return 0; +end + diff --git a/asllib/tests/asl.t/run.t b/asllib/tests/asl.t/run.t index 7ed450f7a..060cb9fe8 100644 --- a/asllib/tests/asl.t/run.t +++ b/asllib/tests/asl.t/run.t @@ -36,7 +36,7 @@ Type-checking errors: Bad types: $ aslref overlapping-slices.asl File overlapping-slices.asl, line 1, character 0 to line 4, character 2: - ASL Typing error: overlapping slices 10:0, 3+:2. + ASL Typing error: overlapping slices 0+:11, 3+:2. [1] Global ignored: @@ -110,7 +110,7 @@ Constrained-type satisfaction: [1] $ cat >type-sat.asl < func invokeMe_2(N: integer, b: bits(N)) + > func invokeMe_2 {N} (b: bits(N)) > begin > // N is under-constrained integer > var x: integer { 2, 4} = N; @@ -189,3 +189,7 @@ UnderConstrained integers: $ aslref named-types-in-slices.asl File named-types-in-slices.asl, line 13, characters 2 to 11: x -> '11111111' + +Arrays indexed by enumerations + $ aslref enum-array.asl + [0, 0, 0] diff --git a/asllib/tests/bad-types.t b/asllib/tests/bad-types.t index 2284e0bbf..6a495e34d 100644 --- a/asllib/tests/bad-types.t +++ b/asllib/tests/bad-types.t @@ -25,7 +25,7 @@ Overlapping slices $ aslref bad-types.asl File bad-types.asl, line 1, character 0 to line 4, character 2: - ASL Typing error: overlapping slices 10:0, 3+:2. + ASL Typing error: overlapping slices 0+:11, 3+:2. [1] Bad slices @@ -38,7 +38,7 @@ Bad slices $ aslref bad-types.asl File bad-types.asl, line 1, character 0 to line 4, character 2: - ASL Typing error: Cannot extract from bitvector of length 12 slices 14:12. + ASL Typing error: Cannot extract from bitvector of length 12 slices 12+:3. [1] $ cat >bad-types.asl < - expr_equal env length_s length_t && type_equal env ty_s ty_t + | T_Array (length_s, ty_s), T_Array (length_t, ty_t) -> ( + type_equal env ty_s ty_t + && + match (length_s, length_t) with + | ArrayLength_Expr length_s, ArrayLength_Expr length_t -> + expr_equal env length_s length_t + | ArrayLength_Enum (name_s, _), ArrayLength_Enum (name_t, _) -> + String.equal name_s name_t + | ArrayLength_Enum (_, _), ArrayLength_Expr _ + | ArrayLength_Expr _, ArrayLength_Enum (_, _) -> + false) | T_Array _, _ -> false (* If S has the structure of a tuple type then T must have the structure of a tuple type with same number of elements as S, @@ -722,8 +731,7 @@ let rec lowest_common_ancestor env s t = let struct_s = get_structure env s and struct_t = get_structure env t in match (struct_s.desc, struct_t.desc) with - | T_Array (l_s, t_s), T_Array (l_t, t_t) - when type_equal env t_s t_t && expr_equal env l_s l_t -> ( + | T_Array _, T_Array _ when type_equal env struct_s struct_t -> ( (* If S and T both have the structure of array types with the same index type and the same element types: – If S is a named type and T is an anonymous type: S From d11e4a1d6dcc0dccb51586acdff42c53d9eb5479 Mon Sep 17 00:00:00 2001 From: Hadrien Renaud Date: Thu, 21 Mar 2024 15:08:19 +0000 Subject: [PATCH 2/5] [asl] Check bitvector width are constrained This implied an important rework on parameter handling. --- asllib/ASTUtils.ml | 39 ++++- asllib/StaticInterpreter.ml | 10 +- asllib/Typing.ml | 290 ++++++++++++++++++++++++------------ asllib/error.ml | 11 ++ asllib/libdir/stdlib.asl | 6 +- asllib/tests/asl.t/bug1.asl | 8 + asllib/tests/asl.t/bug2.asl | 8 + asllib/tests/asl.t/bug3.asl | 7 + asllib/tests/asl.t/run.t | 16 +- asllib/tests/asltests.ml | 5 +- asllib/types.ml | 6 +- 11 files changed, 294 insertions(+), 112 deletions(-) create mode 100644 asllib/tests/asl.t/bug1.asl create mode 100644 asllib/tests/asl.t/bug2.asl create mode 100644 asllib/tests/asl.t/bug3.asl diff --git a/asllib/ASTUtils.ml b/asllib/ASTUtils.ml index d4fc3f6c5..0e153b3b7 100644 --- a/asllib/ASTUtils.ml +++ b/asllib/ASTUtils.ml @@ -551,20 +551,45 @@ let list_cross f li1 li2 = exception FailedConstraintOp +let is_left_increasing = function + | MUL | DIV | DIVRM | MOD | SHL | SHR | POW | PLUS | MINUS -> true + | AND | BAND | BEQ | BOR | EOR | EQ_OP | GT | GEQ | IMPL | LT | LEQ | NEQ | OR + | RDIV -> + raise FailedConstraintOp + +let is_right_increasing = function + | MUL | SHL | SHR | POW | PLUS -> true + | DIV | DIVRM | MOD | MINUS -> false + | AND | BAND | BEQ | BOR | EOR | EQ_OP | GT | GEQ | IMPL | LT | LEQ | NEQ | OR + | RDIV -> + raise FailedConstraintOp + +let is_right_decreasing = function + | MINUS -> true + | DIV | DIVRM | MUL | SHL | SHR | POW | PLUS | MOD -> false + | AND | BAND | BEQ | BOR | EOR | EQ_OP | GT | GEQ | IMPL | LT | LEQ | NEQ | OR + | RDIV -> + raise FailedConstraintOp + let constraint_binop op = + let righ_inc = is_right_increasing op + and righ_dec = is_right_decreasing op + and left_inc = is_left_increasing op in let do_op c1 c2 = - match (c1, c2, op) with - | Constraint_Exact e1, Constraint_Exact e2, _ -> + match (c1, c2) with + | Constraint_Exact e1, Constraint_Exact e2 -> Constraint_Exact (binop op e1 e2) - | Constraint_Exact e1, Constraint_Range (e21, e22), PLUS -> + | Constraint_Exact e1, Constraint_Range (e21, e22) when righ_inc -> Constraint_Range (binop op e1 e21, binop op e1 e22) - | Constraint_Exact e1, Constraint_Range (e21, e22), MINUS -> + | Constraint_Exact e1, Constraint_Range (e21, e22) when righ_dec -> Constraint_Range (binop op e1 e22, binop op e1 e21) - | Constraint_Range (e11, e12), Constraint_Exact e2, (PLUS | MINUS) -> + | Constraint_Range (e11, e12), Constraint_Exact e2 when left_inc -> Constraint_Range (binop op e11 e2, binop op e12 e2) - | Constraint_Range (e11, e12), Constraint_Range (e21, e22), PLUS -> + | Constraint_Range (e11, e12), Constraint_Range (e21, e22) + when left_inc && righ_inc -> Constraint_Range (binop op e11 e21, binop op e12 e22) - | Constraint_Range (e11, e12), Constraint_Range (e21, e22), MINUS -> + | Constraint_Range (e11, e12), Constraint_Range (e21, e22) + when left_inc && righ_dec -> Constraint_Range (binop op e11 e22, binop op e12 e21) | _ -> raise_notrace FailedConstraintOp in diff --git a/asllib/StaticInterpreter.ml b/asllib/StaticInterpreter.ml index 66200f5f6..040598971 100644 --- a/asllib/StaticInterpreter.ml +++ b/asllib/StaticInterpreter.ml @@ -30,6 +30,7 @@ type env = SEnv.env let fatal = Error.fatal let fatal_from = Error.fatal_from +exception StaticEvaluationUnknown exception NotYetImplemented let value_as_int pos = function @@ -148,7 +149,9 @@ let rec static_eval (env : SEnv.env) : expr -> literal = Format.eprintf "Failed to lookup %S in env: %a@." x StaticEnv.pp_env env in - Error.fatal_from e (Error.UndefinedIdentifier x)) + if SEnv.is_undefined x env then + Error.fatal_from e (Error.UndefinedIdentifier x) + else raise StaticEvaluationUnknown) | E_Binop (op, e1, e2) -> let v1 = expr_ e1 and v2 = expr_ e2 in binop_values e op v1 v2 @@ -596,7 +599,10 @@ module Normalize = struct | _ -> ( let v = try static_eval env e - with Error.ASLException { desc = UnsupportedExpr _; _ } -> + with + | StaticEvaluationUnknown + | Error.ASLException { desc = UnsupportedExpr _; _ } + -> raise NotYetImplemented in match v with diff --git a/asllib/Typing.ml b/asllib/Typing.ml index 765f2d54d..15fcc88bb 100644 --- a/asllib/Typing.ml +++ b/asllib/Typing.ml @@ -29,6 +29,7 @@ module TypingRule = Instrumentation.TypingRule let ( |: ) = Instrumentation.TypingNoInstr.use_with let fatal_from = Error.fatal_from let undefined_identifier pos x = fatal_from pos (Error.UndefinedIdentifier x) +let unsupported_expr e = fatal_from e (Error.UnsupportedExpr e) let conflict pos expected provided = fatal_from pos (Error.ConflictingTypes (expected, provided)) @@ -38,15 +39,16 @@ let plus = binop PLUS let t_bits_bitwidth e = T_Bits (e, []) let reduce_expr env e = - try StaticInterpreter.Normalize.normalize env e - with StaticInterpreter.NotYetImplemented -> e + let open StaticInterpreter in + try Normalize.normalize env e with NotYetImplemented -> e let reduce_constants env e = - try StaticInterpreter.static_eval env e - with - | Error.ASLException - { desc = Error.UndefinedIdentifier x; pos_start; pos_end } as error - -> ( + let open StaticInterpreter in + let eval_expr env e = + try static_eval env e with NotYetImplemented -> unsupported_expr e + in + try eval_expr env e + with StaticEvaluationUnknown -> ( let () = if false then Format.eprintf @@ -54,13 +56,8 @@ let reduce_constants env e = %a@]@." PP.pp_expr e PP.pp_pos e in - try - StaticInterpreter.Normalize.normalize env e - |> StaticInterpreter.static_eval env - with StaticInterpreter.NotYetImplemented -> - if pos_end == Lexing.dummy_pos || pos_start == Lexing.dummy_pos then - undefined_identifier e x - else raise error) + try reduce_expr env e |> eval_expr env + with StaticEvaluationUnknown -> unsupported_expr e) let reduce_constraint env = function | Constraint_Exact e -> Constraint_Exact (reduce_expr env e) @@ -327,7 +324,8 @@ module FunctionRenaming (C : ANNOTATE_CONFIG) = struct ( deduce_eqs env caller_arg_types callee_arg_types, name, callee_arg_types, - func_sig.return_type ) + func_sig.return_type, + func_sig.parameters ) else fatal_from loc (Error.NoCallCandidate (name, caller_arg_types)) | None -> undefined_identifier loc name) | Some set -> ( @@ -338,14 +336,14 @@ module FunctionRenaming (C : ANNOTATE_CONFIG) = struct ( deduce_eqs env caller_arg_types callee_arg_types, name', callee_arg_types, - func_sig.return_type ) + func_sig.return_type, + func_sig.parameters ) :: acc else acc in match ISet.fold finder set [] with + | [ res ] -> res | [] -> 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))) @@ -356,11 +354,11 @@ module FunctionRenaming (C : ANNOTATE_CONFIG) = struct try match IMap.find_opt name env.global.subprograms with | None -> undefined_identifier loc ("function " ^ name) - | Some { args = callee_arg_types; return_type; _ } -> + | Some { args = callee_arg_types; return_type; parameters; _ } -> if false then Format.eprintf "@[<2>%a:@ No extra arguments for %s@]@." PP.pp_pos loc name; - ([], name, callee_arg_types, return_type) + ([], name, callee_arg_types, return_type, parameters) with Error.ASLException _ -> raise error) end @@ -390,7 +388,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let eval env e = match reduce_constants env e with | L_Int z -> Z.to_int z - | _ -> fatal_from e @@ Error.UnsupportedExpr e + | _ -> unsupported_expr e in let module DI = Diet.Int in let one_slice loc env diet slice = @@ -519,10 +517,16 @@ module Annotate (C : ANNOTATE_CONFIG) = struct if false then Format.eprintf "Checking that %a is an integer.@." PP.pp_ty t in - match (Types.get_structure env t).desc with + match (Types.make_anonymous env t).desc with | T_Int _ -> () | _ -> conflict loc [ integer' ] t + let check_constrained_integer ~loc env t () = + match (Types.make_anonymous env t).desc with + | T_Int UnConstrained -> fatal_from loc Error.(ConstrainedIntegerExpected t) + | T_Int (WellConstrained _ | UnderConstrained _) -> () + | _ -> conflict loc [ integer' ] t + let check_structure_exception loc env t () = let t_struct = Types.get_structure env t in match t_struct.desc with @@ -566,7 +570,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct match e.desc with | E_Literal (L_Int i) -> Z.sign i = 1 | E_Var _n -> false - | _ -> fatal_from e (UnsupportedExpr e) + | _ -> unsupported_expr e let constraint_is_strict_positive = function | Constraint_Exact e | Constraint_Range (e, _) -> expr_is_strict_positive e @@ -578,7 +582,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct match e.desc with | E_Literal (L_Int i) -> Z.sign i != -1 | E_Var _n -> false - | _ -> fatal_from e (UnsupportedExpr e) + | _ -> unsupported_expr e let constraint_is_non_negative = function | Constraint_Exact e | Constraint_Range (e, _) -> expr_is_non_negative e @@ -586,7 +590,16 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let constraints_is_non_negative = List.for_all constraint_is_non_negative let constraint_binop env op cs1 cs2 = - constraint_binop op cs1 cs2 |> reduce_constraints env + let res = constraint_binop op cs1 cs2 |> reduce_constraints env in + let () = + if false then + Format.eprintf + "Reduction of binop %s@ on@ constraints@ %a@ and@ %a@ gave@ %a@." + (PP.binop_to_string op) PP.pp_int_constraints cs1 + PP.pp_int_constraints cs2 PP.pp_ty + (T_Int res |> add_dummy_pos) + in + res let type_of_array_length ~loc env = function | ArrayLength_Enum (s, _) -> T_Named s |> add_pos_from loc @@ -757,13 +770,15 @@ module Annotate (C : ANNOTATE_CONFIG) = struct t1 |: TypingRule.CheckUnop (* End *) + let var_in_env ?(local = true) env x = + (local && IMap.mem x env.local.storage_types) + || IMap.mem x env.global.storage_types + || IMap.mem x env.global.subprograms + || IMap.mem x env.global.declared_types + let check_var_not_in_env ?(local = true) loc env x () = - if - (local && IMap.mem x env.local.storage_types) - || IMap.mem x env.global.storage_types - || IMap.mem x env.global.subprograms - || IMap.mem x env.global.declared_types - then fatal_from loc (Error.AlreadyDeclaredIdentifier x) + if var_in_env ~local env x then + fatal_from loc (Error.AlreadyDeclaredIdentifier x) else () let check_var_not_in_genv loc = check_var_not_in_env ~local:false loc @@ -835,6 +850,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct StaticEnv.pp_env env in let here t = add_pos_from ty t in + best_effort ty @@ fun _ -> match ty.desc with (* Begin TString *) | T_String -> ty @@ -860,7 +876,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | UnderConstrained _ | UnConstrained -> ty) (* Begin TBits *) | T_Bits (e_width, bitfields) -> - let e_width' = annotate_static_integer ~loc env e_width in + let e_width' = annotate_static_constrained_integer ~loc env e_width in let bitfields' = if bitfields = [] then bitfields else annotate_bitfields ~loc env e_width' bitfields @@ -931,13 +947,19 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let+ () = check_statically_evaluable env e' in reduce_expr env e' + and annotate_static_constrained_integer ~(loc : 'a annotated) env e = + let t, e' = annotate_expr env e in + let+ () = check_constrained_integer ~loc env t in + let+ () = check_statically_evaluable env e' in + reduce_expr env e' + and annotate_constraint ~loc env = function | Constraint_Exact e -> - let e' = annotate_static_integer ~loc env e in + let e' = annotate_static_constrained_integer ~loc env e in Constraint_Exact e' | Constraint_Range (e1, e2) -> - let e1' = annotate_static_integer ~loc env e1 - and e2' = annotate_static_integer ~loc env e2 in + let e1' = annotate_static_constrained_integer ~loc env e1 + and e2' = annotate_static_constrained_integer ~loc env e2 in Constraint_Range (e1', e2') and annotate_slices env = @@ -962,7 +984,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | Slice_Length (offset, length) -> let t_offset, offset' = annotate_expr env offset and length' = - annotate_static_integer ~loc:(to_pos length) env length + annotate_static_constrained_integer ~loc:(to_pos length) env length in let+ () = check_structure_integer offset' env t_offset in Slice_Length (offset', length') |: TypingRule.SliceLength @@ -1100,7 +1122,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct in 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 = + let extra_nargs, name1, callee_arg_types, ret_ty, callee_params = Fn.try_find_name loc env name caller_arg_types in let () = @@ -1126,9 +1148,8 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* End *) in let eqs2 = - let folder acc (x, ty) (t_e, e) = + let folder acc (_x, ty) (t_e, _e) = match ty.desc with - | T_Int _ -> (x, e) :: acc | T_Bits ({ desc = E_Var x; _ }, _) -> ( match (Types.get_structure env t_e).desc with | T_Bits (e, _) -> (x, e) :: acc @@ -1143,7 +1164,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct eprintf "@[Eqs for this call are: %a@]@." (pp_print_list ~pp_sep:pp_print_space (fun f (name, e) -> fprintf f "%S<--%a" name PP.pp_expr e)) - eqs + eqs2 in let () = List.iter2 @@ -1163,11 +1184,31 @@ module Annotate (C : ANNOTATE_CONFIG) = struct Format.eprintf "Renaming call from %s to %s@ at %a.@." name name1 PP.pp_pos loc in + let eqs3 = + List.map + (fun (param_name, e) -> + let e' = annotate_static_constrained_integer ~loc env e in + (param_name, e')) + eqs2 + in + let eqs4 = + List.fold_left2 + (fun eqs (callee_x, _) (caller_ty, caller_e) -> + if + List.exists + (fun (p_name, _ty) -> String.equal callee_x p_name) + callee_params + then + let+ () = check_constrained_integer ~loc env caller_ty in + (callee_x, caller_e) :: eqs + else eqs) + eqs3 callee_arg_types caller_arg_typed + in let ret_ty1 = match (call_type, ret_ty) with (* Begin FCallGetter *) | (ST_Function | ST_Getter), Some ty -> - Some (rename_ty_eqs eqs2 ty) |: TypingRule.FCallGetter + Some (rename_ty_eqs eqs4 ty) |: TypingRule.FCallGetter (* End *) (* Begin FCallSetter *) | (ST_Setter | ST_Procedure), None -> None |: TypingRule.FCallSetter @@ -1179,7 +1220,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* End *) in let () = if false then Format.eprintf "Annotated call to %S.@." name1 in - (name1, args1, eqs2, ret_ty1) + (name1, args1, eqs4, ret_ty1) and annotate_expr env (e : expr) : ty * expr = let () = if false then Format.eprintf "@[Annotating %a@]@." PP.pp_expr e in @@ -1637,7 +1678,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct in LE_SetArray (le2, e_index') |> here |: TypingRule.LESetArray (* End *) - | _ -> fatal_from le1 (Error.UnsupportedExpr (expr_of_lexpr le1))) + | _ -> unsupported_expr (expr_of_lexpr le1)) | _ -> conflict le1 [ default_t_bits ] t_le1) | LE_SetField (le1, field) -> (let t_le1, _ = expr_of_lexpr le1 |> annotate_expr env in @@ -1981,19 +2022,23 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | T_Int UnConstrained, T_Int _ | T_Int _, T_Int UnConstrained -> UnConstrained | T_Int (WellConstrained cs1), T_Int (WellConstrained cs2) -> ( + let bot_cs, top_cs = + match dir with Up -> (cs1, cs2) | Down -> (cs2, cs1) + in try - let bot_cs, top_cs = - match dir with Up -> (cs1, cs2) | Down -> (cs2, cs1) - in let bot = min_constraints env bot_cs and top = max_constraints env top_cs in if bot <= top then WellConstrained [ Constraint_Range (expr_of_z bot, expr_of_z top) ] else WellConstrained cs1 - with ConstraintMinMaxTop -> - (* TODO: this case is not specified by the LRM. *) - UnConstrained) + with ConstraintMinMaxTop -> ( + match (bot_cs, top_cs) with + | [ Constraint_Exact e_bot ], [ Constraint_Exact e_top ] -> + WellConstrained [ Constraint_Range (e_bot, e_top) ] + | _ -> + (* TODO: this case is not specified by the LRM. *) + UnConstrained)) | T_Int (UnderConstrained _), T_Int _ | T_Int _, T_Int (UnderConstrained _) -> assert false @@ -2093,7 +2138,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct if not (should_reduce_to_call env x) then None else let ( let* ) = Option.bind in - let _, _, _, ty_opt = + let _, _, _, ty_opt, _ = try Fn.try_find_name le env x [] with Error.ASLException _ -> assert false in @@ -2165,6 +2210,23 @@ module Annotate (C : ANNOTATE_CONFIG) = struct | LE_Concat (_les, _) -> None | LE_SetArray _ -> assert false + let fold_types_func_sig folder f init = + let from_args = + List.fold_left (fun acc (_x, t) -> folder acc t) init f.args + in + match f.return_type with None -> from_args | Some t -> folder from_args t + + let get_undeclared_defining env = + let of_ty acc ty = + match ty.desc with + | T_Bits ({ desc = E_Var x; _ }, _) -> + if StaticEnv.is_undefined x env then ISet.add x acc else acc + | _ -> acc + in + fun f -> fold_types_func_sig of_ty f ISet.empty + + let use_func_sig f = fold_types_func_sig ASTUtils.use_ty f ISet.empty + let annotate_func_sig ~loc env (f : AST.func) : env * AST.func = let () = if false then @@ -2173,40 +2235,74 @@ module Annotate (C : ANNOTATE_CONFIG) = struct in (* Build typing local environment. *) let env1 = { env with local = empty_local } in + let potential_params = get_undeclared_defining env1 f in (* Add explicit parameters *) - let env2, parameters = - let one_param env1' (x, ty_opt) = - let ty = + let env2, declared_params = + let () = + if false then + Format.eprintf "Defined potential parameters: %a@." ISet.pp_print + potential_params + in + let folder (env1', acc) (x, ty_opt) = + let+ () = check_var_not_in_env loc env1' x in + let+ () = + check_true (ISet.mem x potential_params) @@ fun () -> + fatal_from loc (Error.ParameterWithoutDecl x) + in + let t = match ty_opt with - | Some ty -> annotate_type ~loc env1 ty - | None -> Types.under_constrained_ty x + | None | Some { desc = T_Int UnConstrained; _ } -> + Types.under_constrained_ty x + | Some t -> annotate_type ~loc env1 t + (* Type should be valid in the env with no param declared. *) in - let+ () = check_var_not_in_env loc env1' x in - (* Subtility here: the type should be valid in the env with nothing declared, i.e. [env1]. *) - (add_local x ty LDK_Let env1', (x, Some ty)) + let+ () = check_constrained_integer ~loc env1 t in + (add_local x t LDK_Let env1', IMap.add x t acc) in - list_fold_left_map one_param env1 f.parameters + List.fold_left folder (env1, IMap.empty) f.parameters in - let () = if false then Format.eprintf "Parameters added.@." in - (* Add dependently typed identifiers, from arguments. *) - let env3 = - let add_dependently_typed_from_ty env2' (_, ty) = - let () = - if false then Format.eprintf "Seeing arg of type %a@." PP.pp_ty ty - in - match ty.desc with - | T_Bits ({ desc = E_Var x; _ }, _) -> ( - match StaticEnv.type_of_opt env2' x with - | Some t -> - let () = - if false then - Format.eprintf "%S Already typed: %a@." x PP.pp_ty t - in - env2' - | None -> add_local x (Types.under_constrained_ty x) LDK_Let env2') - | _ -> env2' + let () = if false then Format.eprintf "Explicit parameters added.@." in + (* Add arguments as parameters. *) + let env3, arg_params = + let used = + use_func_sig f + |> ISet.filter (fun s -> + StaticEnv.is_undefined s env1 && not (IMap.mem s declared_params)) + in + let () = + if false then + Format.eprintf "Undefined used in func sig: %a@." ISet.pp_print used in - List.fold_left add_dependently_typed_from_ty env2 f.args + let folder (env2', acc) (x, ty) = + if ISet.mem x used then + let+ () = check_var_not_in_env loc env2' x in + let t = + match ty.desc with + | T_Int UnConstrained -> Types.under_constrained_ty x + | _ -> annotate_type ~loc env2 ty + (* Type sould be valid in env with explicit parameters added, but no implicit parameter from args added. *) + in + let+ () = check_constrained_integer ~loc env2 t in + (add_local x t LDK_Let env2', IMap.add x t acc) + else (env2', acc) + in + List.fold_left folder (env2, IMap.empty) f.args + in + let parameters = + List.append (IMap.bindings declared_params) (IMap.bindings arg_params) + |> List.map (fun (x, t) -> (x, Some t)) + in + let env3, parameters = + (* Do not transliterate, only for v0: promote potential params as params. *) + if C.check = `TypeCheck then (env3, parameters) + else + let folder x (env3', parameters) = + if var_in_env env3 x then (env3', parameters) + else + let t = Types.under_constrained_ty x in + (add_local x t LDK_Let env3', (x, Some t) :: parameters) + in + ISet.fold folder potential_params (env3, parameters) in let () = if false then @@ -2216,32 +2312,36 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Add arguments. *) let env4, args = let one_arg env3' (x, ty) = - let () = if false then Format.eprintf "Adding argument %s.@." x in - let+ () = check_var_not_in_env loc env3' x in - (* Subtility here: the type should be valid in the env with parameters declared, i.e. [env3]. *) - let ty' = annotate_type ~loc env3 ty in - let env3'' = add_local x ty' LDK_Let env3' in - (env3'', (x, ty')) + if IMap.mem x arg_params then + let ty' = annotate_type ~loc env2 ty in + (env3', (x, ty')) + else + let () = if false then Format.eprintf "Adding argument %s.@." x in + let+ () = check_var_not_in_env loc env3' x in + (* Subtility here: the type should be valid in the env with parameters declared, i.e. [env3]. *) + let ty' = annotate_type ~loc env3 ty in + let env3'' = add_local x ty' LDK_Let env3' in + (env3'', (x, ty')) in list_fold_left_map one_arg env3 f.args in - let () = - if false then - Format.eprintf "@[Annotating return-type in env:@ %a@]@." - StaticEnv.pp_env env4 - in (* Check return type. *) let env5, return_type = match f.return_type with - | None -> (env4, None) + | None -> (env4, f.return_type) | Some ty -> - (* Subtility here: the type should be valid in the env with arguments declared, i.e. [env4]. *) - let ty' = annotate_type ~loc env4 ty in + let () = + if false then + Format.eprintf "@[Annotating return-type in env:@ %a@]@." + StaticEnv.pp_env env3 + in + (* Subtility here: the type should be valid in the env with parameters declared, i.e. [env3]. *) + let ty' = annotate_type ~loc env3 ty in let return_type = Some ty' in let env4' = StaticEnv.{ env4 with local = { env4.local with return_type } } in - (env4', Some ty') + (env4', return_type) in (env5, { f with parameters; args; return_type }) @@ -2402,7 +2502,9 @@ module Annotate (C : ANNOTATE_CONFIG) = struct let rename_primitive loc env (f : AST.func) = let name = best_effort f.name @@ fun _ -> - let _, name, _, _ = Fn.find_name loc env f.name (List.map snd f.args) in + let _, name, _, _, _ = + Fn.find_name loc env f.name (List.map snd f.args) + in name in { f with name } diff --git a/asllib/error.ml b/asllib/error.ml index fd734b086..60c140314 100644 --- a/asllib/error.ml +++ b/asllib/error.ml @@ -56,6 +56,8 @@ type error_desc = | BadLDI of AST.local_decl_item | BadRecursiveDecls of identifier list | UnrespectedParserInvariant + | ConstrainedIntegerExpected of ty + | ParameterWithoutDecl of identifier type error = error_desc annotated @@ -202,6 +204,15 @@ let pp_error = (pp_comma_list (fun f -> fprintf f "%S")) decls | UnrespectedParserInvariant -> fprintf f "Parser invariant broke." + | ConstrainedIntegerExpected t -> + fprintf f + "ASL Typing error:@ constrained@ integer@ expected,@ provided@ %a" + pp_ty t + | ParameterWithoutDecl s -> + fprintf f + "ASL Typing error:@ explicit@ parameter@ %S@ does@ not@ have@ a@ \ + corresponding@ defining@ argument" + s | BadReturnStmt (Some t) -> fprintf f "ASL Typing error:@ cannot@ return@ nothing@ from@ a@ function,@ an@ \ diff --git a/asllib/libdir/stdlib.asl b/asllib/libdir/stdlib.asl index 4d6c0f2e9..4644dde7f 100644 --- a/asllib/libdir/stdlib.asl +++ b/asllib/libdir/stdlib.asl @@ -90,7 +90,7 @@ end func Replicate{M}(x: bits(M), N: integer) => bits(M*N) begin if M == 1 then - return ReplicateBit(IsZero(x),N); + return ReplicateBit(IsZero(x),N) as bits (M*N); else var r: bits(M*N) = Zeros(M*N); for i=0 to N-1 do @@ -162,12 +162,12 @@ begin return [Replicate(x[M-1], N - M), x]; end -func ZeroExtend(x :: bits(M), N::integer) => bits(N) +func ZeroExtend {M} (x :: bits(M), N::integer) => bits(N) begin return [Zeros(N - M), x]; end -func Extend(x :: bits(M), N :: integer, unsigned::boolean) => bits(N) +func Extend {M} (x :: bits(M), N :: integer, unsigned::boolean) => bits(N) begin return if unsigned then ZeroExtend(x, N) else SignExtend(x, N); end diff --git a/asllib/tests/asl.t/bug1.asl b/asllib/tests/asl.t/bug1.asl new file mode 100644 index 000000000..9a793d880 --- /dev/null +++ b/asllib/tests/asl.t/bug1.asl @@ -0,0 +1,8 @@ +func main () => integer +begin + let x: integer = 4; + let y: integer = 5; + let foo: bits(x) = Zeros(y); + + return 0; +end diff --git a/asllib/tests/asl.t/bug2.asl b/asllib/tests/asl.t/bug2.asl new file mode 100644 index 000000000..1d7bab541 --- /dev/null +++ b/asllib/tests/asl.t/bug2.asl @@ -0,0 +1,8 @@ +func main () => integer +begin + let x: integer = 4; + let y: integer = 5; + let t = y[x: 0]; + + return 0; +end diff --git a/asllib/tests/asl.t/bug3.asl b/asllib/tests/asl.t/bug3.asl new file mode 100644 index 000000000..b264f9ab1 --- /dev/null +++ b/asllib/tests/asl.t/bug3.asl @@ -0,0 +1,7 @@ +func main () => integer +begin + let x: integer = 4; + let t = Zeros(x); + + return 0; +end diff --git a/asllib/tests/asl.t/run.t b/asllib/tests/asl.t/run.t index 060cb9fe8..1d19753fd 100644 --- a/asllib/tests/asl.t/run.t +++ b/asllib/tests/asl.t/run.t @@ -138,7 +138,7 @@ Runtime checks: [1] $ cat >runtime-type-sat.asl < func test(size: integer) begin + > func test(size: integer {3, 4}) begin > let - = Zeros(4) as bits(size); > end > func main () => integer begin @@ -193,3 +193,17 @@ UnderConstrained integers: Arrays indexed by enumerations $ aslref enum-array.asl [0, 0, 0] + +Parameters bugs: + $ aslref bug1.asl + File bug1.asl, line 5, characters 21 to 29: + ASL Typing error: constrained integer expected, provided integer + [1] + $ aslref bug2.asl + ASL Typing error: constrained integer expected, provided integer + [1] + $ aslref bug3.asl + File bug3.asl, line 4, characters 10 to 18: + ASL Typing error: constrained integer expected, provided integer + [1] + diff --git a/asllib/tests/asltests.ml b/asllib/tests/asltests.ml index 7e41ab885..784a59ca6 100644 --- a/asllib/tests/asltests.ml +++ b/asllib/tests/asltests.ml @@ -8,7 +8,10 @@ let process_test path () = let ast, ver = build_ast_from_file path in (* First interprete it. *) let () = if _dbg then Format.eprintf "@[AST: %a@]@." PP.pp_t ast in - let i, _ = Native.interprete `TypeCheck ast in + let tc_strictness = + match ver with `ASLv0 -> `Silence | `ASLv1 -> `TypeCheck + in + let i, _ = Native.interprete tc_strictness ast in let () = assert (i = 0) in let () = if _dbg then Format.eprintf "Ran successfully.@.@." in diff --git a/asllib/types.ml b/asllib/types.ml index 7b4e7c5d9..484fbc947 100644 --- a/asllib/types.ml +++ b/asllib/types.ml @@ -223,7 +223,7 @@ module Domain = struct with StaticInterpreter.NotYetImplemented -> e in try StaticInterpreter.static_eval env e - with Error.ASLException { desc = Error.UndefinedIdentifier _; _ } -> + with StaticInterpreter.StaticEvaluationUnknown -> raise_notrace StaticEvaluationTop in match v with @@ -839,9 +839,7 @@ let rec base_value loc env t = let normalize env e = let open StaticInterpreter in try Normalize.normalize env e - with NotYetImplemented -> ( - try static_eval env e |> lit - with Error.ASLException _ | NotYetImplemented -> e) + with NotYetImplemented -> ( try static_eval env e |> lit with _ -> e) in let t_struct = get_structure env t in match t_struct.desc with From c88e920b4e492d56485b420e192629f07b4b25ee Mon Sep 17 00:00:00 2001 From: Hadrien Renaud Date: Mon, 4 Mar 2024 16:21:45 +0000 Subject: [PATCH 3/5] [asl] First transliteration of type-annotation --- asllib/doc/ASLTypingReference.tex | 364 ++++++++++++++++++ asllib/instrumentation.ml | 36 ++ .../TypingRule.TArray.asl | 22 ++ .../TypingRule.TBitField.asl | 20 + .../ASLTypingReference.t/TypingRule.TBits.asl | 21 + .../ASLTypingReference.t/TypingRule.TBool.asl | 20 + .../TypingRule.TEnumDecl.asl | 5 + .../TypingRule.TIntUnConstrained.asl | 20 + .../TypingRule.TIntUnderConstrained.asl | 18 + .../TypingRule.TIntWellConstrained.asl | 21 + .../TypingRule.TNamed.asl | 21 + .../TypingRule.TNonDecl.asl | 2 + .../ASLTypingReference.t/TypingRule.TReal.asl | 21 + .../TypingRule.TRecordExceptionDecl.asl | 6 + .../TypingRule.TString.asl | 20 + .../TypingRule.TTuple.asl | 22 ++ asllib/tests/ASLTypingReference.t/run.t | 19 + 17 files changed, 658 insertions(+) create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TArray.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TBitField.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TBits.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TBool.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TEnumDecl.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TIntUnConstrained.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TIntUnderConstrained.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TIntWellConstrained.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TNamed.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TNonDecl.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TReal.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TRecordExceptionDecl.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TString.asl create mode 100644 asllib/tests/ASLTypingReference.t/TypingRule.TTuple.asl diff --git a/asllib/doc/ASLTypingReference.tex b/asllib/doc/ASLTypingReference.tex index e2dd34a23..f4763f8e5 100644 --- a/asllib/doc/ASLTypingReference.tex +++ b/asllib/doc/ASLTypingReference.tex @@ -2137,6 +2137,370 @@ \subsection{Comments} \identr{TTGQ}, \identi{YHML}, \identi{YHRP}, \identi{VMZF}, \identi{YXSY}, \identi{LGHJ}, \identi{RXLG}. +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\chapter{Typing of types} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and one of the following applies: +\begin{itemize} + \item TypingRule.TString (see Section~\ref{sec:TypingRule.TString}); + \item TypingRule.TReal (see Section~\ref{sec:TypingRule.TReal}); + \item TypingRule.TBool (see Section~\ref{sec:TypingRule.TBool}); + \item TypingRule.TNamed (see Section~\ref{sec:TypingRule.TNamed}); + \item TypingRule.TInt (see Section~\ref{sec:TypingRule.TInt}); + \item TypingRule.TBits (see Section~\ref{sec:TypingRule.TBits}); + \item TypingRule.TTuple (see Section~\ref{sec:TypingRule.TTuple}); + \item TypingRule.TArray (see Section~\ref{sec:TypingRule.TArray}); + \item TypingRule.TEnumDecl (see Section~\ref{sec:TypingRule.TEnumDecl}); + \item TypingRule.TRecordExceptionDecl (see + Section~\ref{sec:TypingRule.TRecordExceptionDecl}); + \item TypingRule.TNonDecl (see Section~\ref{sec:TypingRule.TNonDecl}); + \item TypingRule.TBitField (see Section~\ref{sec:TypingRule.TBitField}). +\end{itemize} + + +\section{TypingRule.TString \label{sec:TypingRule.TString}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and all of the following apply: +\begin{itemize} + \item \texttt{ty} is the string type \TString. + \item \texttt{new\_ty} is the string type \TString. +\end{itemize} + +\subsection{Example} +In the following example, all the uses of \texttt{string} are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TString.asl} + +\subsection{Code} +\VerbatimInput[firstline=\TStringBegin, lastline=\TStringEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + +\section{TypingRule.TReal \label{sec:TypingRule.TReal}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and all of the following apply: +\begin{itemize} + \item \texttt{ty} is the real type \TReal. + \item \texttt{new\_ty} is the real type \TReal. +\end{itemize} + + +\subsection{Example} +In the following example, all the uses of \texttt{real} are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TReal.asl} + + +\subsection{Code} +\VerbatimInput[firstline=\TRealBegin, lastline=\TRealEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TBool \label{sec:TypingRule.TBool}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and all of the following apply: +\begin{itemize} + \item \texttt{ty} is the boolean type; + \item \texttt{new\_ty} is the boolean type. +\end{itemize} + +\subsection{Example} +In the following example, all the uses of \texttt{boolean} are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TBool.asl} + +\subsection{Code} +\VerbatimInput[firstline=\TBoolBegin, lastline=\TBoolEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TNamed \label{sec:TypingRule.TNamed}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and all of the following apply: +\begin{itemize} + \item \texttt{ty} is the a named type \texttt{x}; + \item One of the following applies: + \begin{itemize} + \item \texttt{x} is bound in \texttt{tenv} to a type; + \item an error ``\texttt{Undefined Identifier}'' is raised. + \end{itemize} + \item \texttt{new\_ty} is \texttt{ty}. +\end{itemize} + +\subsection{Example} +In the following example, all the uses of \texttt{MyType} are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TNamed.asl} + +\subsection{Code} +\VerbatimInput[firstline=\TNamedBegin, lastline=\TNamedEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TInt \label{sec:TypingRule.TInt}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and one of the following applies: +\begin{itemize} + \item All of the following apply: + \begin{itemize} + \item \texttt{ty} is the unconstrained integer type; + \item \texttt{new\_ty} is the unconstrained integer type. + \end{itemize} + \item All of the following apply: + \begin{itemize} + \item \texttt{ty} is a under-constrained integer type; + \item \texttt{new\_ty} is the under-constrained integer type \texttt{ty}. + \end{itemize} + \item All of the following apply: + \begin{itemize} + \item \texttt{ty} is the well-constrained integer type constrained by + \texttt{constraints}; + \item \texttt{constraints'} is the result of annotating each of the + constraints in \texttt{constraints}; + \item \texttt{new\_ty} is the well-constrained integer type constrained + by \texttt{constraints}. + \end{itemize} +\end{itemize} + +\subsection{Example} + +In the following examples, all the uses of integer types are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TIntUnConstrained.asl} +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TIntWellConstrained.asl} +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TIntUnderConstrained.asl} + +\subsection{Code} +\VerbatimInput[firstline=\TIntBegin, lastline=\TIntEnd]{../Typing.ml} + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TBits \label{sec:TypingRule.TBits}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and all of the following apply: +\begin{itemize} + \item \texttt{ty} is the bit-vector type with width given by the expression + \texttt{e\_width} and the bitfields given by \texttt{bitfields}; + \item \texttt{e\_width'} is the result of annotating the statically-evaluable integer expression \texttt{e\_width}; + \item \texttt{bitfields'} is the result of annotating the bitfields \texttt{bitfields} + \item \texttt{new\_ty} is the bit-vector type with width given by the expression + \texttt{e\_width'} and the bitfields given by \texttt{bitfields'}; +\end{itemize} + +\subsection{Example} +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TBits.asl} + + +\subsection{Code} +In the following example, all the uses of bitvector types are valid: +\VerbatimInput[firstline=\TBitsBegin, lastline=\TBitsEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TTuple \label{sec:TypingRule.TTuple}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and all of the following apply: +\begin{itemize} + \item \texttt{ty} is the tuple type with member types \texttt{tys}; + \item \texttt{tys'} is the result of annotating all the types in + \texttt{tys}; + \item \texttt{new\_ty} is the tuple type with member types \texttt{tys'}. +\end{itemize} + +\subsection{Example} +In the following example, all the uses of tuple types are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TTuple.asl} + + +\subsection{Code} +\VerbatimInput[firstline=\TTupleBegin, lastline=\TTupleEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TArray \label{sec:TypingRule.TArray}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and all of the following apply: +\begin{itemize} + \item All of the following holds: + \begin{itemize} + \item \texttt{ty} is the array type indexed by integer bounded by the + expression \texttt{e} and of elements of type \texttt{t}; + \item \texttt{t'} is the result of annotating the type \texttt{t} in + environment \texttt{env}; + \item \texttt{e'} is the result of annotating the statically evaluable + integer expression \texttt{e}; + \item \texttt{new\_ty} is the array type indexed by integer bounded by + the expression \texttt{e'} and of elements of type \texttt{t'}; + \end{itemize} + \item All of the following holds: + \begin{itemize} + \item \texttt{ty} is the array type indexed by an enumeration type named + \texttt{s} and of elements of type \texttt{t}; + \item \texttt{s} is bound in \texttt{env} to an enumeration type; + \item \texttt{t'} is the result of annotating the type \texttt{t} in + environment \texttt{env}; + \item \texttt{new\_ty} is the array type indexed by an enumeration type + named \texttt{s} and of elements of type \texttt{t'}; + \end{itemize} +\end{itemize} + +\subsection{Example} +In the following example, all the uses of array types are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TArray.asl} + +\subsection{Code} +\VerbatimInput[firstline=\TArrayBegin, lastline=\TArrayEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TEnumDecl \label{sec:TypingRule.TEnumDecl}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and all of the following apply: +\begin{itemize} + \item \texttt{ty} is the enumeration type with enumeration literals + \texttt{li}; + \item This is the declaration of \texttt{ty}; + \item One of the following applies: + \begin{itemize} + \item \texttt{li} does not contains any duplicate enumeration literal. + \item an error ``\texttt{Already declared identifier}'' is raised; + \end{itemize} + \item \texttt{new\_ty} is the enumeration type \texttt{ty}. +\end{itemize} + +\subsection{Example} +In the following example, all the uses of enumeration types are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TEnumDecl.asl} + + +\subsection{Code} +\VerbatimInput[firstline=\TEnumDeclBegin, lastline=\TEnumDeclEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TRecordExceptionDecl \label{sec:TypingRule.TRecordExceptionDecl}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and one of the following applies: +\begin{itemize} + \item All of the following apply: + \begin{itemize} + \item \texttt{ty} is the record type with fields \texttt{fields}; + \item This is the declaration of \texttt{ty}; + \item One of the following applies: + \begin{itemize} + \item \texttt{fields} does not contains any duplicate field. + \item an error ``\texttt{Already declared identifier}'' is raised; + \end{itemize} + \item \texttt{fields'} is the result of annotating each type in + \texttt{fields}; + \item \texttt{new\_ty} is the record type with fields \texttt{fields'}; + \end{itemize} + \item All of the following apply: + \begin{itemize} + \item \texttt{ty} is the exception type with fields \texttt{fields}; + \item This is the declaration of \texttt{ty}; + \item One of the following applies: + \begin{itemize} + \item \texttt{fields} does not contains any duplicate field. + \item an error ``\texttt{Already declared identifier}'' is raised; + \end{itemize} + \item \texttt{fields'} is the result of annotating each type in + \texttt{fields}; + \item \texttt{new\_ty} is the exception type with fields \texttt{fields'}; + \end{itemize} +\end{itemize} + + +\subsection{Example} +In the following example, all the uses of record or exception types are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TRecordExceptionDecl.asl} + + +\subsection{Code} +\VerbatimInput[firstline=\TRecordExceptionDeclBegin, lastline=\TRecordExceptionDeclEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TNonDecl \label{sec:TypingRule.TNonDecl}} + +\subsection{Prose} +Annotating a type~\texttt{ty} in an environment~\texttt{env} results in a +rewritten type~\texttt{new\_ty} and all of the following apply: +\begin{itemize} + \item One of the following applies: + \begin{itemize} + \item \texttt{ty} is a record type; + \item \texttt{ty} is an exception type; + \item \texttt{ty} is an enumeration type; + \end{itemize} + \item This is not the declaration of \texttt{ty}; + \item An error ``Cannot use anonymous form of enumerations, record, or exceptions here.'' is raised. +\end{itemize} + +\subsection{Example} + +In the following example, the use of a record type out of a declaration is invalid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TNonDecl.asl} + +\subsection{Code} +\VerbatimInput[firstline=\TNonDeclBegin, lastline=\TNonDeclEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + +\section{TypingRule.TBitField \label{sec:TypingRule.TBitField}} + +\subsection{Prose} + + +\subsection{Example} +In the following example, all the uses of bitvector types with bitfields are valid: +\VerbatimInput{../tests/ASLTypingReference.t/TypingRule.TBitField.asl} + + +\subsection{Code} +\VerbatimInput[firstline=\TBitFieldBegin, lastline=\TBitFieldEnd]{../Typing.ml} + + +\isempty{\subsection{Comments}} + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \chapter{Typing of Expressions} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/asllib/instrumentation.ml b/asllib/instrumentation.ml index e66b9455b..9c0972e83 100644 --- a/asllib/instrumentation.ml +++ b/asllib/instrumentation.ml @@ -479,6 +479,18 @@ module TypingRule = struct | DeclareGlobalStorage | DeclareTypeDecl | Specification + | TString + | TReal + | TBool + | TNamed + | TInt + | TBits + | TTuple + | TArray + | TEnumDecl + | TRecordExceptionDecl + | TNonDecl + | TBitField let to_string : t -> string = function | BuiltinSingularType -> "BuiltinSingularType" @@ -612,6 +624,18 @@ module TypingRule = struct | DeclareGlobalStorage -> "DeclareGlobalStorage" | DeclareTypeDecl -> "DeclareTypeDecl" | Specification -> "Specification" + | TString -> "TString" + | TReal -> "TReal" + | TBool -> "TBool" + | TNamed -> "TNamed" + | TInt -> "TInt" + | TBits -> "TBits" + | TTuple -> "TTuple" + | TArray -> "TArray" + | TEnumDecl -> "TEnumDecl" + | TRecordExceptionDecl -> "TRecordExceptionDecl" + | TNonDecl -> "TNonDecl" + | TBitField -> "TBitField" let pp f r = to_string r |> Format.pp_print_string f @@ -725,6 +749,18 @@ module TypingRule = struct CatcherNone; CatcherSome; Subprogram; + TString; + TReal; + TBool; + TNamed; + TInt; + TBits; + TTuple; + TArray; + TEnumDecl; + TRecordExceptionDecl; + TNonDecl; + TBitField; ] let all_nb = List.length all diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TArray.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TArray.asl new file mode 100644 index 000000000..a8f9271c8 --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TArray.asl @@ -0,0 +1,22 @@ +type MyType of array [4] of integer; + +func foo (x: array [4] of integer) => array [4] of integer +begin + var y = x; + y[3] = 2; + return y; +end + +func main () => integer +begin + var x: array [4] of integer; + + x[1] = 1; + print(x); + x = foo (x as array [4] of integer); + + let y: array [4] of integer = x; + + + return 0; +end diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TBitField.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TBitField.asl new file mode 100644 index 000000000..fa2ad33fb --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TBitField.asl @@ -0,0 +1,20 @@ +type MyType of bits(4) { [3:2] A, [1] B }; + +func foo (x: bits(4) { [3:2] A, [1] B }) => bits(4) { [3:2] A, [1] B } +begin + return x; +end + +func main () => integer +begin + var x: bits(4) { [3:2] A, [1] B }; + + x = '1010'; + x = foo (x as bits(4) { [3:2] A, [1] B }); + + let y: bits(4) { [3:2] A, [1] B } = x; + + assert x as bits(4) { [3:2] A, [1] B } == x; + + return 0; +end diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TBits.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TBits.asl new file mode 100644 index 000000000..957841ceb --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TBits.asl @@ -0,0 +1,21 @@ +type MyType of bits(4); + +func foo (x: bits(4)) => bits(4) +begin + return NOT x; +end + +func main () => integer +begin + var x: bits(4); + + x = '1010'; + x = foo (x as bits(4)); + + let y: bits(4) = x; + + assert x as bits(4) == x; + + return 0; +end + diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TBool.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TBool.asl new file mode 100644 index 000000000..4614a1866 --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TBool.asl @@ -0,0 +1,20 @@ +type MyType of boolean; + +func foo (x: boolean) => boolean +begin + return FALSE --> x; +end + +func main () => integer +begin + var x: boolean; + + x = TRUE; + x = foo (x as boolean); + + let y: boolean = x && x; + + assert x as boolean == x; + + return 0; +end diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TEnumDecl.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TEnumDecl.asl new file mode 100644 index 000000000..37ea57e9b --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TEnumDecl.asl @@ -0,0 +1,5 @@ +type MyEnum of enumeration { A, B, C }; + +func main () => integer +begin return 0; end + diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnConstrained.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnConstrained.asl new file mode 100644 index 000000000..653fbd8b3 --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnConstrained.asl @@ -0,0 +1,20 @@ +type MyType of integer; +func foo (x: integer) => integer +begin + return x; +end + +func main () => integer +begin + var x: integer; + + x = 4; + x = foo (x as integer); + + let y: integer = x; + + assert x as integer == x; + + return 0; +end + diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnderConstrained.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnderConstrained.asl new file mode 100644 index 000000000..d9f840573 --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TIntUnderConstrained.asl @@ -0,0 +1,18 @@ +func foo {N} (x: bits(N)) => integer +begin + return N; +end + +func bar (N: integer) => bits(N) +begin + return Zeros(N); +end + +func main() => integer +begin + assert 3 == foo ('101'); + assert bar(3) == '000'; + + return 0; +end + diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TIntWellConstrained.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TIntWellConstrained.asl new file mode 100644 index 000000000..128bd653f --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TIntWellConstrained.asl @@ -0,0 +1,21 @@ +type MyType of integer {1..12}; + +func foo (x: integer {1..12}) => integer {1..12} +begin + return x; +end + +func main () => integer +begin + var x: integer {1..12}; + + x = 4; + x = foo (x as integer {1..12}); + + let y: integer {1..12} = x; + + assert x as integer {1..11} == x; + + return 0; +end + diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TNamed.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TNamed.asl new file mode 100644 index 000000000..14e25098d --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TNamed.asl @@ -0,0 +1,21 @@ +type MyType of integer; + +func foo (x: MyType) => MyType +begin + return x; +end + +func main () => integer +begin + var x: MyType; + + x = 4; + x = foo (x as MyType); + + let y: MyType = x; + + assert x as MyType == x; + + return 0; +end + diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TNonDecl.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TNonDecl.asl new file mode 100644 index 000000000..ac7dde2aa --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TNonDecl.asl @@ -0,0 +1,2 @@ +func (x: record { a: integer, b: boolean }) => integer +begin return 0; end diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TReal.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TReal.asl new file mode 100644 index 000000000..5a1804232 --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TReal.asl @@ -0,0 +1,21 @@ +type MyType of real; + +func foo (x: real) => real +begin + return x + 1.0; +end + +func main () => integer +begin + var x: real; + + x = 3.141592; + x = foo (x as real); + + let y: real = x + x; + + assert x as real == x; + + return 0; +end + diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TRecordExceptionDecl.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TRecordExceptionDecl.asl new file mode 100644 index 000000000..33e05e5fe --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TRecordExceptionDecl.asl @@ -0,0 +1,6 @@ +type MyRecord of record { a: integer, b: boolean }; +type MyException of exception { a: integer, b: boolean }; + +func main () => integer +begin return 0; end + diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TString.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TString.asl new file mode 100644 index 000000000..9ad08a6e1 --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TString.asl @@ -0,0 +1,20 @@ +type MyType of string; + +func foo (x: string) => string +begin + return x; +end + +func main () => integer +begin + var x: string; + + x = "foo"; + x = foo (x as string); + + let y: string = x; + + assert x as string == x; + + return 0; +end diff --git a/asllib/tests/ASLTypingReference.t/TypingRule.TTuple.asl b/asllib/tests/ASLTypingReference.t/TypingRule.TTuple.asl new file mode 100644 index 000000000..cc16ee3b7 --- /dev/null +++ b/asllib/tests/ASLTypingReference.t/TypingRule.TTuple.asl @@ -0,0 +1,22 @@ +type MyType of (integer, boolean); + +func foo (x: (integer, boolean)) => (integer, boolean) +begin + let (z, y): (integer, boolean) = x; + return (z + 1, FALSE --> y); +end + +func main () => integer +begin + var x: (integer, boolean); + + x = (3, TRUE); + x = foo (x as (integer, boolean)); + + let y: (integer, boolean) = x; + + let (x0, x1) = x as (integer, boolean); + assert x0 == 4 && x1 == TRUE; + + return 0; +end diff --git a/asllib/tests/ASLTypingReference.t/run.t b/asllib/tests/ASLTypingReference.t/run.t index 120ee3fef..ee2db85f1 100644 --- a/asllib/tests/ASLTypingReference.t/run.t +++ b/asllib/tests/ASLTypingReference.t/run.t @@ -21,3 +21,22 @@ ASL Typing Reference: $ aslref TypingRule.LDTyped.asl $ aslref TypingRule.LDTuple.asl $ aslref TypingRule.Lit.asl + +ASL Typing Reference / annotating types: + $ aslref TypingRule.TReal.asl + $ aslref TypingRule.TBool.asl + $ aslref TypingRule.TNamed.asl + $ aslref TypingRule.TIntUnConstrained.asl + $ aslref TypingRule.TIntWellConstrained.asl + $ aslref TypingRule.TIntUnderConstrained.asl + $ aslref TypingRule.TBits.asl + $ aslref TypingRule.TTuple.asl + $ aslref TypingRule.TArray.asl + [0, 1, 0, 0] + $ aslref TypingRule.TEnumDecl.asl + $ aslref TypingRule.TRecordExceptionDecl.asl + $ aslref TypingRule.TNonDecl.asl + File TypingRule.TNonDecl.asl, line 1, characters 5 to 6: + ASL Error: Cannot parse. + [1] + $ aslref TypingRule.TBitField.asl From 68dc69680d32678a683c96acce32f901e3340f2c Mon Sep 17 00:00:00 2001 From: Hadrien Renaud Date: Wed, 10 Apr 2024 18:53:31 +0100 Subject: [PATCH 4/5] [asl] Small changes to Domain construction --- asllib/tests/asl.t/bug4.asl | 8 ++++++++ asllib/tests/asl.t/run.t | 5 +++++ asllib/types.ml | 6 ++++-- 3 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 asllib/tests/asl.t/bug4.asl diff --git a/asllib/tests/asl.t/bug4.asl b/asllib/tests/asl.t/bug4.asl new file mode 100644 index 000000000..d58fb7a56 --- /dev/null +++ b/asllib/tests/asl.t/bug4.asl @@ -0,0 +1,8 @@ +func main() => integer +begin + let a: integer {3, 4} = 3; + let b: integer {3, 4} = 4; + let pb = Zeros(a) OR Zeros(b); + + return 0; +end diff --git a/asllib/tests/asl.t/run.t b/asllib/tests/asl.t/run.t index 1d19753fd..63d1974cc 100644 --- a/asllib/tests/asl.t/run.t +++ b/asllib/tests/asl.t/run.t @@ -206,4 +206,9 @@ Parameters bugs: File bug3.asl, line 4, characters 10 to 18: ASL Typing error: constrained integer expected, provided integer [1] + $ aslref bug4.asl + File bug4.asl, line 5, characters 11 to 31: + ASL Typing error: Illegal application of operator OR on types bits(a) + and bits(b) + [1] diff --git a/asllib/types.ml b/asllib/types.ml index 484fbc947..219d72501 100644 --- a/asllib/types.ml +++ b/asllib/types.ml @@ -346,7 +346,10 @@ module Domain = struct | T_Bits (width, _) -> ( try match of_expr env width with - | D_Int is -> D_Bits is + | D_Int (Finite int_set as d) -> + if Z.equal (IntSet.cardinal int_set) Z.one then D_Bits d + else raise StaticEvaluationTop + | D_Int (FromSyntax [ Constraint_Exact _ ] as d) -> D_Bits d | _ -> raise StaticEvaluationTop with StaticEvaluationTop -> D_Bits (FromSyntax [ Constraint_Exact width ])) @@ -408,7 +411,6 @@ module Domain = struct if Z.equal (IntSet.cardinal int_set) Z.one then Some (IntSet.min_elt int_set |> IntSet.Interval.x) else None - | D_Bits _ -> None | _ -> None end From 1244bb89f62a3aff3d7738ee4ffde5acf409a783 Mon Sep 17 00:00:00 2001 From: Hadrien Renaud Date: Thu, 11 Apr 2024 00:56:57 +0100 Subject: [PATCH 5/5] [asl] Use more constraints in stdlib.asl --- asllib/Native.ml | 36 +++++++++++++++++++++++++++--------- herd/ASLSem.ml | 16 ++++++++++++++-- 2 files changed, 41 insertions(+), 11 deletions(-) diff --git a/asllib/Native.ml b/asllib/Native.ml index 88be1785e..c7669487e 100644 --- a/asllib/Native.ml +++ b/asllib/Native.ml @@ -316,8 +316,18 @@ module NativeBackend = struct let round_towards_zero = wrap_real_to_int "RoundTowardsZero" truncate let primitives = + let e_var x = E_Var x |> add_dummy_pos in + let eoi i = expr_of_int i in + let binop = ASTUtils.binop in + let minus_one e = binop MINUS e (eoi 1) in + let pow_2 = binop POW (eoi 2) in + let neg e = E_Unop (NEG, e) |> add_pos_from e in (* [t_bits "N"] is the bitvector type of length [N]. *) - let t_bits x = T_Bits (E_Var x |> add_dummy_pos, []) |> add_dummy_pos in + let t_bits x = T_Bits (e_var x, []) |> add_dummy_pos in + (* [t_int_ctnt e1 e2] is [integer {e1..e2}] *) + let t_int_ctnt e1 e2 = + T_Int (WellConstrained [ Constraint_Range (e1, e2) ]) |> add_dummy_pos + in (* [p ~parameters ~args ~returns name f] declares a primtive named [name] with body [f], and signature specified by [parameters] [args] and [returns]. *) @@ -329,14 +339,22 @@ module NativeBackend = struct ({ name; parameters; args; body; return_type; subprogram_type }, f) in [ - p - ~parameters:[ ("N", None) ] - ~args:[ ("x", t_bits "N") ] - ~returns:integer "UInt" uint; - p - ~parameters:[ ("N", None) ] - ~args:[ ("x", t_bits "N") ] - ~returns:integer "SInt" sint; + (let two_pow_n_minus_one = minus_one (pow_2 (e_var "N")) in + let returns = t_int_ctnt (eoi 0) two_pow_n_minus_one in + p + ~parameters:[ ("N", None) ] + ~args:[ ("x", t_bits "N") ] + ~returns "UInt" uint); + (let two_pow_n_minus_one = pow_2 (minus_one (e_var "N")) in + let minus_two_pow_n_minus_one = neg two_pow_n_minus_one + and two_pow_n_minus_one_minus_one = minus_one two_pow_n_minus_one in + let returns = + t_int_ctnt minus_two_pow_n_minus_one two_pow_n_minus_one_minus_one + in + p + ~parameters:[ ("N", None) ] + ~args:[ ("x", t_bits "N") ] + ~returns "SInt" sint); p ~args:[ ("x", integer) ] ~returns:string "DecStr" dec_str; p ~args:[ ("x", integer) ] ~returns:string "HexStr" hex_str; p ~args:[ ("x", integer) ] ~returns:string "AsciiStr" ascii_str; diff --git a/herd/ASLSem.ml b/herd/ASLSem.ml index fd887a1f5..257e5d17a 100644 --- a/herd/ASLSem.ml +++ b/herd/ASLSem.ml @@ -648,6 +648,9 @@ module Make (C : Config) = struct let open AST in let with_pos = Asllib.ASTUtils.add_dummy_pos in let integer = Asllib.ASTUtils.integer in + let int_ctnt e1 e2 = + T_Int (WellConstrained [ Constraint_Range (e1, e2) ]) |> with_pos + in let boolean = Asllib.ASTUtils.boolean in let reg = integer in let var x = E_Var x |> with_pos in @@ -656,7 +659,16 @@ module Make (C : Config) = struct let bv_var x = bv @@ var x in let bv_lit x = bv @@ lit x in let bv_64 = bv_lit 64 in + let binop = Asllib.ASTUtils.binop in + let minus_one e = binop MINUS e (lit 1) in + let pow_2 = binop POW (lit 2) in let t_named x = T_Named x |> with_pos in + let uint_returns = + int_ctnt (lit 0) (minus_one (pow_2 (var "N"))) + and sint_returns = + let big_pow = pow_2 (minus_one (var "N")) in + int_ctnt (E_Unop(NEG, big_pow) |> with_pos) (minus_one big_pow) + in [ (* Fences *) p0 "primitive_isb" (primitive_isb ii_env); @@ -686,11 +698,11 @@ module Make (C : Config) = struct p1r "UInt" ~parameters:[ ("N", None) ] ("x", bv_var "N") - ~returns:integer uint; + ~returns:uint_returns uint; p1r "SInt" ~parameters:[ ("N", None) ] ("x", bv_var "N") - ~returns:integer sint; + ~returns:sint_returns sint; (* Misc *) p0r "ProcessorID" ~returns:integer (processor_id ii_env); p2r "CanPredictFrom"