From 420f16a3e2bb756c5ed282e0f3522225c44ff544 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Mon, 23 Sep 2024 10:25:56 +0100 Subject: [PATCH] create target and files for lean backend --- dune-project | 7 + sail.opam | 1 + sail_lean_backend.opam | 42 ++++++ src/sail_lean_backend/dune | 20 +++ src/sail_lean_backend/sail_plugin_lean.ml | 154 ++++++++++++++++++++++ 5 files changed, 224 insertions(+) create mode 100644 sail_lean_backend.opam create mode 100644 src/sail_lean_backend/dune create mode 100644 src/sail_lean_backend/sail_plugin_lean.ml diff --git a/dune-project b/dune-project index cff2f951e..c81429af9 100644 --- a/dune-project +++ b/dune-project @@ -98,6 +98,12 @@ http://www.cl.cam.ac.uk/~pes20/sail/. (depends (libsail (= :version)))) +(package + (name sail_lean_backend) + (synopsis "Sail to Lean translation") + (depends + (libsail (= :version)))) + (package (name sail_output) (synopsis "Example Sail output plugin") @@ -141,6 +147,7 @@ http://www.cl.cam.ac.uk/~pes20/sail/. (sail_sv_backend (and (= :version) :post)) (sail_lem_backend (and (= :version) :post)) (sail_coq_backend (and (= :version) :post)) + (sail_lean_backend (and (= :version) :post)) (sail_latex_backend (and (= :version) :post)) (sail_doc_backend (and (= :version) :post)) (sail_output (and (= :version) :post)) diff --git a/sail.opam b/sail.opam index 36327ab08..ca57626a1 100644 --- a/sail.opam +++ b/sail.opam @@ -39,6 +39,7 @@ depends: [ "sail_sv_backend" {= version & post} "sail_lem_backend" {= version & post} "sail_coq_backend" {= version & post} + "sail_lean_backend" {= version & post} "sail_latex_backend" {= version & post} "sail_doc_backend" {= version & post} "sail_output" {= version & post} diff --git a/sail_lean_backend.opam b/sail_lean_backend.opam new file mode 100644 index 000000000..6507ee4d9 --- /dev/null +++ b/sail_lean_backend.opam @@ -0,0 +1,42 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "0.18" +synopsis: "Sail to Lean translation" +maintainer: ["Sail Devs "] +authors: [ + "Alasdair Armstrong" + "Thomas Bauereiss" + "Brian Campbell" + "Shaked Flur" + "Jonathan French" + "Kathy Gray" + "Robert Norton" + "Christopher Pulte" + "Peter Sewell" + "Mark Wassell" +] +license: "BSD-2-Clause" +homepage: "https://github.com/rems-project/sail" +bug-reports: "https://github.com/rems-project/sail/issues" +depends: [ + "dune" {>= "3.0"} + "libsail" {= version} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "--promote-install-files=false" + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] + ["dune" "install" "-p" name "--create-install-files" name] +] +dev-repo: "git+https://github.com/rems-project/sail.git" diff --git a/src/sail_lean_backend/dune b/src/sail_lean_backend/dune new file mode 100644 index 000000000..fbd1c131b --- /dev/null +++ b/src/sail_lean_backend/dune @@ -0,0 +1,20 @@ +(env + (dev + (flags + (:standard -w -33 -w -27 -w -32 -w -26 -w -37))) + (release + (flags + (:standard -w -33 -w -27 -w -32 -w -26 -w -37)))) + +(executable + (name sail_plugin_lean) + (modes + (native plugin)) + (libraries libsail)) + +(install + (section + (site + (libsail plugins))) + (package sail_lean_backend) + (files sail_plugin_lean.cmxs)) diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml new file mode 100644 index 000000000..d32381186 --- /dev/null +++ b/src/sail_lean_backend/sail_plugin_lean.ml @@ -0,0 +1,154 @@ +(****************************************************************************) +(* 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"). *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(****************************************************************************) + +open Libsail + +open Interactive.State + +let opt_lean_output_dir : string option ref = ref None + +let lean_options = + [ + ( "-lean_output_dir", + Arg.String (fun dir -> opt_lean_output_dir := Some dir), + " set a custom directory to output generated Lean" + ); + ] + +(* TODO[javra]: Currently these are the same as the Coq rewrites, we might want to change them. *) +let lean_rewrites = + let open Rewrites in + [ + ("instantiate_outcomes", [String_arg "coq"]); + ("realize_mappings", []); + ("remove_vector_subrange_pats", []); + ("remove_duplicate_valspecs", []); + ("toplevel_string_append", []); + ("pat_string_append", []); + ("mapping_patterns", []); + ("add_unspecified_rec", []); + ("undefined", [Bool_arg true]); + ("vector_string_pats_to_bit_list", []); + ("remove_not_pats", []); + ("remove_impossible_int_cases", []); + ("tuple_assignments", []); + ("vector_concat_assignments", []); + ("simple_assignments", []); + ("remove_vector_concat", []); + ("remove_bitvector_pats", []); + ("remove_numeral_pats", []); + ("pattern_literals", [Literal_arg "lem"]); + ("guarded_pats", []); + (* ("register_ref_writes", rewrite_register_ref_writes); *) + ("nexp_ids", []); + ("split", [String_arg "execute"]); + ("minimise_recursive_functions", []); + ("remove_bitfield_records", []); + ("recheck_defs", []); + (* Put prover regstate generation after removing bitfield records, + which has to be followed by type checking *) + ("prover_regstate", [Bool_arg true]); + (* ("remove_assert", rewrite_ast_remove_assert); *) + ("move_termination_measures", []); + ("top_sort_defs", []); + ("const_prop_mutrec", [String_arg "coq"]); + ("exp_lift_assign", []); + ("early_return", []); + (* We need to do the exhaustiveness check before merging, because it may + introduce new wildcard clauses *) + ("recheck_defs", []); + ("make_cases_exhaustive", []); + (* merge funcls before adding the measure argument so that it doesn't + disappear into an internal pattern match *) + ("merge_function_clauses", []); + ("recheck_defs", []); + ("rewrite_explicit_measure", []); + ("rewrite_loops_with_escape_effect", []); + ("recheck_defs", []); + ("infer_effects", [Bool_arg true]); + ("attach_effects", []); + ("remove_blocks", []); + ("attach_effects", []); + ("letbind_effects", []); + ("remove_e_assign", []); + ("attach_effects", []); + ("internal_lets", []); + ("remove_superfluous_letbinds", []); + ("remove_superfluous_returns", []); + ("bit_lists_to_lits", []); + ("toplevel_let_patterns", []); + ("recheck_defs", []); + ("attach_effects", []); + ] + +let output files = failwith "Lean backend not yet implemented" + +let lean_target out_file { ctx; ast; effect_info; env; _ } = + let out_file = match out_file with Some f -> f | None -> "out" in + output [(out_file, ctx, effect_info, env, ast)] + +let _ = Target.register ~name:"lean" ~options:lean_options ~rewrites:lean_rewrites ~asserts_termination:true lean_target