From f69418a29ce66a0be9eed40d83482113821adef1 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 8 Oct 2024 13:25:01 +0100 Subject: [PATCH] Add lazy API to type-checker (#738) Update generated opam files --- sail_smt_backend.opam | 2 +- src/lib/ast_defs.ml | 8 ++++++ src/lib/ast_defs.mli | 59 ++++++++++++++++++++++++++++++++++++++ src/lib/type_check.ml | 64 +++++++++++++++++++++++++++++------------- src/lib/type_check.mli | 6 ++++ 5 files changed, 119 insertions(+), 20 deletions(-) create mode 100644 src/lib/ast_defs.mli diff --git a/sail_smt_backend.opam b/sail_smt_backend.opam index 6ae4f77e4..89689e6a9 100644 --- a/sail_smt_backend.opam +++ b/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 "] authors: [ "Alasdair Armstrong" diff --git a/src/lib/ast_defs.ml b/src/lib/ast_defs.ml index 69c0d79e2..f25033ecb 100644 --- a/src/lib/ast_defs.ml +++ b/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 = [] } diff --git a/src/lib/ast_defs.mli b/src/lib/ast_defs.mli new file mode 100644 index 000000000..42ebce92c --- /dev/null +++ b/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 REMS: Rigorous *) +(* Engineering for Mainstream Systems, 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 diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index aee1a47c8..d3e05f4a4 100644 --- a/src/lib/type_check.ml +++ b/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 diff --git a/src/lib/type_check.mli b/src/lib/type_check.mli index ecfa9285e..b3ef86687 100644 --- a/src/lib/type_check.mli +++ b/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