diff --git a/src/flags.ml b/src/flags.ml index f28e72a3f..f9b25580f 100644 --- a/src/flags.ml +++ b/src/flags.ml @@ -2906,6 +2906,24 @@ module Global = struct " ) let lus_main () = !lus_main + + + let lus_main_type_default = None + + let lus_main_type = ref lus_main_type_default + let _ = add_spec + "--lus_main_type" + (Arg.String (fun str -> lus_main_type := Some str)) + (fun fmt -> + Format.fprintf fmt + "\ + where is a type alias identifier from the Lustre input file@ \ + Designate a type declaration for which the corresponding generated node@ \ + is the top node for realizability analysis@ \ + Default: all type aliases \ + " + ) + let lus_main_type () = !lus_main_type (* Input format. *) @@ -3683,6 +3701,7 @@ let check_reach = Global.check_reach let check_nonvacuity = Global.check_nonvacuity let check_subproperties = Global.check_subproperties let lus_main = Global.lus_main +let lus_main_type = Global.lus_main_type let debug = Global.debug let debug_log = Global.debug_log let exit_code_mode = Global.exit_code_mode diff --git a/src/flags.mli b/src/flags.mli index 12e42e765..a64db3137 100644 --- a/src/flags.mli +++ b/src/flags.mli @@ -147,6 +147,9 @@ val add_input_file : string -> bool (** Main node in Lustre file *) val lus_main : unit -> string option +(** Main type alias in Lustre file *) +val lus_main_type : unit -> string option + (** Format of input file *) type input_format = [ `Lustre | `Horn | `Native ] val input_format : unit -> input_format diff --git a/src/kind2.ml b/src/kind2.ml index a60d958e5..4222e42c8 100644 --- a/src/kind2.ml +++ b/src/kind2.ml @@ -135,7 +135,8 @@ let setup : unit -> any_input = fun () -> | LustreAst.Parser_error -> (* We should have printed the appropriate message so just 'gracefully' exit *) KEvent.terminate_log () ; exit ExitCodes.parse_error - | LustreInput.NoMainNode msg -> + | LustreInput.NoMainNode msg + | LustreInput.MainTypeWithoutRealizability msg -> KEvent.log L_fatal "Error reading input file '%s': %s" in_file msg ; KEvent.terminate_log () ; exit ExitCodes.error | Sys_error msg -> diff --git a/src/lustre/lspInfo.ml b/src/lustre/lspInfo.ml index fe0b657ea..62b4a7eb2 100644 --- a/src/lustre/lspInfo.ml +++ b/src/lustre/lspInfo.ml @@ -21,22 +21,28 @@ module Ast = LustreAst let pp_print_fname_json ppf fname = if fname = "" then () else Format.fprintf ppf "\"file\" : \"%s\",@," fname -let lsp_type_decl_json ppf { Ast.start_pos = spos; Ast.end_pos = epos } = +let lsp_type_decl_json ppf ctx { Ast.start_pos = spos; Ast.end_pos = epos } = function - | LustreAst.AliasType (_, id, _) | LustreAst.FreeType (_, id) -> + | LustreAst.AliasType (p, id, _) | LustreAst.FreeType (p, id) -> let file, slnum, scnum = Lib.file_row_col_of_pos spos in let _, elnum, ecnum = Lib.file_row_col_of_pos epos in + (* TypeCheckerContext.pp_print_tc_context Format.std_formatter ctx; *) + (* print_endline (HString.string_of_hstring id); *) + let ty = TypeCheckerContext.expand_type_syn ctx (LustreAst.UserType (p, id)) in + let contains_ref = TypeCheckerContext.type_contains_ref ctx ty in Format.fprintf ppf ",@.{@[@,\ \"objectType\" : \"lsp\",@,\ \"source\" : \"lsp\",@,\ \"kind\" : \"typeDecl\",@,\ \"name\" : \"%a\",@,\ + \"containsRefinementType\" : \"%b\",@,\ %a\"startLine\" : %d,@,\ \"startColumn\" : %d,@,\ \"endLine\" : %d,@,\ \"endColumn\" : %d@]@.}@." HString.pp_print_hstring id + contains_ref pp_print_fname_json file slnum scnum elnum ecnum @@ -140,12 +146,12 @@ let lsp_contract_json ppf { Ast.start_pos = spos; Ast.end_pos = epos } pp_print_fname_json file slnum scnum elnum ecnum -let print_ast_info declarations = +let print_ast_info ctx declarations = List.iter (fun decl -> match decl with | LustreAst.TypeDecl (span, type_decl) -> - lsp_type_decl_json !Lib.log_ppf span type_decl + lsp_type_decl_json !Lib.log_ppf ctx span type_decl | LustreAst.ConstDecl (span, const_decl) -> lsp_const_decl_json !Lib.log_ppf span const_decl | LustreAst.NodeDecl (span, node) -> lsp_node_json !Lib.log_ppf span node diff --git a/src/lustre/lspInfo.mli b/src/lustre/lspInfo.mli index d2d370d2a..8f0b6b293 100644 --- a/src/lustre/lspInfo.mli +++ b/src/lustre/lspInfo.mli @@ -21,4 +21,4 @@ @author Abdalrhman Mohamed *) (* Print parsing information about top level declarations *) -val print_ast_info : LustreAst.declaration list -> unit +val print_ast_info : TypeCheckerContext.tc_context -> LustreAst.declaration list -> unit diff --git a/src/lustre/lustreGenRefTypeImpNodes.ml b/src/lustre/lustreGenRefTypeImpNodes.ml index c41ae294d..9aab4c3fe 100644 --- a/src/lustre/lustreGenRefTypeImpNodes.ml +++ b/src/lustre/lustreGenRefTypeImpNodes.ml @@ -52,7 +52,7 @@ let node_decl_to_contracts List.map (fun (p, id, ty, cl) -> (p, id, ty, cl, false)) outputs, List.map (fun (p, id, ty, cl, _) -> (p, id, ty, cl)) inputs in - (* Since we are omitting assumptions from environment realizablity checks, + (* Since we are omitting assumptions from environment realizability checks, we need to chase base types for environment inputs *) let inputs2 = List.map (fun (p, id, ty, cl, b) -> let ty = Chk.expand_type_syn_reftype_history_subrange ctx ty |> unwrap in @@ -73,10 +73,9 @@ let node_decl_to_contracts to the generated imported node. For example, if "ty" is a refinement type T = { x: int | x > C }, and C has a refinement type, then C's refinement type needs to be captured as an assumption in the output imported node. *) -let type_to_contract: Lib.position -> Ctx.tc_context -> HString.t -> A.lustre_type -> A.declaration option -= fun pos ctx id ty -> +let type_to_contract: Lib.position ->HString.t -> A.lustre_type -> A.declaration option += fun pos id ty -> let span = { A.start_pos = pos; end_pos = pos } in - if not (Ctx.type_contains_ref ctx ty) then None else let gen_node_id = HString.concat2 (HString.mk_hstring type_tag) id in (* To prevent slicing, we mark generated imported nodes as main nodes *) let node_items = [A.AnnotMain(pos, true)] in @@ -89,7 +88,7 @@ let gen_imp_nodes: Ctx.tc_context -> A.declaration list -> A.declaration list | A.ConstDecl (_, FreeConst _) | A.ConstDecl (_, TypedConst _) -> decl :: acc | A.TypeDecl (_, AliasType (p, id, ty)) -> - (match type_to_contract p ctx id ty with + (match type_to_contract p id ty with | Some decl1 -> decl :: decl1 :: acc | None -> decl :: acc) | A.TypeDecl (_, FreeType _) diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index 650d97bd7..5efe09bb7 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -66,6 +66,7 @@ let (let*) = Res.(>>=) let (>>) = Res.(>>) exception NoMainNode of string +exception MainTypeWithoutRealizability of string (* The parser has succeeded and produced a semantic value.*) let success (v : LustreAst.t): LustreAst.t = @@ -165,6 +166,10 @@ let type_check declarations = (* Step 8. Type check nodes and contracts *) let* global_ctx, warnings3 = TC.type_check_infer_nodes_and_contracts inlined_ctx sorted_node_contract_decls in + (* Provide lsp info if option is enabled *) + if Flags.log_format_json () && Flags.Lsp.lsp () then + LspInfo.print_ast_info global_ctx declarations; + (* Step 9. Generate imported nodes associated with refinement types if realizability checking is enabled *) let sorted_node_contract_decls = if List.mem `CONTRACTCK (Flags.enabled ()) @@ -268,10 +273,6 @@ let of_channel old_frontend only_parse in_ch = (* Get declarations from channel. *) let* declarations = ast_of_channel in_ch in - (* Provide lsp info if option is enabled *) - if Flags.log_format_json () && Flags.Lsp.lsp () then - LspInfo.print_ast_info declarations; - if old_frontend then Log.log L_note "Old front-end enabled" ; @@ -292,7 +293,19 @@ let of_channel old_frontend only_parse in_ch = (* Command-line flag for main node given? *) match Flags.lus_main () with (* Use given identifier to choose main node *) - | Some s -> [LustreIdent.mk_string_ident s] + | Some s -> + let s_ident = LustreIdent.mk_string_ident s in ( + try + let _ = LN.node_of_name s_ident nodes in + [s_ident] + (* User-specified main node in command-line input might not exist *) + with Not_found -> + let msg = + Format.asprintf "Main node '%a' not found in input" + (LustreIdent.pp_print_ident false) s_ident + in + raise (NoMainNode msg) + ) (* No main node name given on command-line *) | None -> ( try @@ -303,25 +316,39 @@ let of_channel old_frontend only_parse in_ch = This only happens when there are no nodes in the input. *) raise (NoMainNode "No main node defined in input")) in + let nodes, globals, main_nodes = + match Flags.lus_main_type () with + | Some _ -> raise (NoMainNode "Flag --lus_main_type not supported in old front-end") + | None -> nodes, globals, main_nodes + in Ok (nodes, globals, main_nodes) else let* (ctx, gids, decls, toplevel_nodes, _) = type_check declarations in let nodes, globals = LNG.compile ctx gids decls in let main_nodes = match Flags.lus_main () with | Some s -> - let s_ident = LustreIdent.mk_string_ident s in - let main_lustre_node = LN.node_of_name s_ident nodes in - (* If checking realizability, then - we are actually checking realizability of Kind 2-generated imported nodes representing - the (1) the main node's contract instrumented with type info and - (2) the main node's enviornment *) - if (not main_lustre_node.is_extern) && List.mem `CONTRACTCK (Flags.enabled ()) then - [LustreIdent.mk_string_ident (LGI.contract_tag ^ s); - LustreIdent.mk_string_ident (LGI.inputs_tag ^ s)] - else if main_lustre_node.is_extern && List.mem `CONTRACTCK (Flags.enabled ()) then - [s_ident; - LustreIdent.mk_string_ident (LGI.inputs_tag ^ s)] - else [s_ident] + let s_ident = LustreIdent.mk_string_ident s in ( + try + let main_lustre_node = LN.node_of_name s_ident nodes in + (* If checking realizability, then + we are actually checking realizability of Kind 2-generated imported nodes representing + the (1) the main node's contract instrumented with type info and + (2) the main node's enviornment *) + if (not main_lustre_node.is_extern) && List.mem `CONTRACTCK (Flags.enabled ()) then + [LustreIdent.mk_string_ident (LGI.contract_tag ^ s); + LustreIdent.mk_string_ident (LGI.inputs_tag ^ s)] + else if main_lustre_node.is_extern && List.mem `CONTRACTCK (Flags.enabled ()) then + [s_ident; + LustreIdent.mk_string_ident (LGI.inputs_tag ^ s)] + else [s_ident] + (* User-specified main node in command-line input might not exist *) + with Not_found -> + let msg = + Format.asprintf "Main node '%a' not found in input" + (LustreIdent.pp_print_ident false) s_ident + in + raise (NoMainNode msg) + ) | None -> ( match LustreNode.get_main_annotated_nodes nodes with | h :: t -> h :: t @@ -332,21 +359,35 @@ let of_channel old_frontend only_parse in_ch = s |> HString.string_of_hstring |> LustreIdent.mk_string_ident) ) in + let main_nodes = match Flags.lus_main_type () with + | Some s -> + let s_ident = LustreIdent.mk_string_ident s in + if not (List.mem `CONTRACTCK (Flags.enabled ())) then + let msg = + Format.asprintf "Option --lus_main_type can only be used when realizability checking is enabled (--enable CONTRACTCK)" + in + raise (MainTypeWithoutRealizability msg) + else ( + try + let s_ident = LustreIdent.mk_string_ident (LGI.type_tag ^ s) in + let _ = LN.node_of_name s_ident nodes in + match Flags.lus_main () with + | Some _ -> s_ident :: main_nodes + | None -> [s_ident] + (* User-specified type alias in command-line input might not exist *) + with Not_found -> + let msg = + Format.asprintf "No refinement type with alias '%a' found in input" + (LustreIdent.pp_print_ident false) s_ident + in + raise (NoMainNode msg) + ) + | None -> main_nodes in Ok (nodes, globals, main_nodes) in match result with | Ok (nodes, globals, main_nodes) -> - (* Check that main nodes all exist *) - main_nodes |> List.iter (fun mn -> - if not (LN.exists_node_of_name mn nodes) then - (* This can only happen when the name is passed as command-line argument *) - let msg = - Format.asprintf "Main node '%a' not found in input" - (LustreIdent.pp_print_ident false) mn - in - raise (NoMainNode msg) - ) ; let nodes = List.map (fun ({ LustreNode.name } as n) -> if List.exists (fun id -> LustreIdent.equal id name) main_nodes then { n with is_main = true } diff --git a/src/lustre/lustreInput.mli b/src/lustre/lustreInput.mli index 0d3ffa2f0..12479dd11 100644 --- a/src/lustre/lustreInput.mli +++ b/src/lustre/lustreInput.mli @@ -106,6 +106,7 @@ *) exception NoMainNode of string +exception MainTypeWithoutRealizability of string type error = [ | `LustreArrayDependencies of Lib.position * LustreArrayDependencies.error_kind @@ -128,7 +129,8 @@ type error = [ If a syntax or semantic error is detected, it triggers a [Parser_error] exception. If [only_parse] is false, and the Lustre model doesn't include a main node, it triggers a - {!NoMainNode} exception. + {!NoMainNode} exception. If --lus_main_type is used without CONTRACTCK + enabled, it triggers a {!MainTypeWithoutRealizability} exception. *) val of_file : ?old_frontend:bool -> bool -> string ->