Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load

18 files changed, 148 insertions, 92 deletions

diff --git a/configure b/configure
index 3bdb5d2b..626bf3aa 100755
--- a/configure
+++ b/configure
@@ -818,6 +818,7 @@ cat >> Makefile.config <<EOF
 ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure
 EXECUTE=k1-cluster --syscall=libstd_scalls.so --
 CFLAGS= -D __K1C_COS__
+SIMU=k1-cluster -- 
 BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
     Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 087e0308..ac34fa5f 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -238,11 +238,38 @@ let rv64 =
                    struct_return_style = SR_ref } (* to check *)
 
 let mppa_k1c =
-  { ilp32ll64 with sizeof_ptr = 8;
-                   sizeof_long = 8;
-                   name = "k1c";
-                   char_signed = true;
-                   supports_unaligned_accesses = true }
+  { name = "k1c";
+    char_signed = true;
+    wchar_signed = true;
+    sizeof_ptr = 8;
+    sizeof_short = 2;
+    sizeof_int = 4;
+    sizeof_long = 8;
+    sizeof_longlong = 8;
+    sizeof_float = 4;
+    sizeof_double = 8;
+    sizeof_longdouble = 8;
+    sizeof_void = None; (* What is this for ? *)
+    sizeof_fun = None; (* What is this for ? *)
+    sizeof_wchar = 4;
+    sizeof_size_t = 8;
+    sizeof_ptrdiff_t = 8;
+    sizeof_intreg = 8; (* What is this for ? *)
+    alignof_ptr = 8;
+    alignof_short = 2;
+    alignof_int = 4;
+    alignof_long = 8;
+    alignof_longlong = 8;
+    alignof_float = 4;
+    alignof_double = 8;
+    alignof_longdouble = 8;
+    alignof_void = None; (* what is this for ? *)
+    alignof_fun = None; (* what is this for ? *)
+    bigendian = false;
+    bitfields_msb_first = false; (* TO CHECK *)
+    supports_unaligned_accesses = true;
+    struct_passing_style = SP_split_args;
+    struct_return_style = SR_int1248 }
 
 (* Add GCC extensions re: sizeof and alignof *)
 
diff --git a/driver/Compiler.v b/driver/Compiler.v
index d006a7d1..7536e8ff 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -148,7 +148,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
   @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program)
   @@@ time "Mach generation" Stacking.transf_program
    @@ print print_Mach
-  @@@ time "Asm generation" Asmgen.transf_program.
+  @@@ time "Total Mach->Asm generation" Asmgen.transf_program.
 
 Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
    OK p
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 17925d8c..994d41a4 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -140,6 +140,7 @@ Extract Constant Compiler.print_LTL => "PrintLTL.print_if".
 Extract Constant Compiler.print_Mach => "PrintMach.print_if".
 Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x".
 Extract Constant Compiler.time  => "Timing.time_coq".
+Extract Constant Asmgen.time  => "Timing.time_coq".
 
 (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*)
 
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 5a103915..37bfbed9 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -345,34 +345,32 @@ let expand_int64_arith conflict rl fn = assert false
 (* Byte swaps.  There are no specific instructions, so we use standard,
    not-very-efficient formulas. *)
 
-let expand_bswap16 d s = assert false
+let expand_bswap16 d s = let open Asmvliw in
   (* d = (s & 0xFF) << 8 | (s >> 8) & 0xFF *)
-(*emit (Pandiw(X31, X s, coqint_of_camlint 0xFFl));
-  emit (Pslliw(X31, X X31, _8));
-  emit (Psrliw(d, X s, _8));
-  emit (Pandiw(d, X d, coqint_of_camlint 0xFFl));
-  emit (Porw(d, X X31, X d))
-*)
+  emit (Pandiw(GPR32, s, coqint_of_camlint 0xFFl)); emit Psemi;
+  emit (Pslliw(GPR32, GPR32, _8)); emit Psemi;
+  emit (Psrliw(d, s, _8)); emit Psemi;
+  emit (Pandiw(d, d, coqint_of_camlint 0xFFl));
+  emit (Porw(d, GPR32, d)); emit Psemi
 
-let expand_bswap32 d s = assert false
+let expand_bswap32 d s = let open Asmvliw in
   (* d = (s << 24)
        | (((s >> 8) & 0xFF) << 16)
        | (((s >> 16) & 0xFF) << 8)
        | (s >> 24)  *)
-(*emit (Pslliw(X1, X s, coqint_of_camlint 24l));
-  emit (Psrliw(X31, X s, _8));
-  emit (Pandiw(X31, X X31, coqint_of_camlint 0xFFl));
-  emit (Pslliw(X31, X X31, _16));
-  emit (Porw(X1, X X1, X X31));
-  emit (Psrliw(X31, X s, _16));
-  emit (Pandiw(X31, X X31, coqint_of_camlint 0xFFl));
-  emit (Pslliw(X31, X X31, _8));
-  emit (Porw(X1, X X1, X X31));
-  emit (Psrliw(X31, X s, coqint_of_camlint 24l));
-  emit (Porw(d, X X1, X X31))
-*)
-
-let expand_bswap64 d s = assert false
+  emit (Pslliw(GPR16, s, coqint_of_camlint 24l)); emit Psemi;
+  emit (Psrliw(GPR32, s, _8)); emit Psemi;
+  emit (Pandiw(GPR32, GPR32, coqint_of_camlint 0xFFl)); emit Psemi;
+  emit (Pslliw(GPR32, GPR32, _16)); emit Psemi;
+  emit (Porw(GPR16, GPR16, GPR31)); emit Psemi;
+  emit (Psrliw(GPR32, s, _16)); emit Psemi;
+  emit (Pandiw(GPR32, GPR32, coqint_of_camlint 0xFFl)); emit Psemi;
+  emit (Pslliw(GPR32, GPR32, _8)); emit Psemi;
+  emit (Porw(GPR16, GPR16, GPR32)); emit Psemi;
+  emit (Psrliw(GPR32, s, coqint_of_camlint 24l)); emit Psemi;
+  emit (Porw(d, GPR16, GPR32)); emit Psemi
+
+let expand_bswap64 d s = let open Asmvliw in
   (* d = s << 56
          | (((s >> 8) & 0xFF) << 48)
          | (((s >> 16) & 0xFF) << 40)
@@ -381,17 +379,16 @@ let expand_bswap64 d s = assert false
          | (((s >> 40) & 0xFF) << 16)
          | (((s >> 48) & 0xFF) << 8)
          | s >> 56 *)
-(*emit (Psllil(X1, X s, coqint_of_camlint 56l));
+  emit (Psllil(GPR16, s, coqint_of_camlint 56l)); emit Psemi;
   List.iter
     (fun (n1, n2) ->
-      emit (Psrlil(X31, X s, coqint_of_camlint n1));
-      emit (Pandil(X31, X X31, coqint_of_camlint 0xFFl));
-      emit (Psllil(X31, X X31, coqint_of_camlint n2));
-      emit (Porl(X1, X X1, X X31)))
+      emit (Psrlil(GPR32, s, coqint_of_camlint n1)); emit Psemi;
+      emit (Pandil(GPR32, GPR32, coqint_of_camlint 0xFFl)); emit Psemi;
+      emit (Psllil(GPR32, GPR32, coqint_of_camlint n2)); emit Psemi;
+      emit (Porl(GPR16, GPR16, GPR32)); emit Psemi;)
     [(8l,48l); (16l,40l); (24l,32l); (32l,24l); (40l,16l); (48l,8l)];
-  emit (Psrlil(X31, X s, coqint_of_camlint 56l));
-  emit (Porl(d, X X1, X X31))
-*)
+  emit (Psrlil(GPR32, s, coqint_of_camlint 56l)); emit Psemi;
+  emit (Porl(d, GPR16, GPR32)); emit Psemi
 
 (* Handling of compiler-inlined builtins *)
 let last_system_register = 511l
@@ -477,6 +474,12 @@ let expand_builtin_inline name args res = let open Asmvliw in
      emit (Palclrd(res, addr))
   | "__builtin_alclrw", [BA(IR addr)], BR(IR res) ->
      emit (Palclrw(res, addr))
+  | "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
+     expand_bswap16 res a1
+  | ("__builtin_bswap"| "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
+     expand_bswap32 res a1
+  | "__builtin_bswap64", [BA(IR src)], BR(IR res) ->
+     expand_bswap64 res src
 	  
   (* Byte swaps *)
 (*| "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 58e80be1..c3588871 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -18,15 +18,17 @@
 Require Import Integers.
 Require Import Mach Asm Asmblock Asmblockgen Machblockgen.
 Require Import PostpassScheduling.
-Require Import Errors.
+Require Import Errors String.
 
 Local Open Scope error_monad_scope.
 
+Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f.
+
 Definition transf_program (p: Mach.program) : res Asm.program :=
-  let mbp := Machblockgen.transf_program p in
-  do abp <- Asmblockgen.transf_program mbp;
-  do abp' <- PostpassScheduling.transf_program abp;
-  OK (Asm.transf_program abp').
+  let mbp := (time "Machblock generation" Machblockgen.transf_program) p in
+  do abp <- (time "Asmblock generation" Asmblockgen.transf_program) mbp;
+  do abp' <- (time "PostpassScheduling total oracle+verification" PostpassScheduling.transf_program) abp;
+  OK ((time "Asm generation" Asm.transf_program) abp').
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
   let mbf := Machblockgen.transf_function f in
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index e0878c7d..5d7bb81f 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -35,7 +35,7 @@ Proof.
   intros p tp H.
   unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
   inversion_clear H. apply bind_inversion in H1. destruct H1.
-  inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp.
+  inversion_clear H. inversion H2. unfold time in *. remember (Machblockgen.transf_program p) as mbp.
   unfold match_prog; simpl.
   exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
   exists x; split. apply Asmblockgenproof.transf_program_match; auto.
diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml
index 235496c5..a91119b1 100644
--- a/mppa_k1c/CBuiltins.ml
+++ b/mppa_k1c/CBuiltins.ml
@@ -96,12 +96,8 @@ let builtins = {
 
     (* Synchronization *)
 (*  "__builtin_fence",
-      (TVoid [], [], false);
-    (* Integer arithmetic *)
-    "__builtin_bswap64",
-      (TInt(IULongLong, []), 
-       [TInt(IULongLong, [])], false);
-    (* Float arithmetic *)
+      (TVoid [], [], false); *)
+(*  (* Float arithmetic *)
     "__builtin_fmadd",
       (TFloat(FDouble, []),
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false);
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 41dac766..cdda0e6d 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -991,4 +991,5 @@ let rec bundles_to_coq_schedule = function
 
 (** Called schedule function from Coq *)
 
-let schedule bb = let toto = bundles_to_coq_schedule @@ bblock_to_bundles bb in toto
+let schedule_notime bb = let toto = bundles_to_coq_schedule @@ bblock_to_bundles bb in toto
+let schedule bb = Timing.time_coq ('P'::('o'::('s'::('t'::('p'::('a'::('s'::('s'::('S'::('c'::('h'::('e'::('d'::('u'::('l'::('i'::('n'::('g'::(' '::('o'::('r'::('a'::('c'::('l'::('e'::([])))))))))))))))))))))))))) schedule_notime bb
diff --git a/mppa_k1c/lib/Machblockgenproof.v b/mppa_k1c/lib/Machblockgenproof.v
index 77db094d..02d154c7 100644
--- a/mppa_k1c/lib/Machblockgenproof.v
+++ b/mppa_k1c/lib/Machblockgenproof.v
@@ -719,17 +719,17 @@ Proof.
   intro H; destruct c as [|i' c]. { inversion H. }
   remember (trans_inst i) as ti.
   destruct ti as [lbl|bi|cfi].
-  - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2:{ destruct i; simpl in * |- *; try congruence. }
+  - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; simpl in * |- *; try congruence ).
     exists nil; simpl; eexists. eapply Tr_add_label; eauto.
   - (*i=basic*)
     destruct i'.
-    10: {exists (add_to_new_bblock (MB_basic bi)::nil).  exists b. 
+    Focus 10. exists (add_to_new_bblock (MB_basic bi)::nil).  exists b. 
       cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto.
       rewrite Heqti.        
       eapply  Tr_end_block; eauto.
       rewrite <-Heqti.
       eapply End_basic. inversion H; try(simpl; congruence).
-      simpl in H5; congruence. }
+      simpl in H5; congruence.
     all: try(exists nil; simpl; eexists;  eapply  Tr_add_basic; eauto; inversion H; try(eauto || congruence)).
   - (*i=cfi*)
     destruct i; try(simpl in Heqti; congruence).
diff --git a/test/Makefile b/test/Makefile
index 504e4c53..7efcd8f1 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -1,6 +1,12 @@
 include ../Makefile.config
 
-DIRS=c compression raytracer spass regression
+#DIRS=c compression raytracer spass regression
+
+# Kalray note - removing compression, raytracer and spass that cannot be executed by the simulator in reasonable time
+ifeq ($(ARCH),mppa_k1c)
+	DIRS:=c regression
+endif
+
 ifeq ($(CLIGHTGEN),true)
 DIRS+=clightgen
 endif
diff --git a/test/c/Makefile b/test/c/Makefile
index b2d83352..7aee6c4f 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -45,7 +45,7 @@ test: all
 	   $(EXECUTE) ./$$i.compcert > $$i.compcert.out;\
 	   if cmp -s $$i.compcert.out Results/$$i; \
            then echo "$$i: passed"; \
-           else echo "$$i: FAILED"; \
+           else echo "$$i: FAILED"; exit 2; \
 	   fi; \
          done
 
@@ -54,7 +54,7 @@ test_gcc: all_gcc
 	   $(EXECUTE) ./$$i.gcc > $$i.gcc.out;\
 	   if cmp -s $$i.gcc.out Results/$$i; \
            then echo "$$i: passed"; \
-           else echo "$$i: FAILED"; \
+           else echo "$$i: FAILED"; exit 2;\
 	   fi; \
          done
 
diff --git a/test/compression/Makefile b/test/compression/Makefile
index 2e14e646..48521b14 100644
--- a/test/compression/Makefile
+++ b/test/compression/Makefile
@@ -1,5 +1,7 @@
 include ../../Makefile.config
 
+SIMU=timeout --signal=SIGKILL 20s $(EXECUTE)
+
 CC=../../ccomp 
 CFLAGS=$(CCOMPOPTS) -U__GNUC__ -stdlib ../../runtime -dclight -dasm
 LIBS=
@@ -30,15 +32,19 @@ TESTFILE:=$(firstword $(wildcard /usr/share/dict/words) ./lzss)
 TESTCOMPR=/tmp/testcompr.$$$$
 TESTEXPND=/tmp/testexpnd.$$$$
 
+LIGHTERFILEPRE:=/tmp/lighter
+LIGHTERFILE:=$(LIGHTERFILEPRE)aa
+
 test:
-	@rm -f $(TESTCOMPR) $(TESTEXPND); \
-	echo "Test data: $(TESTFILE)"; \
+	@split -l15 $(TESTFILE) $(LIGHTERFILEPRE); \
+	rm -f $(TESTCOMPR) $(TESTEXPND); \
+	echo "Test data: $(LIGHTERFILE)"; \
 	for i in $(EXE); do \
           echo "$$i: compression..."; \
-          $(SIMU) ./$$i -c -i $(TESTFILE) -o $(TESTCOMPR); \
+          $(SIMU) ./$$i -c -i $(LIGHTERFILE) -o $(TESTCOMPR); \
           echo "$$i: decompression..."; \
           $(SIMU) ./$$i -d -i $(TESTCOMPR) -o $(TESTEXPND); \
-          if cmp $(TESTFILE) $(TESTEXPND); \
+          if cmp $(LIGHTERFILE) $(TESTEXPND); \
           then echo "$$i: passed"; \
           else echo "$$i: FAILED"; exit 2; \
           fi; \
@@ -49,7 +55,7 @@ bench:
 	@rm -f $(TESTCOMPR)
 	@for i in $(EXE); do \
           echo -n "$$i: "; \
-          $(TIME) sh -c "./$$i -c -i $(TESTFILE) -o $(TESTCOMPR) && ./$$i -d -i $(TESTCOMPR) -o /dev/null"; \
+          $(TIME) sh -c "./$$i -c -i $(LIGHTERFILE) -o $(TESTCOMPR) && ./$$i -d -i $(TESTCOMPR) -o /dev/null"; \
          done
 	@rm -f $(TESTCOMPR)
 
diff --git a/test/mppa/interop/common.c b/test/mppa/interop/common.c
index e939e0d1..05b49187 100644
--- a/test/mppa/interop/common.c
+++ b/test/mppa/interop/common.c
@@ -1,17 +1,21 @@
 #define STACK int a[100];\
   a[42] = 42;
 
-#define ONEARG_OP(arg) (3*arg+2)
+#define ONEARG_OP(arg) (3*magic(arg)+2)
 
-#define MULTIARG_OP(arg1, arg2, arg3, arg4) (arg1 ^ arg2 << arg3 - arg4)
+#define MULTIARG_OP(arg1, arg2, arg3, arg4) (arg1 ^ magic(arg2) << arg3 - arg4)
 
 #define MANYARG_OP(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9,\
                    a10, a11, a12, a13, a14, a15, a16, a17, a18, a19,\
                    a20, a21, a22, a23, a24, a25, a26, a27, a28, a29)\
-  (a0 * a1 * a2 * a3 * a4 * a5 * a6 * a7 * a8 * a9 *\
+  (a0 * a1 * a2 * magic(a3) * a4 * a5 * a6 * a7 * a8 * a9 *\
           a10 * a11 * a12 * a13 * a14 * a15 * a16 * a17 * a18 * a19 *\
           a20 * a21 * a22 * a23 * a24 * a25 * a26 * a27 * a28 * a29)
 
+int magic(long a){
+  return a*42 + 26;
+}
+
 void void_void(){
   STACK;
 }
diff --git a/test/mppa/interop/vaarg_common.c b/test/mppa/interop/vaarg_common.c
index 9033893b..3314959f 100644
--- a/test/mppa/interop/vaarg_common.c
+++ b/test/mppa/interop/vaarg_common.c
@@ -3,20 +3,24 @@
 #define STACK int a[100];\
   a[42] = 42;
 
-#define ONEARG_OP(arg) (3*arg+2)
+#define ONEARG_OP(arg) (3*magic(arg)+2)
 
-#define MULTIARG_OP(arg1, arg2, arg3, arg4) (arg1 ^ arg2 << arg3 - arg4)
+#define MULTIARG_OP(arg1, arg2, arg3, arg4) (arg1 ^ magic(arg2) << arg3 - arg4)
 
 #define MANYARG_OP(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9,\
                    a10, a11, a12, a13, a14, a15, a16, a17, a18, a19,\
                    a20, a21, a22, a23, a24, a25, a26, a27, a28, a29)\
-  (a0 + a1 * a2 + a3 * a4 + a5 + a6 + a7 - a8 + a9 +\
-          a10 + a11 - a12 ^ a13 + a14 - a15 + a16 ^ a17 + a18 + a19 +\
+  (a0 + a1 * a2 + magic(a3) * a4 + a5 + a6 + a7 - a8 + a9 +\
+          a10 + a11 - a12 ^ a13 + a14 - magic(a15) + a16 ^ a17 + a18 + a19 +\
           a20 + a21 + a22 * a23 + a24 + a25 << a26 & a27 + a28 + a29)
 
 #define VA_START(vl, arg) va_list vl; va_start(vl, arg)
 #define VA_END(vl) va_end(vl)
 
+int magic(long a){
+  return a*2 + 42;
+}
+
 void void_void(void){
   STACK;
 }
diff --git a/test/regression/Makefile b/test/regression/Makefile
index ab27c85a..57547694 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -9,8 +9,7 @@ LIBS=$(LIBMATH)
 
 # Can run, both in compiled mode and in interpreter mode,
 # and have reference output in Results
-
-TESTS=int32 int64 floats floats-basics \
+TESTS?=int32 int64 floats floats-basics \
   expr1 expr6 funptr2 initializers initializers2 initializers3 \
   volatile1 volatile2 volatile3 volatile4 \
   funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \
@@ -20,11 +19,16 @@ TESTS=int32 int64 floats floats-basics \
 
 # Can run, but only in compiled mode, and have reference output in Results
 
-TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
+TESTS_COMP?=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
   bitfields5 bitfields6 bitfields7 bitfields8 \
   builtins-$(ARCH) alignas \
-  varargs1 varargs2 varargs3 sections alias aligned
-# FIXME K1C : packedstruct1 packedstruct2
+  varargs1 varargs2 varargs3 sections alias aligned\
+  packedstruct1 packedstruct2
+
+# varargs2 ---> bug in k1-cos-gcc
+ifeq ($(ARCH),mppa_k1c)
+	TESTS_COMP:=$(filter-out varargs2,$(TESTS_COMP))
+endif
 
 # Can run, both in compiled mode and in interpreter mode,
 # but produce processor-dependent results, so no reference output in Results
diff --git a/test/regression/extasm.c b/test/regression/extasm.c
index 83a07a05..95628f7f 100644
--- a/test/regression/extasm.c
+++ b/test/regression/extasm.c
@@ -21,7 +21,8 @@ int clobbers(int x, int z)
 #if (defined(ARCH_x86) && defined(MODEL_64)) \
  || (defined(ARCH_riscV) && defined(MODEL_64)) \
  || (defined(ARCH_powerpc) && defined(MODEL_ppc64)) \
- || (defined(ARCH_powerpc) && defined(MODEL_e5500))
+ || (defined(ARCH_powerpc) && defined(MODEL_e5500)) \
+ || (defined(ARCH_mppa_k1c) && defined(MODEL_64))
 #define SIXTYFOUR
 #else
 #undef SIXTYFOUR
diff --git a/test/regression/packedstruct1.c b/test/regression/packedstruct1.c
index 5d3e7124..ac68c698 100644
--- a/test/regression/packedstruct1.c
+++ b/test/regression/packedstruct1.c
@@ -2,8 +2,8 @@
 
 #include <stdio.h>
 
-/* offsetof is the offset computed by the verified front-end (cfrontend/) */
-#define offsetof(s,f) (int)&(((struct s *)0)->f)
+/* offsetOf is the offset computed by the verified front-end (cfrontend/) */
+#define offsetOf(s,f) (int)&(((struct s *)0)->f)
 
 /* boffsetof is the offset computed by the elaborator (cparser/) */
 #define boffsetof(s,f) (int)__builtin_offsetof(struct s, f)
@@ -23,9 +23,9 @@ void test1(void)
   struct s1 s1;
   printf("sizeof(struct s1) = %d\n", szof(s1));
   printf("precomputed sizeof(struct s1) = %d\n", bszof(s1));
-  printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
-         offsetof(s1,x), offsetof(s1,y), offsetof(s1,z));
-  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+  printf("offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
+         offsetOf(s1,x), offsetOf(s1,y), offsetOf(s1,z));
+  printf("precomputed offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
          boffsetof(s1,x), boffsetof(s1,y), boffsetof(s1,z));
   s1.x = 123; s1.y = -456; s1.z = 3.14159;
   printf("s1 = {x = %d, y = %d, z = %.5f}\n\n", s1.x, s1.y, s1.z);
@@ -44,9 +44,9 @@ void test2(void)
   printf("sizeof(struct s2) = %d\n", szof(s2));
   printf("precomputed sizeof(struct s2) = %d\n", bszof(s2));
   printf("&s2 mod 16 = %d\n", ((int) &s2) & 0xF);
-  printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
-         offsetof(s2,x), offsetof(s2,y), offsetof(s2,z));
-  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+  printf("offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
+         offsetOf(s2,x), offsetOf(s2,y), offsetOf(s2,z));
+  printf("precomputed offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
          boffsetof(s2,x), boffsetof(s2,y), boffsetof(s2,z));
   s2.x = 12345; s2.y = -456; s2.z = 3.14159;
   printf("s2 = {x = %d, y = %d, z = %.5f}\n\n", s2.x, s2.y, s2.z);
@@ -73,8 +73,8 @@ void test3(void)
 
   printf("sizeof(struct s3) = %d\n", szof(s3));
   printf("precomputed sizeof(struct s3) = %d\n", bszof(s3));
-  printf("offsetof(s) = %d\n", offsetof(s3,s));
-  printf("precomputed offsetof(s) = %d\n", boffsetof(s3,s));
+  printf("offsetOf(s) = %d\n", offsetOf(s3,s));
+  printf("precomputed offsetOf(s) = %d\n", boffsetof(s3,s));
   s3.x = 123;
   s3.y = 45678;
   s3.z = 0x80000001U;
@@ -103,9 +103,9 @@ void test4(void)
 
   printf("sizeof(struct s4) = %d\n", szof(s4));
   printf("precomputed sizeof(struct s4) = %d\n", bszof(s4));
-  printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
-         offsetof(s4,x), offsetof(s4,y), offsetof(s4,z));
-  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+  printf("offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
+         offsetOf(s4,x), offsetOf(s4,y), offsetOf(s4,z));
+  printf("precomputed offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
          boffsetof(s4,x), boffsetof(s4,y), boffsetof(s4,z));
   s4.x = 123; s4.y = -456; s4.z = 3.14159;
   printf("s4 = {x = %d, y = %d, z = %.5f}\n\n", s4.x, s4.y, s4.z);
@@ -121,9 +121,9 @@ void test5(void)
 
   printf("sizeof(struct s5) = %d\n", szof(s5));
   printf("precomputed sizeof(struct s5) = %d\n", bszof(s5));
-  printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
-         offsetof(s5,x), offsetof(s5,y), offsetof(s5,z));
-  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+  printf("offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
+         offsetOf(s5,x), offsetOf(s5,y), offsetOf(s5,z));
+  printf("precomputed offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
          boffsetof(s5,x), boffsetof(s5,y), boffsetof(s5,z));
   s5.x = 123; s5.y = -456; s5.z = 3.14159;
   printf("s5 = {x = %d, y = %d, z = %.5f}\n\n", s5.x, s5.y, s5.z);
@@ -139,9 +139,9 @@ void test6(void)
 
   printf("sizeof(struct s6) = %d\n", szof(s6));
   printf("precomputed sizeof(struct s6) = %d\n", bszof(s6));
-  printf("offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
-         offsetof(s6,x), offsetof(s6,y), offsetof(s6,z));
-  printf("precomputed offsetof(x) = %d, offsetof(y) = %d, offsetof(z) = %d\n",
+  printf("offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
+         offsetOf(s6,x), offsetOf(s6,y), offsetOf(s6,z));
+  printf("precomputed offsetOf(x) = %d, offsetOf(y) = %d, offsetOf(z) = %d\n",
          boffsetof(s6,x), boffsetof(s6,y), boffsetof(s6,z));
   s62.x = 123; s62.y = -456; s62.z = 3.14159;
   printf("s62 = {x = %d, y = %d, z = %.5f}\n\n", s62.x, s62.y, s62.z);