From 6a7bab4a976ca06ebc5ae7a9f4dfd7443956bc00 Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Tue, 16 Apr 2024 13:35:44 +0100 Subject: [PATCH] Add translation start/end outcomes --- lib/concurrency_interface/translation.sail | 89 ++++++++++++++++++++++ src/lib/monad_params.ml | 6 ++ src/sail_coq_backend/pretty_print_coq.ml | 2 + src/sail_lem_backend/pretty_print_lem.ml | 2 + 4 files changed, 99 insertions(+) create mode 100644 lib/concurrency_interface/translation.sail diff --git a/lib/concurrency_interface/translation.sail b/lib/concurrency_interface/translation.sail new file mode 100644 index 000000000..276f9536e --- /dev/null +++ b/lib/concurrency_interface/translation.sail @@ -0,0 +1,89 @@ +/*==========================================================================*/ +/* 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-2024 */ +/* 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. */ +/*==========================================================================*/ + +$sail_internal + +$ifndef _CONCURRENCY_INTERFACE_TRANSLATION +$define _CONCURRENCY_INTERFACE_TRANSLATION + +$include + +outcome sail_translation_start : 'trans_start -> unit +with + 'trans_start : Type += { + impl emulator(_) = () +} + +outcome sail_translation_end : 'trans_end -> unit +with + 'trans_end : Type += { + impl emulator(_) = () +} + +$endif diff --git a/src/lib/monad_params.ml b/src/lib/monad_params.ml index 36e1fdb13..d07113869 100644 --- a/src/lib/monad_params.ml +++ b/src/lib/monad_params.ml @@ -78,6 +78,8 @@ type parameters = { pa_type : typ; tlbi_type : typ; translation_summary_type : typ; + trans_start_type : typ; + trans_end_type : typ; arch_ak_type : typ; } @@ -121,6 +123,8 @@ let find_monad_parameters type_env = let cache_op_type = extract_arg_typ "sail_cache_op" in let fault_type = extract_arg_typ "sail_take_exception" in let tlbi_type = extract_arg_typ "sail_tlbi" in + let trans_start_type = extract_arg_typ "sail_translation_start" in + let trans_end_type = extract_arg_typ "sail_translation_end" in Some { abort_type; @@ -130,5 +134,7 @@ let find_monad_parameters type_env = pa_type; tlbi_type; translation_summary_type; + trans_start_type; + trans_end_type; arch_ak_type; } diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml index 4420400df..e53962174 100644 --- a/src/sail_coq_backend/pretty_print_coq.ml +++ b/src/sail_coq_backend/pretty_print_coq.ml @@ -3630,6 +3630,8 @@ let pp_ast_coq (types_file, types_modules) (defs_file, defs_modules) type_defs_m string " Definition pa_countable : Countable pa := _.";*) string " Definition arch_ak := " ^^ pp_typ params.arch_ak_type ^^ string "."; string " Definition translation := " ^^ pp_typ params.translation_summary_type ^^ string "."; + string " Definition trans_start := " ^^ pp_typ params.trans_start_type ^^ string "."; + string " Definition trans_end := " ^^ pp_typ params.trans_end_type ^^ string "."; string " Definition abort := " ^^ pp_typ params.abort_type ^^ string "."; string " Definition barrier := " ^^ pp_typ params.barrier_type ^^ string "."; string " Definition cache_op := " ^^ pp_typ params.cache_op_type ^^ string "."; diff --git a/src/sail_lem_backend/pretty_print_lem.ml b/src/sail_lem_backend/pretty_print_lem.ml index 969382246..9a724ddf2 100644 --- a/src/sail_lem_backend/pretty_print_lem.ml +++ b/src/sail_lem_backend/pretty_print_lem.ml @@ -1831,6 +1831,8 @@ let doc_ast_lem out_filename split_files base_imports extra_imports effect_info params.pa_type; params.tlbi_type; params.translation_summary_type; + params.trans_start_type; + params.trans_end_type; params.arch_ak_type; ] in