Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work

5 files changed, 120 insertions, 33 deletions

diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index e9b2610c..980e18f8 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -474,4 +474,106 @@ Proof.
     }
   }
 
-*)
\ No newline at end of file
+ *)
+
+Require Import Coq.ZArith.Zquot.
+Lemma Z_quot_pos_pos_bound: forall a b m,
+    0 <= a <= m -> 1 <= b -> 0 <= Z.quot a b <= m.
+Proof.
+  intros.
+  split.
+  { rewrite <- (Z.quot_0_l b) by omega.
+    apply Z_quot_monotone; omega.
+  }
+  apply Z.le_trans with (m := a).
+  {
+    apply Z_quot_le; tauto.
+  }
+  tauto.
+Qed.
+Lemma Z_quot_neg_pos_bound: forall a b m,
+    m <= a <= 0 -> 1 <= b -> m <= Z.quot a b <= 0.
+  intros.
+  assert (0 <= - (a ÷ b) <= -m).
+  {
+    rewrite <- Z.quot_opp_l by omega.
+    apply Z_quot_pos_pos_bound; omega.
+  }
+  omega.
+Qed.
+
+Lemma Z_quot_signed_pos_bound: forall a b,
+    Int.min_signed <= a <= Int.max_signed -> 1 <= b ->
+    Int.min_signed <= Z.quot a b <= Int.max_signed.
+Proof.
+  intros.
+  destruct (Z_lt_ge_dec a 0).
+  {
+    split.
+    { apply Z_quot_neg_pos_bound; omega. }
+    { eapply Z.le_trans with (m := 0).
+      { apply Z_quot_neg_pos_bound with (m := Int.min_signed); trivial.
+        split. tauto. auto with zarith.
+      }
+      discriminate.
+    }
+  }
+  { split.
+    { eapply Z.le_trans with (m := 0).
+      discriminate.
+      apply Z_quot_pos_pos_bound with (m := Int.max_signed); trivial.
+      split. omega. tauto.
+    }
+    { apply Z_quot_pos_pos_bound; omega.
+    }
+  }
+Qed.
+
+Lemma Z_quot_signed_neg_bound: forall a b,
+    Int.min_signed <= a <= Int.max_signed -> b < -1 ->
+    Int.min_signed <= Z.quot a b <= Int.max_signed.
+Proof.
+  change Int.min_signed with (-2147483648).
+  change Int.max_signed with 2147483647.
+  intros.
+
+  replace b with (-(-b)) by auto with zarith.
+  rewrite Z.quot_opp_r by omega.
+  assert (-2147483647 <= (a ÷ - b) <= 2147483648).
+  2: omega.
+  
+  destruct (Z_lt_ge_dec a 0).
+  {
+    replace a with (-(-a)) by auto with zarith.
+    rewrite Z.quot_opp_l by omega.
+    assert (-2147483648 <= - a ÷ - b <= 2147483647).
+    2: omega.
+    split.
+    {
+      rewrite Z.quot_opp_l by omega.
+      assert (a ÷ - b <= 2147483648).
+      2: omega.
+      {
+        apply Z.le_trans with (m := 0).
+        rewrite <- (Z.quot_0_l (-b)) by omega.
+        apply Z_quot_monotone; omega.
+        discriminate.
+      }
+    }
+    assert (- a ÷ - b < -a ).
+    2: omega.
+    apply Z_quot_lt; omega.
+  }
+  {
+    split.
+    { apply Z.le_trans with (m := 0).
+      discriminate.
+      rewrite <- (Z.quot_0_l (-b)) by omega.
+      apply Z_quot_monotone; omega.
+    }
+    { apply Z.le_trans with (m := a).
+      apply Z_quot_le.
+      all: omega.
+    }
+  }
+Qed.
diff --git a/test/monniaux/benches.sh b/test/monniaux/benches.sh
index f6552370..9bca6b42 100644
--- a/test/monniaux/benches.sh
+++ b/test/monniaux/benches.sh
@@ -1,4 +1 @@
-#benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow ternary too_slow"
-benches="binary_search bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow ternary too_slow"
-
-# TODO - put back bitslices-aes once i get it working again
+benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow ternary too_slow"
diff --git a/test/monniaux/bitsliced-aes/Makefile b/test/monniaux/bitsliced-aes/Makefile
deleted file mode 100644
index 6a0367e0..00000000
--- a/test/monniaux/bitsliced-aes/Makefile
+++ /dev/null
@@ -1,23 +0,0 @@
-src = $(wildcard *.c) tests/tests.c
-
-include ../rules.mk
-
-all: test.gcc.k1c.out test.gcc.o1.k1c.out test.ccomp.k1c.out test.gcc.host.out test.ccomp.host.out
-
-test.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) -o $@ $+
-
-test.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) -o $@ $+
-
-test.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) -o $@ $+
-
-test.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o
-	$(CC) $(CFLAGS) -o $@ $+
-
-test.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) -o $@ $+
-
-clean:
-	rm -f *.o *.k1c *.host */*.o *.s */*.s *.out
diff --git a/test/monniaux/bitsliced-aes/make.proto b/test/monniaux/bitsliced-aes/make.proto
index 6f3139c7..530d7e36 100644
--- a/test/monniaux/bitsliced-aes/make.proto
+++ b/test/monniaux/bitsliced-aes/make.proto
@@ -1 +1,2 @@
+sources: "$(wildcard *.c) tests/tests.c"
 target: test
diff --git a/test/monniaux/genmake.py b/test/monniaux/genmake.py
index 7e25c181..c0fe0d05 100755
--- a/test/monniaux/genmake.py
+++ b/test/monniaux/genmake.py
@@ -41,6 +41,10 @@ with open(yaml_file, "r") as f:
 basename = settings["target"]
 objdeps = settings["objdeps"] if "objdeps" in settings else []
 intro = settings["intro"] if "intro" in settings else ""
+sources = settings["sources"] if "sources" in settings else None
+
+if sources:
+  intro += "\nsrc=" + sources
 
 for objdep in objdeps:
   if objdep["compiler"] not in ("gcc", "ccomp", "both"):
@@ -59,9 +63,16 @@ def make_obj(name, env, compiler_short):
 def make_clock(env, optim):
   return "clock.gcc." + env.target
 
+def make_sources(env, optim):
+  if sources:
+    return "$(src:.c=." + env.compiler.short + (("." + optim.short) if optim.short != "" else "") + "." + env.target + ".o)"
+  else:
+    return "{product}.o".format(product = make_product(env, optim))
+
 def print_rule(env, optim):
-  print("{product}: {product}.o ../{clock}.o "
-        .format(product = make_product(env, optim), clock = make_clock(env, optim))
+  print("{product}: {sources} ../{clock}.o "
+        .format(product = make_product(env, optim),
+          sources = make_sources(env, optim), clock = make_clock(env, optim))
           + " ".join([make_obj(objdep["name"], env, (objdep["compiler"] if objdep["compiler"] != "both" else env.compiler.short)) for objdep in objdeps]))
   print("	{compiler} {flags} $+ -o $@"
         .format(compiler = env.compiler.full, flags = optim.full))
@@ -91,8 +102,7 @@ for env in environments:
     print_rule(env, optim)
 
 print("""
+.PHONY:
 clean:
-	-rm -f *.o *.s *.k1c
-
-.PHONY: clean
+	rm -f *.o *.s *.k1c
 """)