Start working on supporting different back endsdev/scheduling

3 files changed, 5 insertions, 32 deletions

diff --git a/Makefile b/Makefile
index 4e44eeb..f9dfce2 100644
--- a/Makefile
+++ b/Makefile
@@ -43,7 +43,7 @@ lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
 
 install:
 	install -d $(PREFIX)/bin
-	sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
+	sed -i'' -e 's/arch=verilog/arch=aarch64/' _build/default/driver/compcert.ini
 	install -C _build/default/driver/compcert.ini $(PREFIX)/bin/.
 	install -C _build/default/driver/VericertDriver.exe $(PREFIX)/bin/vericert-kvx
 
diff --git a/lib/CompCert b/lib/CompCert
-Subproject 9c72ffe762dc2f90109d5991f74ee0ee4e9a8ec
+Subproject 246ae564d9ce6c04ba4169b80d2ff9ce21deca3
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index 1bdc170..8084d32 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -307,8 +307,6 @@ Definition translate_condition (c : Op.condition) (args : list reg) : mon expr :
   | Op.Ccompu c, _ => translate_comparisonu c args
   | Op.Ccompimm c i, _ => translate_comparison_imm c args i
   | Op.Ccompuimm c i, _ => translate_comparison_immu c args i
-  | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero")
-  | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero")
   | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other")
   end.
 
@@ -321,22 +319,11 @@ Definition check_address_parameter_unsigned (p : Z) : bool :=
 
 Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr :=
   match a, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Op.Aindexed off, r1::nil =>
+  | Op.Aindexed off', r1::nil =>
+      let off := Integers.Ptrofs.unsigned off' in
     if (check_address_parameter_signed off)
     then ret (boplitz Vadd r1 off)
     else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds")
-  | Op.Ascaled scale offset, r1::nil =>
-    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset)))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds")
-  | Op.Aindexed2 offset, r1::r2::nil =>
-    if (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset)))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds")
-  | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
-    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset))))
-    else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds")
   | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in
     if (check_address_parameter_unsigned a)
@@ -353,7 +340,6 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r))
   | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2)
   | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2)
-  | Op.Omulimm n, r::nil => ret (boplit Vmul r n)
   | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs")
   | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu")
   | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2)
@@ -366,7 +352,6 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
   | Op.Oorimm n, r::nil => ret (boplit Vor r n)
   | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2)
   | Op.Oxorimm n, r::nil => ret (boplit Vxor r n)
-  | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r))
   | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2)
   | Op.Oshlimm n, r::nil => ret (boplit Vshl r n)
   | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2)
@@ -377,15 +362,9 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
                   (Vbinop Vshru (Vvar r) (Vlit n)))
   | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2)
   | Op.Oshruimm n, r::nil => ret (boplit Vshru r n)
-  | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm")
   (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32)))
                                         (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*)
-  | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n)))
   | Op.Ocmp c, _ => translate_condition c args
-  | Op.Osel c AST.Tint, r1::r2::rl =>
-    do tc <- translate_condition c rl;
-    ret (Vternary tc (Vvar r1) (Vvar r2))
-  | Op.Olea a, _ => translate_eff_addressing a args
   | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other")
   end.
 
@@ -426,17 +405,11 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit :=
 Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing)
            (args : list reg) (stack : reg) : mon expr :=
   match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*)
-  | Mint32, Op.Aindexed off, r1::nil =>
+  | Mint32, Op.Aindexed off', r1::nil =>
+      let off := Integers.Ptrofs.unsigned off' in
     if (check_address_parameter_signed off)
     then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4))))
     else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
-  | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *)
-    if (check_address_parameter_signed scale) && (check_address_parameter_signed offset)
-    then ret (Vvari stack
-                    (Vbinop Vdivu
-                            (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale))
-                            (Vlit (ZToValue 4))))
-    else error (Errors.msg "HTLgen: translate_arr_access address out of bounds")
   | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *)
     let a := Integers.Ptrofs.unsigned a in
     if (check_address_parameter_unsigned a)