Library ArchSemArm.ArmInst
From SailStdpp Require Import -(notations) Base ConcurrencyInterfaceTypes.
From SailTinyArm Require Export System_types.
From SailTinyArm Require Import System.
From ASCommon Require Import Options.
From ASCommon Require Import Common Effects.
From ArchSem Require Import
Interface TermModels CandidateExecutions GenPromising SeqModel ArchInst.
From ArchSem Require Export FromSail.
Module SA := System_types.Arch.
Module SI := System_types.Interface.
There a few missing definition that are not generated by Sail
Module ArchExtra <: FromSail.ArchExtra SA.
Import SA.
Definition pc_reg : reg := _PC.
Definition reg_of_string := register_of_string.
Equations reg_type_of_gen (r : reg) (rv : reg_gen_val) :
result string (reg_type r) :=
reg_type_of_gen (R_bitvector_1 _) (RVNumber z) := Ok (Z_to_bv 1 z);
reg_type_of_gen (R_bitvector_2 _) (RVNumber z) := Ok (Z_to_bv 2 z);
reg_type_of_gen (R_bitvector_4 _) (RVNumber z) := Ok (Z_to_bv 4 z);
reg_type_of_gen (R_bitvector_64 _) (RVNumber z) := Ok (Z_to_bv 64 z);
reg_type_of_gen r _ := Error ("Error decoding " ++ pretty r)%string.
Equations reg_type_to_gen (r : reg) (rv : reg_type r) : reg_gen_val :=
reg_type_to_gen (R_bitvector_1 _) bv := RVNumber (bv_unsigned bv);
reg_type_to_gen (R_bitvector_2 _) bv := RVNumber (bv_unsigned bv);
reg_type_to_gen (R_bitvector_4 _) bv := RVNumber (bv_unsigned bv);
reg_type_to_gen (R_bitvector_64 _) bv := RVNumber (bv_unsigned bv).
End ArchExtra.
Import SA.
Definition pc_reg : reg := _PC.
Definition reg_of_string := register_of_string.
Equations reg_type_of_gen (r : reg) (rv : reg_gen_val) :
result string (reg_type r) :=
reg_type_of_gen (R_bitvector_1 _) (RVNumber z) := Ok (Z_to_bv 1 z);
reg_type_of_gen (R_bitvector_2 _) (RVNumber z) := Ok (Z_to_bv 2 z);
reg_type_of_gen (R_bitvector_4 _) (RVNumber z) := Ok (Z_to_bv 4 z);
reg_type_of_gen (R_bitvector_64 _) (RVNumber z) := Ok (Z_to_bv 64 z);
reg_type_of_gen r _ := Error ("Error decoding " ++ pretty r)%string.
Equations reg_type_to_gen (r : reg) (rv : reg_type r) : reg_gen_val :=
reg_type_to_gen (R_bitvector_1 _) bv := RVNumber (bv_unsigned bv);
reg_type_to_gen (R_bitvector_2 _) bv := RVNumber (bv_unsigned bv);
reg_type_to_gen (R_bitvector_4 _) bv := RVNumber (bv_unsigned bv);
reg_type_to_gen (R_bitvector_64 _) bv := RVNumber (bv_unsigned bv).
End ArchExtra.
Then we can use this to generate an ArchSem architecture module
Module Arch := ArchFromSail SA ArchExtra.
Module NoCHERI.
Definition no_cheri : ¬ Arch.CHERI := ltac:(naive_solver).
End NoCHERI.
Module NoCHERI.
Definition no_cheri : ¬ Arch.CHERI := ltac:(naive_solver).
End NoCHERI.
This instantiates all ArchSem arch-generic code, for Arm
Module Arm := ArchInst.ArchInst Arch NoCHERI.
Module IMonFromSail := IMonFromSail SA SI ArchExtra Arch Arm.Interface.
Export Arch.
Export Arm.
Export Arm.Interface.
Export Arm.TM.
Export Arm.Cand.
Export Arm.GenPro.
Export Arm.SeqModel.
Export Arm.ISAManip.
Export IMonFromSail.
Module IMonFromSail := IMonFromSail SA SI ArchExtra Arch Arm.Interface.
Export Arch.
Export Arm.
Export Arm.Interface.
Export Arm.TM.
Export Arm.Cand.
Export Arm.GenPro.
Export Arm.SeqModel.
Export Arm.ISAManip.
Export IMonFromSail.
Make type abbreviations transparent
#[export] Typeclasses Transparent bits.
#[export] Typeclasses Transparent SA.addr_size.
#[export] Typeclasses Transparent System_types.addr_space.
#[export] Typeclasses Transparent SA.addr_space.
#[export] Typeclasses Transparent SA.sys_reg_id.
#[export] Typeclasses Transparent SA.mem_acc.
#[export] Typeclasses Transparent SA.abort.
#[export] Typeclasses Transparent SA.barrier.
#[export] Typeclasses Transparent SA.cache_op.
#[export] Typeclasses Transparent SA.tlbi.
#[export] Typeclasses Transparent SA.exn.
#[export] Typeclasses Transparent SA.trans_start.
#[export] Typeclasses Transparent SA.trans_end.
#[export] Typeclasses Transparent SA.addr_size.
#[export] Typeclasses Transparent System_types.addr_space.
#[export] Typeclasses Transparent SA.addr_space.
#[export] Typeclasses Transparent SA.sys_reg_id.
#[export] Typeclasses Transparent SA.mem_acc.
#[export] Typeclasses Transparent SA.abort.
#[export] Typeclasses Transparent SA.barrier.
#[export] Typeclasses Transparent SA.cache_op.
#[export] Typeclasses Transparent SA.tlbi.
#[export] Typeclasses Transparent SA.exn.
#[export] Typeclasses Transparent SA.trans_start.
#[export] Typeclasses Transparent SA.trans_end.
Since ArchSem only uses register types through reg_type, there is no need
for those slow and risky instances
#[export] Remove Hints
Decidable_eq_register_values
Inhabited_register_values
Countable_register_values
: typeclass_instances.
Decidable_eq_register_values
Inhabited_register_values
Countable_register_values
: typeclass_instances.
The semantics of instructions from system sail-tiny-arm by using the
conversion code from ArchSem.FromSail
Definition sail_tiny_arm_sem (nondet : bool) : iMon () :=
iMon_from_Sail nondet (System.fetch_and_execute ()).
iMon_from_Sail nondet (System.fetch_and_execute ()).