From d56912d9a5bdd2906b706022b6ae09af2d61be81 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Tue, 4 Jun 2024 13:08:24 -0500 Subject: [PATCH 1/6] Fail gracefully when lus_main does not exist, and allow lus_main to refer to global type declaration --- src/lustre/lustreInput.ml | 53 ++++++++++++++++++++++----------------- 1 file changed, 30 insertions(+), 23 deletions(-) diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index 650d97bd7..0af461813 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -309,19 +309,36 @@ let of_channel old_frontend only_parse in_ch = 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 ( + (* In the following try blocks, LN.node_of_name can throw Not_found *) + 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 could refer to a global type declaration (when checking realizability) *) + with Not_found -> try + let s_ident = LustreIdent.mk_string_ident (LGI.type_tag ^ s) in + 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) + ) | None -> ( match LustreNode.get_main_annotated_nodes nodes with | h :: t -> h :: t @@ -337,16 +354,6 @@ let of_channel old_frontend only_parse in_ch = 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 } From e64c4c00b6601de90a9179da8c6b1d53639aa3e4 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Wed, 5 Jun 2024 16:20:58 -0500 Subject: [PATCH 2/6] Use --lus_main_type flag for main type aliases rather than --lus_main --- src/flags.ml | 19 +++++++++++++++++++ src/flags.mli | 3 +++ src/lustre/lustreInput.ml | 32 ++++++++++++++++++++++++-------- 3 files changed, 46 insertions(+), 8 deletions(-) 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/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index 0af461813..bb26ec521 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -310,7 +310,6 @@ let of_channel old_frontend only_parse in_ch = let main_nodes = match Flags.lus_main () with | Some s -> let s_ident = LustreIdent.mk_string_ident s in ( - (* In the following try blocks, LN.node_of_name can throw Not_found *) try let main_lustre_node = LN.node_of_name s_ident nodes in (* If checking realizability, then @@ -324,13 +323,6 @@ let of_channel old_frontend only_parse in_ch = [s_ident; LustreIdent.mk_string_ident (LGI.inputs_tag ^ s)] else [s_ident] - - (* User specified main node could refer to a global type declaration (when checking realizability) *) - with Not_found -> try - let s_ident = LustreIdent.mk_string_ident (LGI.type_tag ^ s) in - 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 = @@ -349,6 +341,30 @@ 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 (NoMainNode 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 "Type alias '%a' not found in input" + (LustreIdent.pp_print_ident false) s_ident + in + raise (NoMainNode msg) + ) + | None -> main_nodes in Ok (nodes, globals, main_nodes) in From 3325923c7696af0d433edfe14e9e3a74299315c6 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Wed, 5 Jun 2024 16:24:48 -0500 Subject: [PATCH 3/6] Throw a different exception for when there is a --lus_main_type without realizability enabled --- src/kind2.ml | 3 ++- src/lustre/lustreInput.ml | 3 ++- src/lustre/lustreInput.mli | 4 +++- 3 files changed, 7 insertions(+), 3 deletions(-) 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/lustreInput.ml b/src/lustre/lustreInput.ml index bb26ec521..0363bbece 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 = @@ -348,7 +349,7 @@ let of_channel old_frontend only_parse in_ch = let msg = Format.asprintf "Option --lus_main_type can only be used when realizability checking is enabled (--enable CONTRACTCK)" in - raise (NoMainNode msg) + raise (MainTypeWithoutRealizability msg) else ( try let s_ident = LustreIdent.mk_string_ident (LGI.type_tag ^ s) in 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 -> From 77170d393cfa3d2c2a237a6e25254154f808b7d9 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Sun, 9 Jun 2024 11:06:02 -0500 Subject: [PATCH 4/6] Display whether or not a type decl contains a refinement type in lsp info --- src/lustre/lspInfo.ml | 14 ++++++++++---- src/lustre/lspInfo.mli | 2 +- src/lustre/lustreGenRefTypeImpNodes.ml | 9 ++++----- src/lustre/lustreInput.ml | 10 +++++----- src/lustre/lustreTransSys.ml | 1 + 5 files changed, 21 insertions(+), 15 deletions(-) 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 0363bbece..c564f4af1 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -166,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 ()) @@ -269,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" ; @@ -360,7 +360,7 @@ let of_channel old_frontend only_parse in_ch = (* User-specified type alias in command-line input might not exist *) with Not_found -> let msg = - Format.asprintf "Type alias '%a' not found in input" + Format.asprintf "No refinement type with alias '%a' found in input" (LustreIdent.pp_print_ident false) s_ident in raise (NoMainNode msg) diff --git a/src/lustre/lustreTransSys.ml b/src/lustre/lustreTransSys.ml index 4adfa3f52..f735d67be 100644 --- a/src/lustre/lustreTransSys.ml +++ b/src/lustre/lustreTransSys.ml @@ -456,6 +456,7 @@ let add_constraints_of_type init terms state_var = | None, None -> Term.mk_bool true in + (*!! Int range constraints for global constants, I think *) let qct = List.fold_left (fun acc (ty, iv) -> From 50628fcd17e831f0e8f431ec9ee2ceba762d9ea7 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Tue, 11 Jun 2024 11:28:37 -0500 Subject: [PATCH 5/6] Remove comment --- src/lustre/lustreTransSys.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/lustre/lustreTransSys.ml b/src/lustre/lustreTransSys.ml index f735d67be..4adfa3f52 100644 --- a/src/lustre/lustreTransSys.ml +++ b/src/lustre/lustreTransSys.ml @@ -456,7 +456,6 @@ let add_constraints_of_type init terms state_var = | None, None -> Term.mk_bool true in - (*!! Int range constraints for global constants, I think *) let qct = List.fold_left (fun acc (ty, iv) -> From fc4b5c5aec794cf6a6fd610d9a3e1613302e4ca1 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Mon, 17 Jun 2024 11:33:06 -0500 Subject: [PATCH 6/6] Handle missing --lus_main and handle --lus_main_type in old frontend --- src/lustre/lustreInput.ml | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index c564f4af1..5efe09bb7 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -293,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 @@ -304,6 +316,11 @@ 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