Add lem stubs for softfloat externs.rsnikhil

2 files changed, 218 insertions, 0 deletions

diff --git a/handwritten_support/0.11/riscv_extras_fdext.lem b/handwritten_support/0.11/riscv_extras_fdext.lem
new file mode 100644
index 0000000..3c79089
--- /dev/null
+++ b/handwritten_support/0.11/riscv_extras_fdext.lem
@@ -0,0 +1,109 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_mwords
+open import Sail2_prompt_monad
+open import Sail2_prompt
+
+type bitvector 'a = mword 'a
+
+(* stub functions emulating the C softfloat interface *)
+
+val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_add _ _ _ = ()
+
+val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_sub _ _ _ = ()
+
+val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_mul _ _ _ = ()
+
+val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_div _ _ _ = ()
+
+val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_add _ _ _ = ()
+
+val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_sub _ _ _ = ()
+
+val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_mul _ _ _ = ()
+
+val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_div _ _ _ = ()
+
+
+val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_muladd _ _ _ _ = ()
+
+val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_muladd _ _ _ _ = ()
+
+
+val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_sqrt _ _ = ()
+
+val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_sqrt _ _ = ()
+
+
+val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_i32 _ _ = ()
+
+val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f32 _ _ = ()
+
+val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f32 _ _ = ()
+
+val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_i64 _ _ = ()
+
+val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f32 _ _ = ()
+
+val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f32 _ _ = ()
+
+
+val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_i32 _ _ = ()
+
+val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f64 _ _ = ()
+
+val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f64 _ _ = ()
+
+val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_i64 _ _ = ()
+
+val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f64 _ _ = ()
+
+val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f64 _ _ = ()
+
+
+val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_f64 _ _ = ()
+
+val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_f32 _ _ = ()
+
+
+
diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem
new file mode 100644
index 0000000..3c79089
--- /dev/null
+++ b/handwritten_support/riscv_extras_fdext.lem
@@ -0,0 +1,109 @@
+open import Pervasives
+open import Pervasives_extra
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_mwords
+open import Sail2_prompt_monad
+open import Sail2_prompt
+
+type bitvector 'a = mword 'a
+
+(* stub functions emulating the C softfloat interface *)
+
+val softfloat_f32_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_add _ _ _ = ()
+
+val softfloat_f32_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_sub _ _ _ = ()
+
+val softfloat_f32_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_mul _ _ _ = ()
+
+val softfloat_f32_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_div _ _ _ = ()
+
+val softfloat_f64_add : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_add _ _ _ = ()
+
+val softfloat_f64_sub : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_sub _ _ _ = ()
+
+val softfloat_f64_mul : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_mul _ _ _ = ()
+
+val softfloat_f64_div : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_div _ _ _ = ()
+
+
+val softfloat_f32_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f32_muladd _ _ _ _ = ()
+
+val softfloat_f64_muladd : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> bitvector 's -> bitvector 's -> unit
+let softfloat_f64_muladd _ _ _ _ = ()
+
+
+val softfloat_f32_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_sqrt _ _ = ()
+
+val softfloat_f64_sqrt : forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_sqrt _ _ = ()
+
+
+val softfloat_f32_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_i32 _ _ = ()
+
+val softfloat_f32_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f32 _ _ = ()
+
+val softfloat_ui32_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f32 _ _ = ()
+
+val softfloat_f32_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_i64 _ _ = ()
+
+val softfloat_f32_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f32 _ _ = ()
+
+val softfloat_ui64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f32 _ _ = ()
+
+
+val softfloat_f64_to_i32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_i32 _ _ = ()
+
+val softfloat_f64_to_ui32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_ui32 _ _ = ()
+
+val softfloat_i32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i32_to_f64 _ _ = ()
+
+val softfloat_ui32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui32_to_f64 _ _ = ()
+
+val softfloat_f64_to_i64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_i64 _ _ = ()
+
+val softfloat_f64_to_ui64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_ui64 _ _ = ()
+
+val softfloat_i64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_i64_to_f64 _ _ = ()
+
+val softfloat_ui64_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_ui64_to_f64 _ _ = ()
+
+
+val softfloat_f32_to_f64: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f32_to_f64 _ _ = ()
+
+val softfloat_f64_to_f32: forall 'rm 's. Size 'rm, Size 's => bitvector 'rm -> bitvector 's -> unit
+let softfloat_f64_to_f32 _ _ = ()
+
+
+