Skip to content

Commit

Permalink
Merge branch 'sail2' into lean/typdef
Browse files Browse the repository at this point in the history
  • Loading branch information
javra authored Dec 18, 2024
2 parents fdc7669 + fd18b93 commit 788d0eb
Show file tree
Hide file tree
Showing 31 changed files with 373 additions and 188 deletions.
10 changes: 5 additions & 5 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -10,29 +10,29 @@ jobs:
strategy:
matrix:
version: [4.08.1, 5.2.1]
os: [ubuntu-latest, macOS-latest]
os: [ubuntu-latest, macos-latest]
exclude:
- os: macos-latest
version: 4.08.1

runs-on: ${{ matrix.os }}

steps:
- uses: actions/checkout@v3
- uses: actions/checkout@v4

- name: System dependencies (ubuntu)
if: startsWith(matrix.os, 'ubuntu')
run: |
sudo apt install build-essential libgmp-dev z3 cvc4 opam
- name: System dependencies (macOS)
if: startsWith(matrix.os, 'macOS')
if: startsWith(matrix.os, 'macos')
run: |
brew install --force --overwrite gpatch gmp z3 pkgconf opam
- name: Restore cached opam
id: cache-opam-restore
uses: actions/cache/restore@v3
uses: actions/cache/restore@v4
with:
path: ~/.opam
key: ${{ matrix.os }}-${{ matrix.version }}
Expand All @@ -45,7 +45,7 @@ jobs:
- name: Save cached opam
if: steps.cache-opam-restore.outputs.cache-hit != 'true'
id: cache-opam-save
uses: actions/cache/save@v3
uses: actions/cache/save@v4
with:
path: ~/.opam
key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
Expand Down
4 changes: 2 additions & 2 deletions src/bin/dune
Original file line number Diff line number Diff line change
Expand Up @@ -242,6 +242,6 @@
(%{workspace_root}/src/gen_lib/sail2_values.lem
as
src/gen_lib/sail2_values.lem)
(%{workspace_root}/src/sail_lean_backend/Sail/sail.lean
(%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean
as
src/sail_lean_backend/Sail/sail.lean)))
src/sail_lean_backend/Sail/Sail.lean)))
2 changes: 1 addition & 1 deletion src/bin/sail.ml
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ let add_target_header plugin opts =
let load_plugin opts plugin =
try
if is_bytecode then Dynlink.loadfile plugin else Dynlink.loadfile_private plugin;
let plugin_opts = Target.extract_options () |> fix_options |> target_align in
let plugin_opts = Target.extract_options () |> List.map Flag.to_arg |> fix_options |> target_align in
opts := add_target_header plugin !opts @ plugin_opts
with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg)

Expand Down
64 changes: 64 additions & 0 deletions src/lib/flag.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
(****************************************************************************)
(* 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 Arg

type t = { prefix : string list; hide_prefix : bool; debug : bool; hide : bool; arg : string option; key : string }

let create ?(prefix = []) ?(hide_prefix = false) ?(debug = false) ?(hide = false) ?arg key =
{ prefix; hide_prefix; debug; hide; arg; key }

let underscore_sep = Util.string_of_list "_" (fun s -> s)

let to_arg (flag, spec, doc) =
let apply_prefix key =
match flag.prefix with [] -> key | _ when flag.hide_prefix -> key | _ -> underscore_sep flag.prefix ^ "_" ^ key
in
let key =
"-" ^ if flag.key = "" then underscore_sep flag.prefix else (if flag.debug then "d" else "") ^ apply_prefix flag.key
in
let arg_prefix = match flag.arg with Some desc -> "<" ^ desc ^ "> " | None -> " " in
(key, spec, if flag.hide then "" else arg_prefix ^ (if flag.debug then "(debug) " else "") ^ doc)
51 changes: 51 additions & 0 deletions src/lib/flag.mli
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
(****************************************************************************)
(* 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 *)
(****************************************************************************)

type t

val create : ?prefix:string list -> ?hide_prefix:bool -> ?debug:bool -> ?hide:bool -> ?arg:string -> string -> t

val to_arg : t * Arg.spec * string -> Arg.key * Arg.spec * Arg.doc
6 changes: 3 additions & 3 deletions src/lib/target.ml
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ module StringMap = Map.Make (String)

type target = {
name : string;
options : (Arg.key * Arg.spec * Arg.doc) list;
options : (Flag.t * Arg.spec * string) list;
pre_parse_hook : unit -> unit;
pre_initial_check_hook : string list -> unit;
pre_rewrites_hook : typed_ast -> Effects.side_effect_info -> Env.t -> unit;
Expand Down Expand Up @@ -93,12 +93,12 @@ let register ~name ?flag ?description:desc ?(options = []) ?(pre_parse_hook = fu
prerr_endline ("Cannot use multiple Sail targets simultaneously: " ^ tgt ^ " and " ^ name);
exit 1
in
let desc = match desc with Some desc -> desc | None -> " invoke the Sail " ^ name ^ " target" in
let desc = match desc with Some desc -> desc | None -> "invoke the Sail " ^ name ^ " target" in
let flag = match flag with Some flag -> flag | None -> name in
let tgt =
{
name;
options = ("-" ^ flag, Arg.Unit set_target, desc) :: options;
options = (Flag.create ~prefix:[flag] "", Arg.Unit set_target, desc) :: options;
pre_parse_hook;
pre_initial_check_hook;
pre_rewrites_hook;
Expand Down
4 changes: 2 additions & 2 deletions src/lib/target.mli
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ val register :
name:string ->
?flag:string ->
?description:string ->
?options:(Arg.key * Arg.spec * Arg.doc) list ->
?options:(Flag.t * Arg.spec * string) list ->
?pre_parse_hook:(unit -> unit) ->
?pre_initial_check_hook:(string list -> unit) ->
?pre_rewrites_hook:(typed_ast -> Effects.side_effect_info -> Env.t -> unit) ->
Expand All @@ -130,4 +130,4 @@ val get : name:string -> target option
val extract_registered : unit -> string list

(** Used internally to dynamically update the option list when loading plugins *)
val extract_options : unit -> (Arg.key * Arg.spec * Arg.doc) list
val extract_options : unit -> (Flag.t * Arg.spec * string) list
4 changes: 3 additions & 1 deletion src/lib/type_check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4194,7 +4194,9 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, uannot)) as mpa
| _ -> Reporting.unreachable l __POS__ "unifying mapping type, expanded synonyms to non-mapping type!"
end
| MP_app (other, mpats) when Env.is_mapping other env ->
bind_mpat allow_unknown other_env env (MP_aux (MP_app (other, [mk_mpat (MP_tuple mpats)]), (l, uannot))) typ
bind_mpat allow_unknown other_env env
(MP_aux (MP_app (other, [mk_mpat ~loc:l (MP_tuple mpats)]), (l, uannot)))
typ
| MP_app (f, _) when not (Env.is_union_constructor f env || Env.is_mapping f env) ->
typ_error l (string_of_id f ^ " is not a union constructor or mapping in mapping-pattern " ^ string_of_mpat mpat)
| MP_as (mpat, id) ->
Expand Down
56 changes: 31 additions & 25 deletions src/sail_c_backend/sail_plugin_c.ml
Original file line number Diff line number Diff line change
Expand Up @@ -53,39 +53,42 @@ let opt_specialize_c = ref false

let c_options =
[
( "-c_include",
( Flag.create ~prefix:["c"] ~arg:"filename" "include",
Arg.String (fun i -> opt_includes_c := i :: !opt_includes_c),
"<filename> provide additional include for C output"
"provide additional include for C output"
);
("-c_no_main", Arg.Set C_backend.opt_no_main, " do not generate the main() function");
("-c_no_rts", Arg.Set C_backend.opt_no_rts, " do not include the Sail runtime");
( "-c_no_lib",
(Flag.create ~prefix:["c"] "no_main", Arg.Set C_backend.opt_no_main, "do not generate the main() function");
(Flag.create ~prefix:["c"] "no_rts", Arg.Set C_backend.opt_no_rts, "do not include the Sail runtime");
( Flag.create ~prefix:["c"] "no_lib",
Arg.Tuple [Arg.Set C_backend.opt_no_lib; Arg.Set C_backend.opt_no_rts],
" do not include the Sail runtime or library"
"do not include the Sail runtime or library"
);
("-c_prefix", Arg.String (fun prefix -> C_backend.opt_prefix := prefix), "<prefix> prefix generated C functions");
( "-c_extra_params",
( Flag.create ~prefix:["c"] ~arg:"prefix" "prefix",
Arg.String (fun prefix -> C_backend.opt_prefix := prefix),
"prefix generated C functions"
);
( Flag.create ~prefix:["c"] ~arg:"parameters" "extra_params",
Arg.String (fun params -> C_backend.opt_extra_params := Some params),
"<parameters> generate C functions with additional parameters"
"generate C functions with additional parameters"
);
( "-c_extra_args",
( Flag.create ~prefix:["c"] ~arg:"arguments" "extra_args",
Arg.String (fun args -> C_backend.opt_extra_arguments := Some args),
"<arguments> supply extra argument to every generated C function call"
"supply extra argument to every generated C function call"
);
("-c_specialize", Arg.Set opt_specialize_c, " specialize integer arguments in C output");
( "-c_preserve",
(Flag.create ~prefix:["c"] "specialize", Arg.Set opt_specialize_c, "specialize integer arguments in C output");
( Flag.create ~prefix:["c"] "preserve",
Arg.String (fun str -> Specialize.add_initial_calls (Ast_util.IdSet.singleton (Ast_util.mk_id str))),
" make sure the provided function identifier is preserved in C output"
"make sure the provided function identifier is preserved in C output"
);
( "-c_fold_unit",
( Flag.create ~prefix:["c"] "fold_unit",
Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str),
" remove comma separated list of functions from C output, replacing them with unit"
"remove comma separated list of functions from C output, replacing them with unit"
);
( "-c_coverage",
( Flag.create ~prefix:["c"] ~arg:"file" "coverage",
Arg.String (fun str -> C_backend.opt_branch_coverage := Some (open_out str)),
"<file> Turn on coverage tracking and output information about all branches and functions to a file"
"Turn on coverage tracking and output information about all branches and functions to a file"
);
( "-O",
( Flag.create ~prefix:["c"] ~hide_prefix:true "O",
Arg.Tuple
[
Arg.Set C_backend.optimize_primops;
Expand All @@ -94,17 +97,20 @@ let c_options =
Arg.Set C_backend.optimize_struct_updates;
Arg.Set C_backend.optimize_alias;
],
" turn on optimizations for C compilation"
"turn on optimizations for C compilation"
);
( "-Ofixed_int",
( Flag.create ~prefix:["c"] ~hide_prefix:true "Ofixed_int",
Arg.Set C_backend.optimize_fixed_int,
" assume fixed size integers rather than GMP arbitrary precision integers"
"assume fixed size integers rather than GMP arbitrary precision integers"
);
( "-Ofixed_bits",
( Flag.create ~prefix:["c"] ~hide_prefix:true "Ofixed_bits",
Arg.Set C_backend.optimize_fixed_bits,
" assume fixed size bitvectors rather than arbitrary precision bitvectors"
"assume fixed size bitvectors rather than arbitrary precision bitvectors"
);
( Flag.create ~prefix:["c"] ~hide_prefix:true "static",
Arg.Set C_backend.opt_static,
"make generated C functions static"
);
("-static", Arg.Set C_backend.opt_static, " make generated C functions static");
]

let c_rewrites =
Expand Down
Loading

0 comments on commit 788d0eb

Please sign in to comment.