Mise à jour vis à vis de CompCert 3.4

7 files changed, 51 insertions, 10 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 557ab788..40df63e5 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -1130,6 +1130,16 @@ Definition preg_of (r: mreg) : preg :=
   | R60 => GPR60 | R61 => GPR61 | R62 => GPR62 | R63 => GPR63
   end.
 
+(** Undefine all registers except SP and callee-save registers *)
+
+Definition undef_caller_save_regs (rs: regset) : regset :=
+  fun r =>
+    if preg_eq r SP
+    || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs))
+    then rs r
+    else Vundef.
+
+
 (** Extract the values of the arguments of an external call.
     We exploit the calling conventions from module [Conventions], except that
     we use RISC-V registers instead of locations. *)
@@ -1197,7 +1207,7 @@ Inductive step: state -> trace -> state -> Prop :=
       Genv.find_funct_ptr ge b = Some (External ef) ->
       external_call ef ge args m t res m' ->
       extcall_arguments rs m (ef_sig ef) args ->
-      rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs RA) ->
+      rs' = (set_pair (loc_external_result (ef_sig ef) ) res (undef_caller_save_regs rs))#PC <- (rs RA) ->
       step (State rs m) t (State rs' m')
   .
 
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 2ac5cc16..d024a74f 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -62,6 +62,7 @@ Notation "a ::g b" := (cons (A:=instruction) a b) (at level 49, right associativ
 Notation "a ::i b" := (cons (A:=basic) a b) (at level 49, right associativity).
 Notation "a ::b lb" := ((bblock_single_inst a) :: lb) (at level 49, right associativity).
 Notation "a ++g b" := (app (A:=instruction) a b) (at level 49, right associativity).
+Notation "a @@ b" := (app a b) (at level 49, right associativity).
 
 (** Smart constructors for arithmetic operations involving
   a 32-bit or 64-bit integer constant.  Depending on whether the
@@ -910,7 +911,7 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep:
   | mb :: lmb => 
       do lb <- transl_block f mb (if Machblock.header mb then ep else false);
       do lb' <- transl_blocks f lmb false;
-      OK (lb ++ lb')
+      OK (lb @@ lb')
   end
 .
 
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index ee18e5e3..f97a71b1 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -2088,6 +2088,7 @@ Local Transparent destroyed_at_function_entry.
   unfold loc_external_result.

   apply agree_set_other; auto.

   apply agree_set_pair; auto.

+  apply agree_undef_caller_save_regs; auto.

 

 - (* return *) 

   inv MS.

diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index e2b72295..443e8757 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -13,6 +13,7 @@ Require Import Locations.
 Require Import Machblock.
 Require Import Asmblock.
 Require Import Asmblockgen.
+Require Import Conventions1.
 
 Module MB:=Machblock.
 Module AB:=Asmblock.
@@ -301,6 +302,23 @@ Proof.
   intros. rewrite Pregmap.gso; auto.
 Qed.
 
+Lemma agree_undef_caller_save_regs:
+  forall ms sp rs,
+  agree ms sp rs ->
+  agree (Mach.undef_caller_save_regs ms) sp (Asmblock.undef_caller_save_regs rs).
+Proof.
+  intros. destruct H. unfold Mach.undef_caller_save_regs, Asmblock.undef_caller_save_regs; split.
+- unfold proj_sumbool; rewrite dec_eq_true. auto.
+- auto.
+- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
+  destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl.
++ apply list_in_map_inv in i. destruct i as (mr & A & B). 
+  assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A.
+  apply List.filter_In in B. destruct B as [C D]. rewrite D. auto.
++ destruct (is_callee_save r) eqn:CS; auto.
+  elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. 
+Qed.
+
 Lemma agree_change_sp:
   forall ms sp rs sp',
   agree ms sp rs -> sp' <> Vundef ->
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 13869268..3b3b2b65 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -24,7 +24,7 @@ open Asmgen
 open Asmexpandaux
 open AST
 open Camlcoq
-open Integers
+open !Integers
 
 exception Error of string
 
@@ -557,10 +557,7 @@ let preg_to_dwarf = let open Asmblock in function
 let expand_function id fn =
   try
     set_current_function fn;
-    if !Clflags.option_g then
-      expand_debug id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code
-    else
-      List.iter expand_instruction fn.fn_code;
+    expand id (* sp= *) 2 preg_to_dwarf expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
diff --git a/mppa_k1c/Machblock.v b/mppa_k1c/Machblock.v
index 44cec642..30393fd5 100644
--- a/mppa_k1c/Machblock.v
+++ b/mppa_k1c/Machblock.v
@@ -327,7 +327,7 @@ Inductive step: state -> trace -> state -> Prop :=
       Genv.find_funct_ptr ge fb = Some (External ef) ->
       extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
       external_call ef ge args m t res m' ->
-      rs' = set_pair (loc_result (ef_sig ef)) res rs ->
+      rs' = set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) ->
       step (Callstate s fb rs m)
          t (Returnstate s rs' m')
   | exec_return:
diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile
index 89ff9a73..34b5e9ec 100644
--- a/test/mppa/instr/Makefile
+++ b/test/mppa/instr/Makefile
@@ -3,7 +3,7 @@ CC ?= gcc
 CCOMP ?= ccomp
 CFLAGS ?= -O2
 SIMU ?= k1-cluster
-TIMEOUT ?= 10s
+TIMEOUT ?= --signal=SIGTERM 20s
 
 DIR=./
 SRCDIR=$(DIR)
@@ -37,7 +37,7 @@ BIN=$(addprefix $(BINDIR)/,$(addsuffix .x86-gcc.bin,$(TESTNAMES)))\
 
 all: $(BIN)
 
-.PHONY:
+.PHONY: 
 test: $(X86_GCC_OUT) $(GCC_OUT)
 	@echo "Comparing x86 gcc output to k1 gcc.."
 	@for test in $(TESTNAMES); do\
@@ -70,6 +70,20 @@ check: $(GCC_OUT) $(CCOMP_OUT)
 .SECONDARY:
 # Generating output
 
+## Version sans les timeout
+#$(OUTDIR)/%.x86-gcc.out: $(BINDIR)/%.x86-gcc.bin
+#	@mkdir -p $(@D)
+#	./$< > $@; echo $$? >> $@
+#
+#$(OUTDIR)/%.gcc.out: $(BINDIR)/%.gcc.bin $(SIMUPATH)
+#	@mkdir -p $(@D)
+#	$(SIMU) -- $< > $@ ; echo $$? >> $@
+#
+#$(OUTDIR)/%.ccomp.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH)
+#	@mkdir -p $(@D)
+#	$(SIMU) -- $< > $@ ; echo $$? >> $@
+
+## Version avec timeout
 $(OUTDIR)/%.x86-gcc.out: $(BINDIR)/%.x86-gcc.bin
 	@mkdir -p $(@D)
 	ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@