Skip to content

Commit

Permalink
Add translation start/end outcomes
Browse files Browse the repository at this point in the history
  • Loading branch information
@bauereiss
bauereiss committed Apr 25, 2024
1 parent 4cdda5d commit 6a7bab4
Show file tree
Hide file tree
Showing 4 changed files with 99 additions and 0 deletions.
89 changes: 89 additions & 0 deletions lib/concurrency_interface/translation.sail
View file
Original file line number Diff line number Diff line change
@@ -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 <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"). */
/* */
/* 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 <concurrency_interface/common.sail>

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
6 changes: 6 additions & 0 deletions src/lib/monad_params.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down Expand Up @@ -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;
Expand All @@ -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;
}
2 changes: 2 additions & 0 deletions src/sail_coq_backend/pretty_print_coq.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 ".";
Expand Down
2 changes: 2 additions & 0 deletions src/sail_lem_backend/pretty_print_lem.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 6a7bab4

Please sign in to comment.