[aslref] complete annotations for all left-/right- hand side expressions

asllib/Runner.ml

@@ -159,6 +159,7 @@ let run_with (args : args) : unit =
       || Option.is_some args.print_lisp
       || args.print_serialized_typed
 
+    let complete_type_annotations = false
     let use_field_getter_extension = args.use_field_getter_extension
     let override_mode = args.override_mode
 

asllib/TypeAnnotations.mli

@@ -0,0 +1,50 @@
+(** {b This module is not part of the ASL type system.}
+
+    Type annotation completion is an optional implementation-level
+    post-processing pass for consumers that require a fully annotated AST. It
+    does not decide whether an ASL program is well typed: it runs only after
+    ordinary typechecking has succeeded. Annotations inserted by this module are
+    consumer-facing metadata and must not be interpreted as results of ASL
+    typechecking.
+
+    The pass conservatively fills type annotation holes. These are not
+    necessarily the precise annotations that the ASL typechecker would infer or
+    generate. Existing typechecker annotations are preserved.
+
+    {b Explicit call parameter.} An explicit actual parameter is processed by
+    ordinary expression typing before completion. For example:
+    {[
+      let value = UInt{2}('11');
+    ]}
+    The parameter expression [2] has the constrained integer type assigned by
+    the typechecker. Completion preserves the annotation. More generally, an
+    explicit parameter retains whichever constrained or parameterized integer
+    type the typechecker assigned to it.
+
+    {b Inserted call parameter.} In the following call, the typechecker may
+    infer and insert the omitted width parameter [2] from the bitvector
+    argument:
+    {[
+      let value = UInt('11');
+    ]}
+    If that inserted expression has [ty_opt = None], completion assigns it
+    [T_Int UnConstrained]. This is not a claim that the typechecker inferred the
+    type [integer]; it is only the consumer-facing completion described above.
+
+    {b Structured base value.} A declaration without an initializer causes the
+    typechecker to synthesize a base value expression, for example:
+    {[
+      var registers : array [[31]] of bits(64);
+    ]}
+    Completion propagates the declared array type through the synthesized
+    structure: the array length uses the annotation on the declared length when
+    available, falling back to an unconstrained integer, and the repeated value
+    is completed as [bits(64)]. *)
+
+(** {1 Completion} *)
+
+val complete : ?validate:bool -> StaticEnv.global -> AST.t -> AST.t
+(** [complete ~validate genv ast] conservatively fills missing type annotations
+    in the already typechecked AST [ast], using global environment [genv] to
+    resolve named types. Existing annotations are preserved. When [validate] is
+    true, the completed AST is checked for any remaining annotation holes. *)

asllib/Typing.ml

@@ -142,6 +142,7 @@ module type ANNOTATE_CONFIG = sig
   val check : strictness
   val output_format : Error.output_format
   val print_typed : bool
+  val complete_type_annotations : bool
   val use_field_getter_extension : bool
   val fine_grained_side_effects : bool
   val use_conflicting_side_effects_extension : bool
@@ -4353,7 +4354,19 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
       let () = List.iter (check_global_pragma env) pragmas in
       (List.rev ast_rev, env)
 
-  let type_check_ast ast = type_check_ast_in_env empty_global ast
+  let type_check_ast ast =
+    let typed_ast, env = type_check_ast_in_env empty_global ast in
+    let should_complete_type_annotations =
+      match C.check with
+      | TypeCheck | TypeCheckNoWarn -> C.complete_type_annotations
+      | Warn | Silence -> false
+    in
+    let typed_ast =
+      if should_complete_type_annotations then
+        TypeAnnotations.complete ~validate:false env typed_ast
+      else typed_ast
+    in
+    (typed_ast, env)
 
   (* Note: produces a *dynamic* error if the main function cannot be found *)
   let find_main env =
@@ -4374,6 +4387,7 @@ module TypeCheckDefault = Annotate (struct
   let check = TypeCheck
   let output_format = Error.HumanReadable
   let print_typed = false
+  let complete_type_annotations = false
   let use_field_getter_extension = false
   let fine_grained_side_effects = false
   let use_conflicting_side_effects_extension = false

asllib/Typing.mli

@@ -38,6 +38,13 @@ module type ANNOTATE_CONFIG = sig
   val check : strictness
   val output_format : Error.output_format
   val print_typed : bool
+
+  val complete_type_annotations : bool
+  (** Whether to run the conservative type-annotation completion post-pass after
+      normal typechecking.
+      {b This post-pass is not part of the ASL type system, and annotations it
+         inserts are not typechecker results.} *)
+
   val use_field_getter_extension : bool
   val fine_grained_side_effects : bool
   val use_conflicting_side_effects_extension : bool

asllib/dune

@@ -76,7 +76,13 @@
  (modules
   (:standard \ aslref primitives_to_ml))
  (public_name aslref)
- (private_modules Parser0 Gparser0 Lexer0 SimpleLexer0 RepeatableLexer)
+ (private_modules
+  Parser0
+  Gparser0
+  Lexer0
+  SimpleLexer0
+  RepeatableLexer
+  TypeAnnotations)
  (modules_without_implementation Backend AST ParserConfig)
  (flags
   (:standard -w -40-42-48))

herd/ASLSem.ml

@@ -115,6 +115,7 @@ module Make (Conf : Config) = struct
 
     let output_format = Asllib.Error.HumanReadable
     let print_typed = false
+    let complete_type_annotations = false
     let use_field_getter_extension = false
     let fine_grained_side_effects = false
     let use_conflicting_side_effects_extension = false