Merge pull request kind2-mc#1075 from lorchrob/lsp-ref-type-info

Add --lus_main_type flag and give info about type declarations in LSP info

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 <string> 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

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

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 ->

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
         ",@.{@[<v 1>@,\
          \"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

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

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 _)

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 }

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 ->