From 66b095f9f2feb870fe494502a07b37505136874d Mon Sep 17 00:00:00 2001 From: Hadrien Renaud Date: Thu, 21 Mar 2024 15:08:19 +0000 Subject: [PATCH] [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 | 264 ++++++++++++++++++++++++------------ 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, 274 insertions(+), 106 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 d4fc3f6c55..0e153b3b71 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 66200f5f6f..0405989717 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 d6af76f666..01bf353e75 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 @@ -833,6 +846,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 @@ -858,7 +872,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 @@ -929,13 +943,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 = @@ -960,7 +980,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 @@ -1098,7 +1118,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 () = @@ -1124,9 +1144,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 @@ -1141,7 +1160,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 @@ -1161,11 +1180,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 @@ -1177,7 +1216,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 @@ -1635,7 +1674,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 @@ -1979,19 +2018,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 @@ -2091,7 +2134,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 @@ -2163,6 +2206,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 @@ -2172,39 +2232,61 @@ module Annotate (C : ANNOTATE_CONFIG) = struct (* Build typing local environment. *) let env1 = { env with local = empty_local } in (* Add explicit parameters *) - let env2, parameters = - let one_param env1' (x, ty_opt) = - let ty = + let env2, declared_params = + let with_def = get_undeclared_defining env1 f in + let () = + if false then + Format.eprintf "Defined potential parameters: %a@." ISet.pp_print + with_def + in + let folder (env1', acc) (x, ty_opt) = + let+ () = check_var_not_in_env loc env1' x in + let+ () = + check_true (ISet.mem x with_def) @@ 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 + 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 add_dependently_typed_from_ty env2 f.args + 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 () = if false then @@ -2214,32 +2296,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 }) @@ -2400,7 +2486,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 fd734b086b..60c1403144 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 4d6c0f2e9b..4644dde7f7 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 0000000000..9a793d8803 --- /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 0000000000..1d7bab5413 --- /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 0000000000..b264f9ab12 --- /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 060cb9fe83..1d19753fd7 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 7e41ab8858..784a59ca63 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 7b4e7c5d95..484fbc9476 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