Add lazy API to type-checker (#738)

Update generated opam files

sail_smt_backend.opam

@@ -1,7 +1,7 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 version: "0.18"
-synopsis: "Sail to C translation"
+synopsis: "Sail to SMT translation"
 maintainer: ["Sail Devs <[email protected]>"]
 authors: [
   "Alasdair Armstrong"

src/lib/ast_defs.ml

@@ -46,6 +46,14 @@
 
 open Ast
 
+type ('a, 'b) lazy_def = Strict_def of ('a, 'b) def | Lazy_fundef of id * ('a, 'b) def Lazy.t
+
+let force_lazy_def = function Strict_def def -> def | Lazy_fundef (_, (lazy def)) -> def
+
 type ('a, 'b) ast = { defs : ('a, 'b) def list; comments : (string * Lexer.comment list) list }
 
+type ('a, 'b) lazy_ast = { lazy_defs : ('a, 'b) lazy_def list; comments : (string * Lexer.comment list) list }
+
+let force_lazy_ast { lazy_defs; comments } = { defs = List.map force_lazy_def lazy_defs; comments }
+
 let empty_ast = { defs = []; comments = [] }

src/lib/ast_defs.mli

@@ -0,0 +1,59 @@
+(****************************************************************************)
+(*     Sail                                                                 *)
+(*                                                                          *)
+(*  Sail and the Sail architecture models here, comprising all files and    *)
+(*  directories except the ASL-derived Sail code in the aarch64 directory,  *)
+(*  are subject to the BSD two-clause licence below.                        *)
+(*                                                                          *)
+(*  The ASL derived parts of the ARMv8.3 specification in                   *)
+(*  aarch64/no_vector and aarch64/full are copyright ARM Ltd.               *)
+(*                                                                          *)
+(*  Copyright (c) 2013-2021                                                 *)
+(*    Kathyrn Gray                                                          *)
+(*    Shaked Flur                                                           *)
+(*    Stephen Kell                                                          *)
+(*    Gabriel Kerneis                                                       *)
+(*    Robert Norton-Wright                                                  *)
+(*    Christopher Pulte                                                     *)
+(*    Peter Sewell                                                          *)
+(*    Alasdair Armstrong                                                    *)
+(*    Brian Campbell                                                        *)
+(*    Thomas Bauereiss                                                      *)
+(*    Anthony Fox                                                           *)
+(*    Jon French                                                            *)
+(*    Dominic Mulligan                                                      *)
+(*    Stephen Kell                                                          *)
+(*    Mark Wassell                                                          *)
+(*    Alastair Reid (Arm Ltd)                                               *)
+(*                                                                          *)
+(*  All rights reserved.                                                    *)
+(*                                                                          *)
+(*  This work was partially supported by EPSRC grant EP/K008528/1 <a        *)
+(*  href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous          *)
+(*  Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA   *)
+(*  KTF funding, and donations from Arm.  This project has received         *)
+(*  funding from the European Research Council (ERC) under the European     *)
+(*  Union’s Horizon 2020 research and innovation programme (grant           *)
+(*  agreement No 789108, ELVER).                                            *)
+(*                                                                          *)
+(*  This software was developed by SRI International and the University of  *)
+(*  Cambridge Computer Laboratory (Department of Computer Science and       *)
+(*  Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV")        *)
+(*  and FA8750-10-C-0237 ("CTSRD").                                         *)
+(*                                                                          *)
+(*  SPDX-License-Identifier: BSD-2-Clause                                   *)
+(****************************************************************************)
+
+open Ast
+
+type ('a, 'b) lazy_def = Strict_def of ('a, 'b) def | Lazy_fundef of id * ('a, 'b) def Lazy.t
+
+val force_lazy_def : ('a, 'b) lazy_def -> ('a, 'b) def
+
+type ('a, 'b) ast = { defs : ('a, 'b) def list; comments : (string * Lexer.comment list) list }
+
+type ('a, 'b) lazy_ast = { lazy_defs : ('a, 'b) lazy_def list; comments : (string * Lexer.comment list) list }
+
+val force_lazy_ast : ('a, 'b) lazy_ast -> ('a, 'b) ast
+
+val empty_ast : ('a, 'b) ast

src/lib/type_check.ml

@@ -1279,6 +1279,8 @@ type tannot = tannot' option * uannot
 
 type typed_def = (tannot, env) def
 type typed_ast = (tannot, env) ast
+type typed_lazy_def = (tannot, env) lazy_def
+type typed_lazy_ast = (tannot, env) lazy_ast
 
 let untyped_annot tannot = snd tannot
 
@@ -4454,7 +4456,7 @@ let check_funcls_complete l env funcls typ =
 
 let empty_tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)
 
-let check_fundef env def_annot (FD_aux (FD_function (recopt, tannot_opt, funcls), (l, _))) =
+let check_fundef_lazy env def_annot (FD_aux (FD_function (recopt, tannot_opt, funcls), (l, _))) =
   let id =
     match
       List.fold_right
@@ -4542,20 +4544,27 @@ let check_fundef env def_annot (FD_aux (FD_function (recopt, tannot_opt, funcls)
       ([synthesize_val_spec env id quant typ def_annot], Env.add_val_spec id (quant, typ) env)
     else ([], env)
   in
-  let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in
-  let funcls, update_attr =
-    if
-      Option.is_some (get_def_attribute "complete" def_annot)
-      || Option.is_some (get_def_attribute "incomplete" def_annot)
-    then (funcls, fun attrs -> attrs)
-    else check_funcls_complete l funcl_env funcls typ
+  (* For performance, we can lazily check the body if we need it later *)
+  let check_body =
+    lazy
+      (let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in
+       let funcls, update_attr =
+         if
+           Option.is_some (get_def_attribute "complete" def_annot)
+           || Option.is_some (get_def_attribute "incomplete" def_annot)
+         then (funcls, fun attrs -> attrs)
+         else check_funcls_complete l funcl_env funcls typ
+       in
+       let def_annot = fix_body_visibility (update_attr def_annot) in
+       DEF_aux (DEF_fundef (FD_aux (FD_function (recopt, empty_tannot_opt, funcls), (l, empty_tannot))), def_annot)
+      )
   in
-  let def_annot = fix_body_visibility (update_attr def_annot) in
   let env = Env.define_val_spec id env in
-  ( vs_def
-    @ [DEF_aux (DEF_fundef (FD_aux (FD_function (recopt, empty_tannot_opt, funcls), (l, empty_tannot))), def_annot)],
-    env
-  )
+  (vs_def, id, check_body, env)
+
+let check_fundef env def_annot fdef =
+  let vs_def, _, check_body, env = check_fundef_lazy env def_annot fdef in
+  (vs_def @ [Lazy.force check_body], env)
 
 let check_mapdef env def_annot (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l, _))) =
   typ_print (lazy ("\nChecking mapping " ^ string_of_id id));
@@ -5121,8 +5130,19 @@ and check_def : Env.t -> untyped_def -> typed_def list * Env.t =
       (* These will be checked during the move_loop_measures rewrite *)
       ([DEF_aux (DEF_loop_measures (id, measures), def_annot)], env)
 
-and check_defs_progress : int -> int -> Env.t -> untyped_def list -> typed_def list * Env.t =
- fun n total env defs ->
+and check_def_lazy env def =
+  match def with
+  | DEF_aux (DEF_fundef fdef, def_annot) ->
+      let def_annot = def_annot_map_env (fun _ -> env) def_annot in
+      let vs_def, id, check_body, env = check_fundef_lazy env def_annot fdef in
+      (List.map (fun def -> Strict_def def) vs_def @ [Lazy_fundef (id, check_body)], env)
+  | _ ->
+      let defs, env = check_def env def in
+      (List.map (fun def -> Strict_def def) defs, env)
+
+and check_defs_progress :
+      'a. (Env.t -> untyped_def -> 'a list * Env.t) -> int -> int -> Env.t -> untyped_def list -> 'a list * Env.t =
+ fun checker n total env defs ->
   let rec aux n total acc env defs =
     match defs with
     | [] -> (List.rev acc, env)
@@ -5142,9 +5162,9 @@ and check_defs_progress : int -> int -> Env.t -> untyped_def list -> typed_def l
         let def, env =
           match get_def_attribute "fix_location" def_annot with
           | Some (fix_l, _) -> (
-              try check_def env def with Type_error (_, err) -> typ_raise fix_l err
+              try checker env def with Type_error (_, err) -> typ_raise fix_l err
             )
-          | None -> check_def env def
+          | None -> checker env def
         in
         aux (n + 1) total (List.rev def @ acc) (restore env) defs
   in
@@ -5153,14 +5173,20 @@ and check_defs_progress : int -> int -> Env.t -> untyped_def list -> typed_def l
 and check_defs : Env.t -> untyped_def list -> typed_def list * Env.t =
  fun env defs ->
   let total = List.length defs in
-  check_defs_progress 1 total env defs
+  check_defs_progress check_def 1 total env defs
 
 let check : Env.t -> untyped_ast -> typed_ast * Env.t =
  fun env ast ->
   let total = List.length ast.defs in
-  let defs, env = check_defs_progress 1 total env ast.defs in
+  let defs, env = check_defs_progress check_def 1 total env ast.defs in
   ({ ast with defs }, env)
 
+let check_lazy : Env.t -> untyped_ast -> typed_lazy_ast * Env.t =
+ fun env ast ->
+  let total = List.length ast.defs in
+  let defs, env = check_defs_progress check_def_lazy 1 total env ast.defs in
+  ({ lazy_defs = defs; comments = ast.comments }, Env.open_all_modules env)
+
 let rec check_with_envs : Env.t -> untyped_def list -> (typed_def list * Env.t) list =
  fun env defs ->
   match defs with

src/lib/type_check.mli

@@ -258,8 +258,12 @@ type tannot
 (** Aliases for typed definitions and ASTs for readability *)
 type typed_def = (tannot, env) def
 
+type typed_lazy_def = (tannot, env) lazy_def
+
 type typed_ast = (tannot, env) ast
 
+type typed_lazy_ast = (tannot, env) lazy_ast
+
 (** The canonical view of a type annotation is that it is a tuple
    containing an environment (env), a type (typ), such that check_X
    env (strip_X X) typ succeeds, where X is typically exp (i.e an
@@ -489,6 +493,8 @@ Some invariants that will hold of a fully checked AST are:
    Type_error.check *)
 val check : Env.t -> untyped_ast -> typed_ast * Env.t
 
+val check_lazy : Env.t -> untyped_ast -> typed_lazy_ast * Env.t
+
 val check_defs : Env.t -> untyped_def list -> typed_def list * Env.t
 
 (** The same as [check], but exposes the intermediate type-checking