Add library to run models from Ocaml

ArchSem/FromSail.v

@@ -88,6 +88,9 @@ Module Type ArchExtra (SA : SailArch).
   Import SA.
 
   Parameter pc_reg : reg.
+  Parameter reg_of_string : string → option reg.
+  Parameter reg_type_of_gen : ∀ r : reg, reg_gen_val → result string (reg_type r).
+  Parameter reg_type_to_gen : ∀ r : reg, reg_type r → reg_gen_val.
 End ArchExtra.
 
 (** * Convert from Sail generated instantiations to ArchSem ones *)
@@ -101,8 +104,9 @@ Module ArchFromSail (SA : SailArch) (AE : ArchExtra SA) <: Arch.
   Definition reg_countable : Countable reg := SA.reg_countable.
   #[export] Typeclasses Transparent reg_countable.
   Definition pretty_reg : Pretty reg := SA.reg_pretty.
-  #[export] Typeclasses Transparent reg_countable.
-
+  #[export] Typeclasses Transparent pretty_reg.
+  Definition reg_of_string := AE.reg_of_string.
+  #[export] Typeclasses Transparent reg_of_string.
 
   Definition pc_reg := AE.pc_reg.
   #[export] Typeclasses Transparent pc_reg.
@@ -126,6 +130,11 @@ Module ArchFromSail (SA : SailArch) (AE : ArchExtra SA) <: Arch.
       abstract (dependent destruction Heq; simp ctrans in *; by rewrite JMeq_simpl).
   Defined.
 
+  Definition reg_type_of_gen := AE.reg_type_of_gen.
+  #[export] Typeclasses Transparent reg_type_of_gen.
+  Definition reg_type_to_gen := AE.reg_type_to_gen.
+  #[export] Typeclasses Transparent reg_type_to_gen.
+
   (* TODO get sail to generate reg_acc *)
   Definition reg_acc := option SA.sys_reg_id.
   #[export] Typeclasses Transparent reg_acc.

ArchSem/Interface.v

@@ -45,6 +45,17 @@
 From ASCommon Require Import Options.
 From ASCommon Require Import Common FMon.
 
+(** * Generic register management
+
+    This type allows to parse and print register states in a generic manner *)
+
+Inductive reg_gen_val :=
+| RVNumber (z : Z)
+| RVString (s : string)
+| RVArray (l : list reg_gen_val)
+| RVStruct (l : list (string * reg_gen_val)).
+
+
 (** * The architecture requirements
 
 The SailStdpp library already defines the architecure requirements, however this
@@ -61,6 +72,8 @@ Module Type Arch.
   #[export] Existing Instance reg_countable.
   Parameter pretty_reg : Pretty reg.
   #[export] Existing Instance pretty_reg.
+  Parameter reg_of_string : string → option reg.
+
 
   (** Register value type are dependent on the register, therefore we need all
       the dependent type manipulation typeclasses *)
@@ -77,6 +90,9 @@ Module Type Arch.
   #[export] Existing Instance ctrans_reg_type_simpl.
   Parameter reg_type_eq_dep_dec : EqDepDecision reg_type.
   #[export] Existing Instance reg_type_eq_dep_dec.
+  Parameter reg_type_of_gen : ∀ r : reg, reg_gen_val → result string (reg_type r).
+  Parameter reg_type_to_gen : ∀ r : reg, reg_type r → reg_gen_val.
+
 
 
   (** Register access kind (architecture specific) *)

ArchSemArm/ArmInst.v

@@ -64,6 +64,31 @@ Module Arm.
     Import SA.
 
     Definition pc_reg : reg := _PC.
+    Definition reg_of_string := register_of_string.
+
+    Equations set_ProcState_gen_field (field : string) (val : reg_gen_val)
+        (p : ProcState) : result string ProcState :=
+      set_ProcState_gen_field "EL" (RVNumber z) p :=
+        Ok $ setv ProcState_EL (Z_to_bv 2 z) p;
+      set_ProcState_gen_field "SP" (RVNumber z) p :=
+        Ok $ setv ProcState_SP (Z_to_bv 1 z) p;
+      set_ProcState_gen_field field _ _ :=
+        Error ("error setting " ++ field ++ " in PSTATE")%string.
+
+    Equations reg_type_of_gen (r : reg) (rv : reg_gen_val) :
+        result string (reg_type r) :=
+      reg_type_of_gen (R_bitvector_64 _) (RVNumber z) := Ok (Z_to_bv 64 z);
+      reg_type_of_gen (R_ProcState _) (RVStruct l) :=
+        foldlM (λ ps '(field, val), set_ProcState_gen_field field val ps) inhabitant l;
+      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_64 _) bv := RVNumber (bv_unsigned bv);
+      reg_type_to_gen (R_ProcState _) ps :=
+        RVStruct [
+            ("EL", RVNumber (bv_unsigned (ProcState_EL ps)));
+            ("SP", RVNumber (bv_unsigned (ProcState_SP ps)));
+            ("TODO", RVString "other fields")].
   End ArchExtra.
 
   (** Then we can use this to generate an ArchSem architecture module *)

ArchSemRiscV/RiscVInst.v

@@ -64,6 +64,15 @@ Module RiscV.
     Import SA.
 
     Definition pc_reg : reg := PC.
+    Definition reg_of_string := register_of_string.
+
+    Definition reg_type_of_gen (r : reg) (rv : reg_gen_val) :
+      result string (reg_type r).
+      (* Only used in extraction for now, should be generated by Sail soon *)
+    Admitted.
+
+    Definition reg_type_to_gen (r : reg) (rv : reg_type r) : reg_gen_val.
+    Admitted.
   End ArchExtra.
 
   (** Then we can use this to generate an ArchSem architecture module *)

Common/CArith.v

@@ -183,6 +183,11 @@ Proof. tcclean. apply Nat2N.inj_mod. Qed.
 
 
 
+(** * fin utils *)
+
+Definition fin0_magic {A} : fin 0 → A :=
+  λ 'f, match f with end.
+
 
 (** * FinUnfold
 

Common/CExtraction.v

@@ -43,16 +43,69 @@
 (******************************************************************************)
 
 From Stdlib Require Import ZArith.
+From Stdlib Require Import Extraction.
+
 Require Import Options.
-Require Import CBase.
+Require Import Common.
+
 
-From Stdlib Require Import Extraction.
+
+(** * Base defaults *)
 
 From Stdlib Require Import ExtrOcamlBasic.
 From Stdlib Require Import ExtrOcamlNativeString.
 From Stdlib Require Import ExtrOcamlZBigInt.
 From Stdlib Require Import ExtrOcamlNatBigInt.
 
+(* Extract Constant BinNums.PosDef.Pos.add => "Big_int_Z.add_big_int". *)
+
+Extract Inlined Constant map => "Stdlib.List.map".
+
 Extraction Blacklist String.
+Extraction Blacklist List.
+
+Extract Inlined Constant Decision => "bool".
+
+Extract Inductive fin => "ZO.t"
+  [ "ZO.zero" "ZO.succ" ]
+  "(fun _fO _fS _n -> garbage___garbage)".
+
+Extraction Implicit Fin.F1 [n].
+Extraction Implicit Fin.FS [n].
+
+Extraction Implicit fin_dec [n].
+Extract Constant fin_dec => "ZO.equal".
+
+Extraction Implicit fin_to_nat [n].
+Extract Inlined Constant fin_to_nat => "(fun x -> x)".
+
+Extract Inlined Constant fin0_magic => "Support.fin0_magic".
+
+(** * Vector
+
+Extracted as lists for now *)
+
+Extract Inductive vec => list [ "[]" "( :: )" ].
+Extraction Implicit vcons [A n].
+Extraction Implicit vmap [A B n].
+Extract Inlined Constant vmap => "List.map".
+Extract Inlined Constant list_to_vec  => "(fun x -> x)".
+
+
+Extraction Implicit vector_lookup_total [A m].
+Extract Inlined Constant vector_lookup_total => "Support.list_get".
+
+Extraction Implicit vinsert [A n].
+Extract Inlined Constant vinsert => "Support.list_set".
+
+(** * Result *)
+
+(* Extract Inductive result => result [ "Ok" "Error"]. *)
+
+(** * CTrans
+
+Extract transport to identity function *)
+
+
 Extract Inlined Constant ctrans => "(fun x -> x)".
 Extraction Implicit ctrans [CTrans x y].

Common/Effects.v

@@ -50,7 +50,7 @@ From stdpp Require Import vector.
 From stdpp Require Import finite.
 
 Require Import Options.
-Require Import CBase CBool CDestruct.
+Require Import CBase CBool CDestruct CArith.
 
 (** * Base effect definitions *)
 
@@ -239,7 +239,7 @@ Proof. solve_decision. Defined.
 Notation MChoose := (@MCall MChoice MChoice_ret).
 Definition mchoose `{!MChoose M} (n : nat) : M (fin n) := mcall (ChooseFin n).
 Definition mdiscard `{MChoose M, FMap M} {A} : M A :=
-  mcall (ChooseFin 0) |$> (λ x, match (x : fin 0) with end).
+  mcall (ChooseFin 0) |$> fin0_magic.
 
 (** Helper to non-deterministically choose in a list *)
 Definition mchoosel `{MChoose M, FMap M} {A} (l : list A) : M A :=

Extraction/ArmInstExtr.v

@@ -1,11 +1,17 @@
 Require Import ASCommon.CExtraction.
-Require Import ArchSemArm.ArmInst.
+From ArchSemArm Require Import ArmInst UMPromising VMPromising.
 
 Unset Extraction SafeImplicits.
 
+Extract Inductive ArchSem.Interface.reg_gen_val =>
+  "Reggenval.gen"
+  ["Reggenval.Number" "Reggenval.String" "Reggenval.Array" "Reggenval.Struct"].
+
 (* DO NOT run this file in your editor. This will extract in the correct folder
    when dune does the extraction *)
 Set Extraction Output Directory ".".
 
-#[warnings="-extraction-remaining-implicit"]
-Separate Extraction sequential_modelc.
+(* Definition umProm_cert_c := UMPromising_cert_c. *)
+
+#[warnings="-extraction-remaining-implicit,-extraction-reserved-identifier"]
+Separate Extraction sequential_modelc sail_tiny_arm_sem Arm UMPromising_cert_c.

Extraction/ZO.ml

@@ -0,0 +1,2 @@
+(* Proxy to access ZArith module from coq extracted code *)
+include Z