Try and define a translation from RTL to SRTL

6 files changed, 78 insertions, 9 deletions

diff --git a/Makefile b/Makefile
index 218598a..da15a06 100644
--- a/Makefile
+++ b/Makefile
@@ -1,3 +1,6 @@
+LIBRARY_SUPERBLOCK ?= no
+PREFIX ?= .
+
 UNAME_S := $(shell uname -s)
 ifeq ($(UNAME_S),Linux)
 	ARCH := verilog-linux
@@ -23,14 +26,23 @@ COQDOCFLAGS := --no-lib-name -l
 
 VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls bourdoncle, src/$(d)/*.v)
 
-PREFIX ?= .
+STAMPS := lib/COMPCERTSTAMP
 
-.PHONY: all install proof clean extraction test
+ifneq ($(LIBRARY_SUPERBLOCK), no)
+VS += $(wildcard src/superblock/*.v)
+COQINCLUDES += -R lib/compcert-kvx kvx -R lib/compcert-kvx/flocq kvx.Flocq
+STAMPS += lib/COMPCERTKVXSTAMP
+endif
+
+.PHONY: all install proof clean extraction test force
 
-all: lib/COMPCERTSTAMP
+all: $(STAMPS)
 	$(MAKE) proof
 	$(MAKE) compile
 
+lib/CompCert/configure:
+	git submodule update --init lib/CompCert
+
 lib/CompCert/Makefile.config: lib/CompCert/configure
 	(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
 
@@ -38,6 +50,16 @@ lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
 	$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert
 	touch $@
 
+lib/compcert-kvx/configure:
+	git submodule update --init lib/compcert-kvx
+
+lib/CompCert/Makefile.config: lib/compcert-kvx/configure
+	(cd lib/compcert-kvx && ./configure --ignore-coq-version $(ARCH))
+
+lib/COMPCERTKVXSTAMP: lib/compcert-kvx/Makefile.config
+	$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/compcert-kvx
+	touch $@
+
 install:
 	install -d $(PREFIX)/bin
 	sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
@@ -71,10 +93,12 @@ src/extraction/STAMP:
 	@$(COQEXEC) ./src/extraction/Extraction.v
 	@touch $@
 
-Makefile.coq:
+Makefile.coq: force
 	@echo "COQMAKE Makefile.coq"
 	$(COQBIN)coq_makefile $(COQINCLUDES) $(VS) -o Makefile.coq
 
+force:
+
 clean:: Makefile.coq
 	$(MAKE) -f Makefile.coq clean
 	$(MAKE) -C test clean
diff --git a/_CoqProject b/_CoqProject
index 69d12c1..a1fe267 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -13,3 +13,6 @@
 -R lib/CompCert/verilog compcert.verilog
 -R lib/CompCert/flocq Flocq
 -R lib/CompCert/MenhirLib MenhirLib
+
+-R lib/compcert-kvx kvx
+-R lib/compcert-kvx/flocq kvx.Flocq
diff --git a/dune b/dune
index f58c64e..1423d67 100644
--- a/dune
+++ b/dune
@@ -1,6 +1,6 @@
 (dirs :standard \ "./lib/CompCert/x86_32" "./lib/CompCert/powerpc" "./lib/CompCert/riscV"
       "./lib/CompCert/arm" "./lib/CompCert/aarch64" "./lib/CompCert/extraction"
-      "./lib/CompCert/x86" "./lib/CompCert/x86_64")
+      "./lib/CompCert/x86" "./lib/CompCert/x86_64" "./lib/compcert-kvx")
 
 (include_subdirs unqualified)
 
diff --git a/lib/dune b/lib/dune
new file mode 100644
index 0000000..4b2632d
--- /dev/null
+++ b/lib/dune
@@ -0,0 +1 @@
+(dirs :standard \ compcert-kvx)
diff --git a/src/common/Show.v b/src/common/Show.v
index 20c07e7..67f6cba 100644
--- a/src/common/Show.v
+++ b/src/common/Show.v
@@ -26,7 +26,7 @@ Local Open Scope string.
 
 Class Show A : Type := { show : A -> string }.
 
-#[export]
+#[global]
 Instance showBool : Show bool :=
   { show := fun b:bool => if b then "true" else "false" }.
 
@@ -48,11 +48,11 @@ Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string :=
 Definition string_of_nat (n : nat) : string :=
   string_of_nat_aux n n "".
 
-#[export]
+#[global]
 Instance showNat : Show nat := { show := string_of_nat }.
 
-#[export]
+#[global]
 Instance showZ : Show Z := { show a := show (Z.to_nat a) }.
 
-#[export]
+#[global]
 Instance showPositive : Show positive := { show a := show (Zpos a) }.
diff --git a/src/superblock/RTLtoSRTL.v b/src/superblock/RTLtoSRTL.v
new file mode 100644
index 0000000..e093bc4
--- /dev/null
+++ b/src/superblock/RTLtoSRTL.v
@@ -0,0 +1,41 @@
+Require Import compcert.common.AST.
+Require Import compcert.backend.RTL.
+
+Require kvx.common.AST.
+Require kvx.backend.RTL.
+
+Module SRTL := kvx.backend.RTL.
+Module SAST := kvx.common.AST.
+
+Parameter transl_signature : signature -> SAST.signature.
+Parameter transl_code : code -> SRTL.code.
+
+Definition transl_function (f: function): SRTL.function :=
+  SRTL.mkfunction (transl_signature f.(fn_sig))
+                  f.(fn_params)
+                  f.(fn_stacksize)
+                  (transl_code f.(fn_code))
+                  f.(fn_entrypoint).
+
+Definition transl_fundef := transf_fundef transl_function.
+
+Inductive init_data: Type :=
+  | Init_int8: int -> init_data
+  | Init_int16: int -> init_data
+  | Init_int32: int -> init_data
+  | Init_int64: int64 -> init_data
+  | Init_float32: float32 -> init_data
+  | Init_float64: float -> init_data
+  | Init_space: Z -> init_data
+  | Init_addrof: ident -> ptrofs -> init_data.  (**r address of symbol + offset *)
+
+Definition transform_globvar {A} (a: globvar A): SAST.globvar A :=
+  SAST.mkglobvar a.(gvar_info)
+
+Definition transform_program_globdef {A B V} (transf: A -> B) (idg: ident * globdef A V) : ident * SAST.globdef B V :=
+  match idg with
+  | (id, Gfun f) => (id, SAST.Gfun (transf f))
+  | (id, Gvar v) => (id, SAST.Gvar v)
+  end.
+
+Definition transl_program (p: program): SRTL.program := transform_program transl_fundef.