Merge branch 'kvx-work' into BTL

12 files changed, 105 insertions, 80 deletions

diff --git a/Makefile.extr b/Makefile.extr
index 6d8611a9..84762c74 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -51,7 +51,7 @@ INCLUDES=$(patsubst %,-I %, $(DIRS))
 # Control of warnings:
 
 # WARNINGS=-w +a-4-9-27-42 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03
-WARNINGS=-w +a-4-9-27-42
+WARNINGS=-w +a-4-9-27-42-70-69 # 70,69 for OCaml 4.13
 
 extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67
diff --git a/compcert_build_env.dockerfile b/compcert_build_env.dockerfile
new file mode 100644
index 00000000..de339e55
--- /dev/null
+++ b/compcert_build_env.dockerfile
@@ -0,0 +1,6 @@
+FROM debian:stable-20210408
+LABEL maintainer="David.Monniaux@univ-grenoble-alpes.fr"
+RUN apt-get update && apt-get upgrade -y && apt-get -y install gcc-powerpc-linux-gnu gcc-powerpc64-linux-gnu gcc-riscv64-linux-gnu gcc-arm-linux-gnueabi gcc-arm-linux-gnueabihf  gcc-aarch64-linux-gnu qemu-user opam
+RUN adduser --gecos "Application user" appuser
+USER appuser
+RUN opam init --disable-sandboxing && opam switch create 4.11.2+flambda && eval $(opam config env) && opam pin -y add -n coq 8.12.2 && opam install -y menhir ocamlbuild coq
diff --git a/compcert_kvx.dockerfile b/compcert_kvx.dockerfile
new file mode 100644
index 00000000..21b15308
--- /dev/null
+++ b/compcert_kvx.dockerfile
@@ -0,0 +1,19 @@
+FROM compcert_build_env
+USER root
+RUN mkdir /opt/CompCert && chown appuser:appuser /opt/CompCert
+COPY --chown=appuser:appuser . CompCert
+USER appuser
+
+RUN eval $(opam config env) && cd CompCert && git clean -dfx && git reset --hard && ./config_aarch64.sh && make && make install
+
+RUN eval $(opam config env) && cd CompCert && git clean -dfx && git reset --hard && ./config_arm.sh && make && make install
+
+RUN eval $(opam config env) && cd CompCert && git clean -dfx && git reset --hard && ./config_armhf.sh && make && make install
+
+# RUN eval $(opam config env) && cd CompCert && git clean -dfx && git reset --hard && ./config_ia32.sh && make && make install
+
+RUN eval $(opam config env) && cd CompCert && git clean -dfx && git reset --hard && ./config_x86_64.sh && make && make install
+
+# RUN eval $(opam config env) && cd CompCert && git clean -dfx && git reset --hard && ./config_rv32.sh && make && make install
+
+RUN eval $(opam config env) && cd CompCert && git clean -dfx && git reset --hard && ./config_rv64.sh && make && make install
diff --git a/compcert_kvx_pruned.dockerfile b/compcert_kvx_pruned.dockerfile
new file mode 100644
index 00000000..c122cb83
--- /dev/null
+++ b/compcert_kvx_pruned.dockerfile
@@ -0,0 +1,5 @@
+FROM compcert_kvx
+USER root
+RUN apt-get -y install gcc && apt-get -y remove opam && apt-get -y autoremove
+RUN rm -rf /home/appuser/.opam /home/appuser/CompCert
+USER appuser
diff --git a/configure b/configure
index 1ec6d210..ee8a1577 100755
--- a/configure
+++ b/configure
@@ -584,9 +584,9 @@ esac
 echo "Testing OCaml... " | tr -d '\n'
 ocaml_ver=`ocamlc -version 2>/dev/null`
 case "$ocaml_ver" in
-  4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*)
+  4.00.*|4.01.*| 4.02.*|4.03.*|4.04.*|4.05.*)
         echo "version $ocaml_ver -- UNSUPPORTED"
-        echo "Error: CompCert requires OCaml version 4.05 or later."
+        echo "Error: CompCert requires OCaml version 4.06 or later."
         missingtools=true;;
   4.*)
         echo "version $ocaml_ver -- good!";;
diff --git a/make_docker.sh b/make_docker.sh
new file mode 100755
index 00000000..9665be4d
--- /dev/null
+++ b/make_docker.sh
@@ -0,0 +1,3 @@
+docker build -t compcert_build_env -f compcert_build_env.dockerfile .
+docker build -t compcert_kvx -f compcert_kvx.dockerfile .
+docker build -t compcert_kvx_pruned -f compcert_kvx_pruned.dockerfile .
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 4f67b9af..5d739375 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -22,13 +22,11 @@ open! Integers
 open Camlcoq
 open Option
 open AST
-open Printf
+open DebugPrint
 
 (** Mini CSE (a dynamic numbering is applied during expansion. 
     The CSE algorithm is inspired by the "static" one used in backend/CSE.v *)
 
-let exp_debug = false
-
 (** Managing virtual registers and node index *)
 
 let reg = ref 1
@@ -80,9 +78,9 @@ type numb = {
 }
 
 let print_list_pos l =
-  if exp_debug then eprintf "[";
-  List.iter (fun i -> if exp_debug then eprintf "%d;" (p2i i)) l;
-  if exp_debug then eprintf "]\n"
+  debug "[";
+  List.iter (fun i -> debug "%d;" (p2i i)) l;
+  debug "]\n"
 
 let empty_numbering () =
   { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 }
@@ -93,11 +91,11 @@ let rec get_nvalues vn = function
       let v =
         match Hashtbl.find_opt !vn.nreg r with
         | Some v ->
-            if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) v;
+            debug "getnval r=%d |-> v=%d\n" (p2i r) v;
             v
         | None ->
             let n = !vn.nnext in
-            if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) n;
+            debug "getnval r=%d |-> v=%d\n" (p2i r) n;
             !vn.nnext <- !vn.nnext + 1;
             Hashtbl.replace !vn.nreg r n;
             Hashtbl.replace !vn.nval n [ r ];
@@ -112,17 +110,17 @@ let get_nval_ornil vn v =
 let forget_reg vn rd =
   match Hashtbl.find_opt !vn.nreg rd with
   | Some v ->
-      if exp_debug then eprintf "forget_reg: r=%d |-> v=%d\n" (p2i rd) v;
+      debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v;
       let old_regs = get_nval_ornil vn v in
-      if exp_debug then eprintf "forget_reg: old_regs are:\n";
+      debug "forget_reg: old_regs are:\n";
       print_list_pos old_regs;
       Hashtbl.replace !vn.nval v
         (List.filter (fun n -> not (P.eq n rd)) old_regs)
   | None ->
-      if exp_debug then eprintf "forget_reg: no mapping for r=%d\n" (p2i rd)
+      debug "forget_reg: no mapping for r=%d\n" (p2i rd)
 
 let update_reg vn rd v =
-  if exp_debug then eprintf "update_reg: update v=%d with r=%d\n" v (p2i rd);
+  debug "update_reg: update v=%d with r=%d\n" v (p2i rd);
   forget_reg vn rd;
   let old_regs = get_nval_ornil vn v in
   Hashtbl.replace !vn.nval v (rd :: old_regs)
@@ -132,7 +130,7 @@ let rec find_valnum_rhs rh = function
   | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl
 
 let set_unknown vn rd =
-  if exp_debug then eprintf "set_unknown: rd=%d\n" (p2i rd);
+  debug "set_unknown: rd=%d\n" (p2i rd);
   forget_reg vn rd;
   Hashtbl.remove !vn.nreg rd
 
@@ -141,19 +139,19 @@ let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> ()
 let addrhs vn rd rh =
   match find_valnum_rhs rh !vn.seqs with
   | Some vres ->
-      if exp_debug then eprintf "addrhs: Some v=%d\n" vres;
+      debug "addrhs: Some v=%d\n" vres;
       Hashtbl.replace !vn.nreg rd vres;
       update_reg vn rd vres
   | None ->
       let n = !vn.nnext in
-      if exp_debug then eprintf "addrhs: None v=%d\n" n;
+      debug "addrhs: None v=%d\n" n;
       !vn.nnext <- !vn.nnext + 1;
       !vn.seqs <- Seq (n, rh) :: !vn.seqs;
       update_reg vn rd n;
       Hashtbl.replace !vn.nreg rd n
 
 let addsop vn v op rd =
-  if exp_debug then eprintf "addsop\n";
+  debug "addsop\n";
   if op = Omove then (
     update_reg vn rd (List.hd v);
     Hashtbl.replace !vn.nreg rd (List.hd v))
@@ -167,11 +165,11 @@ let rec kill_mem_operations = function
   | eq :: tl -> eq :: kill_mem_operations tl
 
 let reg_valnum vn v =
-  if exp_debug then eprintf "reg_valnum: trying to find a mapping for v=%d\n" v;
+  debug "reg_valnum: trying to find a mapping for v=%d\n" v;
   match Hashtbl.find !vn.nval v with
   | [] -> None
   | r :: rs ->
-      if exp_debug then eprintf "reg_valnum: found a mapping r=%d\n" (p2i r);
+      debug "reg_valnum: found a mapping r=%d\n" (p2i r);
       Some r
 
 let rec reg_valnums vn = function
@@ -216,7 +214,7 @@ let addinst vn op args rd =
   let rh = Sop (op, v) in
   match find_rhs vn rh with
   | Some r ->
-      if exp_debug then eprintf "addinst: rhs found with r=%d\n" (p2i r);
+      debug "addinst: rhs found with r=%d\n" (p2i r);
       Sr r
   | None ->
       addsop vn v op rd;
@@ -627,8 +625,7 @@ let get_regs_inst = function
 (** Modify pathmap according to the size of the expansion list *)
 
 let write_pathmap initial esize pm' =
-  if exp_debug then
-    eprintf "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize;
+  debug "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize;
   let path = get_some @@ PTree.get initial !pm' in
   let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in
   let path' =
@@ -655,7 +652,7 @@ let get_arguments vn vals args =
 (** Update the code tree with the expansion list *)
 
 let rec write_tree vn exp initial current code' new_order fturn =
-  if exp_debug then eprintf "wt: node is %d\n" !node;
+  debug "wt: node is %d\n" !node;
   let target_node, next_node =
     if fturn then (P.to_int initial, current) else (current, current - 1)
   in
@@ -685,7 +682,7 @@ let rec write_tree vn exp initial current code' new_order fturn =
 
 (** Main expansion function - TODO gourdinl to split? *)
 let expanse (sb : superblock) code pm =
-  if exp_debug then eprintf "#### New superblock for expansion oracle\n";
+  debug "#### New superblock for expansion oracle\n";
   let new_order = ref [] in
   let liveins = ref sb.liveins in
   let exp = ref [] in
@@ -699,129 +696,129 @@ let expanse (sb : superblock) code pm =
       was_branch := false;
       was_exp := false;
       let inst = get_some @@ PTree.get n code in
-      if exp_debug then eprintf "We are checking node %d\n" (p2i n);
+      debug "We are checking node %d\n" (p2i n);
       (match inst with
        (* Expansion of conditions - Ocmp *)
        | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccomp\n";
+           debug "Iop/Ccomp\n";
            exp := cond_int32s vn false c a1 a2 dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccompu\n";
+           debug "Iop/Ccompu\n";
            exp := cond_int32u vn false c a1 a2 dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccompimm\n";
+           debug "Iop/Ccompimm\n";
            exp := expanse_condimm_int32s vn c a1 imm dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccompuimm\n";
+           debug "Iop/Ccompuimm\n";
            exp := expanse_condimm_int32u vn c a1 imm dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccompl\n";
+           debug "Iop/Ccompl\n";
            exp := cond_int64s vn false c a1 a2 dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccomplu\n";
+           debug "Iop/Ccomplu\n";
            exp := cond_int64u vn false c a1 a2 dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccomplimm\n";
+           debug "Iop/Ccomplimm\n";
            exp := expanse_condimm_int64s vn c a1 imm dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccompluimm\n";
+           debug "Iop/Ccompluimm\n";
            exp := expanse_condimm_int64u vn c a1 imm dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccompf\n";
+           debug "Iop/Ccompf\n";
            exp := expanse_cond_fp vn false cond_float c f1 f2 dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Cnotcompf\n";
+           debug "Iop/Cnotcompf\n";
            exp := expanse_cond_fp vn true cond_float c f1 f2 dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ccompfs\n";
+           debug "Iop/Ccompfs\n";
            exp := expanse_cond_fp vn false cond_single c f1 f2 dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Cnotcompfs\n";
+           debug "Iop/Cnotcompfs\n";
            exp := expanse_cond_fp vn true cond_single c f1 f2 dest;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        (* Expansion of branches - Ccomp *)
        | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccomp\n";
+           debug "Icond/Ccomp\n";
            exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
            was_branch := true;
            was_exp := true
        | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccompu\n";
+           debug "Icond/Ccompu\n";
            exp := cbranch_int32u false c a1 a2 info succ1 succ2 [];
            was_branch := true;
            was_exp := true
        | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccompimm\n";
+           debug "Icond/Ccompimm\n";
            exp := expanse_cbranchimm_int32s vn c a1 imm info succ1 succ2;
            was_branch := true;
            was_exp := true
        | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccompuimm\n";
+           debug "Icond/Ccompuimm\n";
            exp := expanse_cbranchimm_int32u vn c a1 imm info succ1 succ2;
            was_branch := true;
            was_exp := true
        | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccompl\n";
+           debug "Icond/Ccompl\n";
            exp := cbranch_int64s false c a1 a2 info succ1 succ2 [];
            was_branch := true;
            was_exp := true
        | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccomplu\n";
+           debug "Icond/Ccomplu\n";
            exp := cbranch_int64u false c a1 a2 info succ1 succ2 [];
            was_branch := true;
            was_exp := true
        | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccomplimm\n";
+           debug "Icond/Ccomplimm\n";
            exp := expanse_cbranchimm_int64s vn c a1 imm info succ1 succ2;
            was_branch := true;
            was_exp := true
        | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccompluimm\n";
+           debug "Icond/Ccompluimm\n";
            exp := expanse_cbranchimm_int64u vn c a1 imm info succ1 succ2;
            was_branch := true;
            was_exp := true
        | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccompf\n";
+           debug "Icond/Ccompf\n";
            exp :=
              expanse_cbranch_fp vn false cond_float c f1 f2 info succ1 succ2;
            was_branch := true;
            was_exp := true
        | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Cnotcompf\n";
+           debug "Icond/Cnotcompf\n";
            exp := expanse_cbranch_fp vn true cond_float c f1 f2 info succ1 succ2;
            was_branch := true;
            was_exp := true
        | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Ccompfs\n";
+           debug "Icond/Ccompfs\n";
            exp :=
              expanse_cbranch_fp vn false cond_single c f1 f2 info succ1 succ2;
            was_branch := true;
            was_exp := true
        | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
-           if exp_debug then eprintf "Icond/Cnotcompfs\n";
+           debug "Icond/Cnotcompfs\n";
            exp :=
              expanse_cbranch_fp vn true cond_single c f1 f2 info succ1 succ2;
            was_branch := true;
@@ -830,7 +827,7 @@ let expanse (sb : superblock) code pm =
       (if not !was_exp then
        match inst with
        | Iop (Ofloatconst f, nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ofloatconst\n";
+           debug "Iop/Ofloatconst\n";
            let r = r2pi () in
            let l = loadimm64 vn r (Floats.Float.to_bits f) in
            let r', l' = extract_arg l in
@@ -838,7 +835,7 @@ let expanse (sb : superblock) code pm =
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Osingleconst f, nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Osingleconst\n";
+           debug "Iop/Osingleconst\n";
            let r = r2pi () in
            let l = loadimm32 vn r (Floats.Float32.to_bits f) in
            let r', l' = extract_arg l in
@@ -846,57 +843,57 @@ let expanse (sb : superblock) code pm =
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ointconst n, nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ointconst\n";
+           debug "Iop/Ointconst\n";
            exp := loadimm32 vn dest n;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Olongconst n, nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Olongconst\n";
+           debug "Iop/Olongconst\n";
            exp := loadimm64 vn dest n;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Oaddimm n, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Oaddimm\n";
+           debug "Iop/Oaddimm\n";
            exp := addimm32 vn a1 dest n None;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Oaddlimm n, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Oaddlimm\n";
+           debug "Iop/Oaddlimm\n";
            exp := addimm64 vn a1 dest n None;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Oandimm n, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Oandimm\n";
+           debug "Iop/Oandimm\n";
            exp := andimm32 vn a1 dest n;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Oandlimm n, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Oandlimm\n";
+           debug "Iop/Oandlimm\n";
            exp := andimm64 vn a1 dest n;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Oorimm n, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Oorimm\n";
+           debug "Iop/Oorimm\n";
            exp := orimm32 vn a1 dest n;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Oorlimm n, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Oorlimm\n";
+           debug "Iop/Oorlimm\n";
            exp := orimm64 vn a1 dest n;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Oxorimm n, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Oxorimm\n";
+           debug "Iop/Oxorimm\n";
            exp := xorimm32 vn a1 dest n;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Oxorlimm n, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Oxorlimm\n";
+           debug "Iop/Oxorlimm\n";
            exp := xorimm64 vn a1 dest n;
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocast8signed, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/cast8signed\n";
+           debug "Iop/cast8signed\n";
            let op = Oshlimm (Int.repr (Z.of_sint 24)) in
            let r = r2pi () in
            let i1 = addinst vn op [ a1 ] r in
@@ -906,7 +903,7 @@ let expanse (sb : superblock) code pm =
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocast16signed, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/cast16signed\n";
+           debug "Iop/cast16signed\n";
            let op = Oshlimm (Int.repr (Z.of_sint 16)) in
            let r = r2pi () in
            let i1 = addinst vn op [ a1 ] r in
@@ -916,7 +913,7 @@ let expanse (sb : superblock) code pm =
            exp := extract_final vn !exp dest succ;
            was_exp := true
        | Iop (Ocast32unsigned, a1 :: nil, dest, succ) ->
-           if exp_debug then eprintf "Iop/Ocast32unsigned\n";
+           debug "Iop/Ocast32unsigned\n";
            let r1 = r2pi () in
            let r2 = r2pi () in
            let op1 = Ocast32signed in
@@ -933,10 +930,10 @@ let expanse (sb : superblock) code pm =
            was_exp := true
        | Iop (Oshrximm n, a1 :: nil, dest, succ) ->
            if Int.eq n Int.zero then (
-             if exp_debug then eprintf "Iop/Oshrximm1\n";
+             debug "Iop/Oshrximm1\n";
              exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ])
            else if Int.eq n Int.one then (
-             if exp_debug then eprintf "Iop/Oshrximm2\n";
+             debug "Iop/Oshrximm2\n";
              let r1 = r2pi () in
              let r2 = r2pi () in
              let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in
@@ -952,7 +949,7 @@ let expanse (sb : superblock) code pm =
              let r3, l3 = extract_arg (i3 :: l2) in
              exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3)
            else (
-             if exp_debug then eprintf "Iop/Oshrximm3\n";
+             debug "Iop/Oshrximm3\n";
              let r1 = r2pi () in
              let r2 = r2pi () in
              let r3 = r2pi () in
@@ -976,10 +973,10 @@ let expanse (sb : superblock) code pm =
            was_exp := true
        | Iop (Oshrxlimm n, a1 :: nil, dest, succ) ->
            if Int.eq n Int.zero then (
-             if exp_debug then eprintf "Iop/Oshrxlimm1\n";
+             debug "Iop/Oshrxlimm1\n";
              exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ])
            else if Int.eq n Int.one then (
-             if exp_debug then eprintf "Iop/Oshrxlimm2\n";
+             debug "Iop/Oshrxlimm2\n";
              let r1 = r2pi () in
              let r2 = r2pi () in
              let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in
@@ -995,7 +992,7 @@ let expanse (sb : superblock) code pm =
              let r3, l3 = extract_arg (i3 :: l2) in
              exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3)
            else (
-             if exp_debug then eprintf "Iop/Oshrxlimm3\n";
+             debug "Iop/Oshrxlimm3\n";
              let r1 = r2pi () in
              let r2 = r2pi () in
              let r3 = r2pi () in
diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v
index 5b34dc16..2f73f1fa 100644
--- a/scheduling/RTLpath.v
+++ b/scheduling/RTLpath.v
@@ -27,8 +27,6 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
 Require Import RTL Linking.
 
-Declare Scope option_monad_scope.
-
 Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end)
          (at level 200, X ident, A at level 100, B at level 200)
          : option_monad_scope.
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v
index c3266db9..4bb3e18e 100644
--- a/scheduling/RTLpathSE_simu_specs.v
+++ b/scheduling/RTLpathSE_simu_specs.v
@@ -105,13 +105,12 @@ with hsmem_proj hm :=
   | HSstore hm chk addr hl hv _ => Sstore (hsmem_proj hm) chk addr (hsval_list_proj hl) (hsval_proj hv)
   end.
 
-Declare Scope hse.
-Local Open Scope hse.
-
-
 (** We use a Notation instead a Definition, in order to get more automation "for free" *)
 Notation "'seval_hsval' ge sp hsv" := (seval_sval ge sp (hsval_proj hsv))
   (only parsing, at level 0, ge at next level, sp at next level, hsv at next level): hse.
+
+Local Open Scope hse.
+
 Notation "'seval_list_hsval' ge sp lhv" := (seval_list_sval ge sp (hsval_list_proj lhv))
   (only parsing, at level 0, ge at next level, sp at next level, lhv at next level): hse.
 Notation "'seval_hsmem' ge sp hsm" := (seval_smem ge sp (hsmem_proj hsm))
diff --git a/scheduling/abstractbb/AbstractBasicBlocksDef.v b/scheduling/abstractbb/AbstractBasicBlocksDef.v
index 34d72de1..fec716c4 100644
--- a/scheduling/abstractbb/AbstractBasicBlocksDef.v
+++ b/scheduling/abstractbb/AbstractBasicBlocksDef.v
@@ -273,8 +273,6 @@ with list_term :=
 Scheme term_mut := Induction for term Sort Prop
 with list_term_mut := Induction for list_term Sort Prop.
 
-Declare Scope pattern_scope.
-Declare Scope term_scope.
 Bind Scope pattern_scope with term.
 Delimit Scope term_scope with term.
 Delimit Scope pattern_scope with pattern.
diff --git a/test/monniaux/profiling/compcert_profiling.dat b/test/monniaux/profiling/compcert_profiling.dat
index fa57a995..bd2f90da 100644
--- a/test/monniaux/profiling/compcert_profiling.dat
+++ b/test/monniaux/profiling/compcert_profiling.dat
diff --git a/test/monniaux/profiling/test_profiling b/test/monniaux/profiling/test_profiling
index b530aae2..33e22d11 100755
--- a/test/monniaux/profiling/test_profiling
+++ b/test/monniaux/profiling/test_profiling