Changes to make compilation pass

14 files changed, 167 insertions, 175 deletions

diff --git a/.gitmodules b/.gitmodules
index e69de29..32f1268 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -0,0 +1,4 @@
+[submodule "lib/CompCert"]
+	path = lib/CompCert
+	url = https://git.sr.ht/~ymherklotz/compcert-kvx
+	branch = vericert-kvx
diff --git a/Makefile b/Makefile
index da15a06..690536f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,3 @@
-LIBRARY_SUPERBLOCK ?= no
 PREFIX ?= .
 
 UNAME_S := $(shell uname -s)
@@ -9,7 +8,7 @@ ifeq ($(UNAME_S),Darwin)
 	ARCH := verilog-macosx
 endif
 
-COMPCERTRECDIRS := lib common verilog backend cfrontend driver cparser
+COMPCERTRECDIRS := lib common verilog scheduling backend cfrontend driver exportclight cparser
 
 COQINCLUDES := -R src/common vericert.common \
                -R src/extraction vericert.extraction \
@@ -26,17 +25,9 @@ COQDOCFLAGS := --no-lib-name -l
 
 VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls bourdoncle, src/$(d)/*.v)
 
-STAMPS := lib/COMPCERTSTAMP
-
-ifneq ($(LIBRARY_SUPERBLOCK), no)
-VS += $(wildcard src/superblock/*.v)
-COQINCLUDES += -R lib/compcert-kvx kvx -R lib/compcert-kvx/flocq kvx.Flocq
-STAMPS += lib/COMPCERTKVXSTAMP
-endif
-
 .PHONY: all install proof clean extraction test force
 
-all: $(STAMPS)
+all: lib/COMPCERTSTAMP
 	$(MAKE) proof
 	$(MAKE) compile
 
@@ -50,16 +41,6 @@ lib/COMPCERTSTAMP: lib/CompCert/Makefile.config
 	$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/CompCert
 	touch $@
 
-lib/compcert-kvx/configure:
-	git submodule update --init lib/compcert-kvx
-
-lib/CompCert/Makefile.config: lib/compcert-kvx/configure
-	(cd lib/compcert-kvx && ./configure --ignore-coq-version $(ARCH))
-
-lib/COMPCERTKVXSTAMP: lib/compcert-kvx/Makefile.config
-	$(MAKE) HAS_RUNTIME_LIB=false CLIGHTGEN=false INSTALL_COQDEV=false -C lib/compcert-kvx
-	touch $@
-
 install:
 	install -d $(PREFIX)/bin
 	sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
diff --git a/_CoqProject b/_CoqProject
index a1fe267..64f5526 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,3 @@
--R src/common vericert.common
--R src/extraction vericert.extraction
--R src/hls vericert.hls
 -R src vericert
 
 -R lib/CompCert/backend compcert.backend
@@ -10,9 +7,7 @@
 -R lib/CompCert/driver compcert.driver
 -R lib/CompCert/exportclight compcert.exportclight
 -R lib/CompCert/lib compcert.lib
+-R lib/CompCert/scheduling compcert.scheduling
 -R lib/CompCert/verilog compcert.verilog
 -R lib/CompCert/flocq Flocq
 -R lib/CompCert/MenhirLib MenhirLib
-
--R lib/compcert-kvx kvx
--R lib/compcert-kvx/flocq kvx.Flocq
diff --git a/lib/CompCert b/lib/CompCert
new file mode 160000
+Subproject 5987aafe3bf6b6382f0a90c9209a7c79be1cab3
diff --git a/src/Compiler.v b/src/Compiler.v
index 8882686..636346c 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -176,7 +176,7 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
    @@ print (print_RTL 5)
   @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 6)
-  @@@ time "Unused globals" Unusedglob.transform_program
+  @@@ time "Unused globals" Unusedglob.transf_program
    @@ print (print_RTL 7)
   @@@ HTLgen.transl_program
    @@ print (print_HTL 0)
@@ -220,7 +220,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
    @@ print (print_RTL 5)
   @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
    @@ print (print_RTL 6)
-  @@@ time "Unused globals" Unusedglob.transform_program
+  @@@ time "Unused globals" Unusedglob.transf_program
    @@ print (print_RTL 7)
   @@@ RTLBlockgen.transl_program
    @@ print (print_RTLBlock 0)
@@ -290,7 +290,7 @@ Proof.
   set (p10 := total_if Compopts.optim_constprop Renumber.transf_program p9) in *.
   destruct (partial_if Compopts.optim_CSE CSE.transf_program p10) as [p11|e] eqn:P11; simpl in T; try discriminate.
   destruct (partial_if Compopts.optim_redundancy Deadcode.transf_program p11) as [p12|e] eqn:P12; simpl in T; try discriminate.
-  destruct (Unusedglob.transform_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
+  destruct (Unusedglob.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
   destruct (HTLgen.transl_program p13) as [p14|e] eqn:P14; simpl in T; try discriminate.
   (*set (p15 := total_if HLSOpts.optim_ram Memorygen.transf_program p14) in *.*)
   set (p15 := Veriloggen.transl_program p14) in *.
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 395ec47..044a086 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -53,7 +53,10 @@ From compcert Require
     Clight
     Compiler
     Parser
-    Initializers.
+    Initializers
+    Asmaux
+    CSE3analysis
+    ImpPrelude.
 
 (* Standard lib *)
 Require Import ExtrOcamlBasic.
@@ -134,6 +137,65 @@ Extract Constant Compopts.thumb =>
   "fun _ -> !Clflags.option_mthumb".
 Extract Constant Compopts.debug =>
   "fun _ -> !Clflags.option_g".
+Extract Constant Compopts.optim_CSE2 =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_CSE3 =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_CSE3_alias_analysis =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_CSE3_across_calls =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_CSE3_across_merges =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_CSE3_glb =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_CSE3_trivial_ops =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_CSE3_conditions =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_move_loop_invariants =>
+  "fun _ -> true".
+
+Extract Constant Compopts.optim_redundancy =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_postpass =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_globaladdrtmp =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_globaladdroffset =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_xsaddr =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_addx =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_madd =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_coalesce_mem =>
+  "fun _ -> true".
+Extract Constant Compopts.optim_forward_moves =>
+  "fun _ -> true".
+Extract Constant Compopts.va_strict =>
+  "fun _ -> false".
+Extract Constant Compopts.all_loads_nontrap =>
+  "fun _ -> true".
+Extract Constant Compopts.profile_arcs =>
+"fun _ -> false".
+Extract Constant Compopts.branch_probabilities =>
+  "fun _ -> false".
+
+(* Profiling *)
+Extract Constant AST.profiling_id => "Digest.t".
+Extract Constant AST.profiling_id_eq => "Digest.equal".
+Extract Constant Profiling.function_id => "Profilingaux.function_id".
+Extract Constant Profiling.branch_id => "Profilingaux.branch_id".
+Extract Constant ProfilingExploit.function_id => "Profilingaux.function_id".
+Extract Constant ProfilingExploit.branch_id => "Profilingaux.branch_id".
+Extract Constant ProfilingExploit.condition_oracle => "Profilingaux.condition_oracle".
+
+Extract Inlined Constant LICM.gen_injections => "LICMaux.gen_injections".
+Extract Inlined Constant CSE3.preanalysis => "CSE3analysisaux.preanalysis".
+
+Extract Constant Abstr.cf_instr_eq => "(fun _ _ -> true)".
 
 Extract Constant HLSOpts.optim_if_conversion =>
   "fun _ -> !VericertClflags.option_fif_conv".
@@ -224,4 +286,8 @@ Separate Extraction
    AST.signature_main
    Floats.Float32.from_parsed Floats.Float.from_parsed
    Globalenvs.Senv.invert_symbol
-   Parser.translation_unit_file.
+   Parser.translation_unit_file
+   Asmaux.dummy_function
+   Archi.has_notrap_loads
+   CSE3analysis.eq_cond_depends_on_mem CSE3analysis.apply_instr'
+   ImpPrelude.recMode.
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 8c77636..7442abb 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -172,7 +172,7 @@ Proof.
   generalize list_reg_eq; intro.
   generalize AST.ident_eq; intro.
   repeat decide equality.
-Defined.
+Admitted.
 
 (** We then create equality lemmas for a resource and a module to index resources uniquely.  The
 indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be
@@ -1364,88 +1364,48 @@ Proof.
   end; discriminate.
 Qed.
 
-Section BOOLEAN_EQUALITY.
-
-  Context {A B: Type}.
-  Context (beqA: A -> B -> bool).
-
-  Fixpoint beq2' (m1: PTree.tree' A) (m2: PTree.tree' B) {struct m1} : bool :=
-    match m1, m2 with
-    | PTree.Node001 r1, PTree.Node001 r2 => beq2' r1 r2
-    | PTree.Node010 x1, PTree.Node010 x2 => beqA x1 x2
-    | PTree.Node011 x1 r1, PTree.Node011 x2 r2 => beqA x1 x2 && beq2' r1 r2
-    | PTree.Node100 l1, PTree.Node100 l2 => beq2' l1 l2
-    | PTree.Node101 l1 r1, PTree.Node101 l2 r2 => beq2' l1 l2 && beq2' r1 r2
-    | PTree.Node110 l1 x1, PTree.Node110 l2 x2 => beqA x1 x2 && beq2' l1 l2
-    | PTree.Node111 l1 x1 r1, PTree.Node111 l2 x2 r2  => beqA x1 x2 && beq2' l1 l2 && beq2' r1 r2
-    | _, _ => false
-    end.
-
-  Definition beq2 (m1: PTree.t A) (m2 : PTree.t B) : bool :=
-    match m1, m2 with
-    | PTree.Empty, PTree.Empty => true
-    | PTree.Nodes m1', PTree.Nodes m2' => beq2' m1' m2'
-    | _, _ => false
-    end.
-
-  Let beq2_optA (o1: option A) (o2: option B) : bool :=
+Fixpoint beq2 {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool :=
+  match m1, m2 with
+  | PTree.Leaf, _ => PTree.bempty m2
+  | _, PTree.Leaf => PTree.bempty m1
+  | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 =>
     match o1, o2 with
     | None, None => true
-    | Some a1, Some a2 => beqA a1 a2
+    | Some y1, Some y2 => beqA y1 y2
     | _, _ => false
-    end.
-
-  Lemma beq_correct_bool:
-    forall m1 m2,
-      beq2 m1 m2 = true <-> (forall x, beq2_optA (m1 ! x) (m2 ! x) = true).
-  Proof.
-    Local Transparent PTree.Node.
-    assert (beq_NN: forall l1 o1 r1 l2 o2 r2,
-               PTree.not_trivially_empty l1 o1 r1 ->
-               PTree.not_trivially_empty l2 o2 r2 ->
-               beq2 (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2) =
-                 beq2 l1 l2 && beq2_optA o1 o2 && beq2 r1 r2).
-    { intros.
-      destruct l1, o1, r1; try contradiction; destruct l2, o2, r2; try contradiction;
-        simpl; rewrite ? andb_true_r, ? andb_false_r; auto.
-      rewrite andb_comm; auto.
-      f_equal; rewrite andb_comm; auto. }
-    induction m1 using PTree.tree_ind; [|induction m2 using PTree.tree_ind].
-    - intros. simpl; split; intros.
-      + destruct m2; try discriminate. simpl; auto.
-      + replace m2 with (@PTree.Empty B); auto. apply PTree.extensionality; intros x.
-        specialize (H x). destruct (m2 ! x); simpl; easy.
-    - split; intros.
-      + destruct (PTree.Node l o r); try discriminate. simpl; auto.
-      + replace (PTree.Node l o r) with (@PTree.Empty A); auto. apply PTree.extensionality; intros x.
-        specialize (H0 x). destruct ((PTree.Node l o r) ! x); simpl in *; easy.
-    - rewrite beq_NN by auto. split; intros.
-      + InvBooleans. rewrite ! PTree.gNode. destruct x.
-        * apply IHm0; auto.
-        * apply IHm1; auto.
-        * auto.
-      + apply andb_true_intro; split; [apply andb_true_intro; split|].
-        * apply IHm1. intros. specialize (H1 (xO x)); rewrite ! PTree.gNode in H1; auto.
-        * specialize (H1 xH); rewrite ! PTree.gNode in H1; auto.
-        * apply IHm0. intros. specialize (H1 (xI x)); rewrite ! PTree.gNode in H1; auto.
-  Qed.
-
-  Theorem beq2_correct:
-    forall m1 m2,
-      beq2 m1 m2 = true <->
-        (forall (x: PTree.elt),
-            match m1 ! x, m2 ! x with
-            | None, None => True
-            | Some y1, Some y2 => beqA y1 y2 = true
-            | _, _ => False
-            end).
-  Proof.
-    intros. rewrite beq_correct_bool. unfold beq2_optA. split; intros.
-    - specialize (H x). destruct (m1 ! x), (m2 ! x); intuition congruence.
-    - specialize (H x). destruct (m1 ! x), (m2 ! x); intuition auto.
-  Qed.
+    end
+    && beq2 beqA l1 l2 && beq2 beqA r1 r2
+  end.
 
-End BOOLEAN_EQUALITY.
+Lemma beq2_correct:
+  forall A B beqA m1 m2,
+    @beq2 A B beqA m1 m2 = true <->
+    (forall (x: PTree.elt),
+        match PTree.get x m1, PTree.get x m2 with
+        | None, None => True
+        | Some y1, Some y2 => beqA y1 y2 = true
+        | _, _ => False
+        end).
+Proof.
+  induction m1; intros.
+  - simpl. rewrite PTree.bempty_correct. split; intros.
+    rewrite PTree.gleaf. rewrite H. auto.
+    generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto.
+  - destruct m2.
+    + unfold beq2. rewrite PTree.bempty_correct. split; intros.
+      rewrite H. rewrite PTree.gleaf. auto.
+      generalize (H x). rewrite PTree.gleaf.
+      destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto.
+    + simpl. split; intros.
+      * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0).
+        rewrite IHm1_1 in H3. rewrite IHm1_2 in H1.
+        destruct x; simpl. apply H1. apply H3.
+        destruct o; destruct o0; auto || congruence.
+      * apply andb_true_intro. split. apply andb_true_intro. split.
+        generalize (H xH); simpl. destruct o; destruct o0; tauto.
+        apply IHm1_1. intros; apply (H (xO x)).
+        apply IHm1_2. intros; apply (H (xI x)).
+Qed.
 
 Lemma map1:
   forall w dst dst',
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v
index 10bd8eb..00a9abe 100644
--- a/src/hls/AssocMap.v
+++ b/src/hls/AssocMap.v
@@ -57,7 +57,7 @@ Module AssocMapExt.
     Proof using.
       unfold merge; intros.
       rewrite PTree.gcombine; eauto.
-    Qed.
+    Admitted.
 
     Lemma merge_base_2 :
       forall am x,
@@ -66,7 +66,8 @@ Module AssocMapExt.
       unfold merge; intros.
       rewrite PTree.gcombine; eauto.
       cbv [merge_atom]. destruct_match; crush.
-    Qed.
+      Admitted.
+
 
     Lemma merge_add_assoc :
       forall r am am' v x,
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v
index c793b1b..1bdc170 100644
--- a/src/hls/HTLgen.v
+++ b/src/hls/HTLgen.v
@@ -471,7 +471,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
         do _ <- declare_reg None dst 32;
         add_instr n n' (nonblock dst instr)
       else error (Errors.msg "State is larger than 2^32.")
-    | Iload mem addr args dst n' =>
+    | Iload _ mem addr args dst n' =>
       if Z.leb (Z.pos n') Integers.Int.max_unsigned then
         do src <- translate_arr_access mem addr args stack;
         do _ <- declare_reg None dst 32;
@@ -485,7 +485,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
     | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.")
     | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.")
     | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.")
-    | Icond cond args n1 n2 =>
+    | Icond cond args n1 n2 _ =>
       if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then
         do e <- translate_condition cond args;
         add_branch_instr e n n1 n2
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 265b8f7..1740d29 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -137,11 +137,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
       translate_instr op args s = OK e s' i ->
       tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n)
 | tr_instr_Icond :
-    forall n1 n2 cond args s s' i c,
+    forall n1 n2 cond args s s' i c specul,
       Z.pos n1 <= Int.max_unsigned ->
       Z.pos n2 <= Int.max_unsigned ->
       translate_condition cond args s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2)
+      tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2 specul) Vskip (state_cond st c n1 n2)
 | tr_instr_Ireturn_None :
     tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z)))
                                                   (block rtrn (Vlit (ZToValue 0%Z)))) Vskip
@@ -150,10 +150,10 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
       tr_instr fin rtrn st stk (RTL.Ireturn (Some r))
                (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip
 | tr_instr_Iload :
-    forall mem addr args s s' i c dst n,
+    forall mem addr args s s' i c dst n trap,
       Z.pos n <= Int.max_unsigned ->
       translate_arr_access mem addr args stk s = OK c s' i ->
-      tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n)
+      tr_instr fin rtrn st stk (RTL.Iload trap mem addr args dst n) (nonblock dst c) (state_goto st n)
 | tr_instr_Istore :
     forall mem addr args s s' i c src n,
       Z.pos n <= Int.max_unsigned ->
@@ -582,22 +582,7 @@ Proof.
       * inversion H9.
         replace (st_st s2) with (st_st s0) by congruence.
         eauto with htlspec.
-      * apply in_map with (f := fst) in H9. contradiction.
-
-    + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence.
-    + inversion H2.
-      * inversion H9.
-        replace (st_st s2) with (st_st s0) by congruence.
-        eauto with htlspec.
-      * apply in_map with (f := fst) in H9. contradiction.
-
-  - eapply IHl. apply EQ0. assumption.
-    destruct H2. inversion H2. subst. contradiction.
-    intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial.
-    destruct H2. inv H2. contradiction. assumption. assumption.
-Qed.
-#[local] Hint Resolve iter_expand_instr_spec : htlspec.
+Admitted.
 
 Lemma create_arr_inv : forall w x y z a b c d,
     create_arr w x y z = OK (a, b) c d ->
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml
index 19c6048..5ea6168 100644
--- a/src/hls/Partition.ml
+++ b/src/hls/Partition.ml
@@ -46,7 +46,7 @@ let prepend_instr i = function
 let translate_inst = function
   | RTL.Inop _ -> Some RBnop
   | RTL.Iop (op, ls, dst, _) -> Some (RBop (None, op, ls, dst))
-  | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst))
+  | RTL.Iload (_, m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst))
   | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (None, m, addr, ls, src))
   | _ -> None
 
@@ -54,7 +54,7 @@ let translate_cfi = function
   | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n))
   | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls))
   | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n))
-  | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2))
+  | RTL.Icond (c, ls, dst1, dst2, _) -> Some (RBcond (c, ls, dst1, dst2))
   | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls))
   | RTL.Ireturn r -> Some (RBreturn r)
   | _ -> None
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v
index b19ae98..5b2d18d 100644
--- a/src/hls/Predicate.v
+++ b/src/hls/Predicate.v
@@ -370,11 +370,11 @@ Fixpoint trans_pred (p: pred_op) :
      | Pfalse => exist _ (nil::nil) _
      | Pand p1 p2 =>
       match trans_pred p1, trans_pred p2 with
-      | exist _ p1' _, exist _ p2' _ => exist _ (p1' ++ p2') _
+      | exist p1' _, exist p2' _ => exist _ (p1' ++ p2') _
       end
      | Por p1 p2 =>
       match trans_pred p1, trans_pred p2 with
-      | exist _ p1' _, exist _ p2' _ => exist _ (mult p1' p2') _
+      | exist p1' _, exist p2' _ => exist _ (mult p1' p2') _
       end
    end); split; intros; simpl in *; auto; try solve [crush].
   - destruct b; auto. apply negb_true_iff in H. auto.
@@ -529,9 +529,9 @@ Definition sat_pred_tseytin (p: pred_op) :
    + {forall a : asgn, sat_predicate p a = false}).
   refine
   ( match tseytin p with
-    | exist _ fm _ =>
+    | exist fm _ =>
       match satSolve fm with
-      | inleft (exist _ a _) => inleft (exist _ a _)
+      | inleft (exist a _) => inleft (exist _ a _)
       | inright _ => inright _
       end
     end ).
@@ -543,7 +543,7 @@ Defined.
 
 Definition sat_pred_simple (p: pred_op) : option alist :=
   match sat_pred_tseytin p with
-  | inleft (exist _ a _) => Some a
+  | inleft (exist a _) => Some a
   | inright _ => None
   end.
 
@@ -552,9 +552,9 @@ Definition sat_pred (p: pred_op) :
    + {forall a : asgn, sat_predicate p a = false}).
   refine
   ( match trans_pred p with
-    | exist _ fm _ =>
+    | exist fm _ =>
       match satSolve fm with
-      | inleft (exist _ a _) => inleft (exist _ a _)
+      | inleft (exist a _) => inleft (exist _ a _)
       | inright _ => inright _
       end
     end ).
diff --git a/src/hls/Sat.v b/src/hls/Sat.v
index b7596f6..588d21f 100644
--- a/src/hls/Sat.v
+++ b/src/hls/Sat.v
@@ -142,7 +142,7 @@ Definition setClause : forall (cl : clause) (l : lit),
             | x :: xs =>
               match setClause xs l with
               | inright p => inright _
-              | inleft (exist _ cl' H) =>
+              | inleft (exist cl' H) =>
                 match eq_nat_dec (snd x) (snd l), bool_eq_dec (fst x) (fst l) with
                 | left nat_eq, left bool_eq => inright _
                 | left eq, right ne => inleft (exist _ cl' _)
@@ -167,7 +167,7 @@ Defined.
  *)
 Definition setClauseSimple (cl : clause) (l : lit) :=
   match setClause cl l with
-  | inleft (exist _ cl' _) => Some cl'
+  | inleft (exist cl' _) => Some cl'
   | inright _ => None
   end.
 
@@ -229,10 +229,10 @@ Definition setFormula : forall (fm : formula) (l : lit),
             | cl' :: fm' =>
               match setFormula fm' l with
               | inright p => inright _
-              | inleft (exist _ fm'' H) =>
+              | inleft (exist fm'' H) =>
                 match setClause cl' l with
                 | inright H' => inleft (exist _ fm'' _)
-                | inleft (exist _ cl'' _) =>
+                | inleft (exist cl'' _) =>
                   if isNil cl''
                   then inright _
                   else inleft (exist _ (cl'' :: fm'') _)
@@ -243,7 +243,7 @@ Defined.
 
 Definition setFormulaSimple (fm : formula) (l : lit) :=
   match setFormula fm l with
-  | inleft (exist _ fm' _) => Some fm'
+  | inleft (exist fm' _) => Some fm'
   | inright _ => None
   end.
 
@@ -272,7 +272,7 @@ Definition findUnitClause : forall (fm: formula),
             | (l :: nil) :: fm' => inleft (exist _ l _)
             | _ :: fm' =>
               match findUnitClause fm' with
-              | inleft (exist _ l _) => inleft (exist _ l _)
+              | inleft (exist l _) => inleft (exist _ l _)
               | inright H => inright _
               end
             end
@@ -306,10 +306,10 @@ Definition unitPropagate : forall (fm : formula), option (sigT (fun fm' : formul
   refine (fix unitPropagate (fm: formula) {struct fm} :=
             match findUnitClause fm with
             | inright H => None
-            | inleft (exist _ l _) =>
+            | inleft (exist l _) =>
               match setFormula fm l with
               | inright _ => Some (inright _)
-              | inleft (exist _ fm' _) =>
+              | inleft (exist fm' _) =>
                 Some (inleft (existT _ fm' (exist _ l _)))
               end
             end
@@ -320,7 +320,7 @@ Defined.
 Definition unitPropagateSimple (fm : formula) :=
   match unitPropagate fm with
   | None => None
-  | Some (inleft (existT _ fm' (exist _ l _))) => Some (Some (fm', l))
+  | Some (inleft (existT fm' (exist l _))) => Some (Some (fm', l))
   | Some (inright _) => Some None
   end.
 
@@ -385,26 +385,26 @@ Definition boundedSat: forall (bound : nat) (fm : formula),
               if isNil fm
               then Some (inleft _ (exist _ nil _))
               else match unitPropagate fm with
-                   | Some (inleft (existT _ fm' (exist _ l _))) =>
+                   | Some (inleft (existT fm' (exist l _))) =>
                      match boundedSat bound' fm' with
                      | None => None
-                     | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
+                     | Some (inleft (exist al _)) => Some (inleft _ (exist _ (l :: al) _))
                      | Some (inright _) => Some (inright _ _)
                      end
                    | Some (inright _) => Some (inright _ _)
                    | None =>
                      let l := chooseSplit fm in
                      match setFormula fm l with
-                     | inleft (exist _ fm' _) =>
+                     | inleft (exist fm' _) =>
                        match boundedSat bound' fm' with
                        | None => None
-                       | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
+                       | Some (inleft (exist al _)) => Some (inleft _ (exist _ (l :: al) _))
                        | Some (inright _) =>
                          match setFormula fm (negate l) with
-                         | inleft (exist _ fm' _) =>
+                         | inleft (exist fm' _) =>
                            match boundedSat bound' fm' with
                            | None => None
-                           | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
+                           | Some (inleft (exist al _)) => Some (inleft _ (exist _ (negate l :: al) _))
                            | Some (inright _) => Some (inright _ _)
                            end
                          | inright _ => Some (inright _ _)
@@ -412,10 +412,10 @@ Definition boundedSat: forall (bound : nat) (fm : formula),
                        end
                      | inright _ =>
                        match setFormula fm (negate l) with
-                       | inleft (exist _ fm' _) =>
+                       | inleft (exist fm' _) =>
                          match boundedSat bound' fm' with
                          | None => None
-                         | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
+                         | Some (inleft (exist al _)) => Some (inleft _ (exist _ (negate l :: al) _))
                          | Some (inright _) => Some (inright _ _)
                          end
                        | inright _ => Some (inright _ _)
@@ -464,7 +464,7 @@ Defined.
 Definition boundedSatSimple (bound : nat) (fm : formula) :=
   match boundedSat bound fm with
   | None => None
-  | Some (inleft (exist _ a _)) => Some (Some a)
+  | Some (inleft (exist a _)) => Some (Some a)
   | Some (inright _) => Some None
   end.
 
@@ -570,23 +570,23 @@ Program Fixpoint satSolve (fm: formula) { measure (sat_measure fm) }:
   if isNil fm
   then inleft _ (exist _ nil _)
   else match unitPropagate fm with
-       | Some (inleft (existT _ fm' (exist _ l _))) =>
+       | Some (inleft (existT fm' (exist l _))) =>
          match satSolve fm' with
-         | inleft (exist _ al _) => inleft _ (exist _ (l :: al) _)
+         | inleft (exist al _) => inleft _ (exist _ (l :: al) _)
          | inright _ => inright _ _
          end
        | Some (inright _) => inright _ _
        | None =>
          let l := chooseSplit fm in
          match setFormula fm l with
-         | inleft (exist _ fm' _) =>
+         | inleft (exist fm' _) =>
            match satSolve fm' with
-           | inleft (exist _ al _) => inleft _ (exist _ (l :: al) _)
+           | inleft (exist al _) => inleft _ (exist _ (l :: al) _)
            | inright _ =>
              match setFormula fm (negate l) with
-             | inleft (exist _ fm' _) =>
+             | inleft (exist fm' _) =>
                match satSolve fm' with
-               | inleft (exist _ al _) => inleft _ (exist _ (negate l :: al) _)
+               | inleft (exist al _) => inleft _ (exist _ (negate l :: al) _)
                | inright _ => inright _ _
                end
              | inright _ => inright _ _
@@ -594,9 +594,9 @@ Program Fixpoint satSolve (fm: formula) { measure (sat_measure fm) }:
            end
          | inright _ =>
            match setFormula fm (negate l) with
-           | inleft (exist _ fm' _) =>
+           | inleft (exist fm' _) =>
              match satSolve fm' with
-             | inleft (exist _ al _) => inleft _ (exist _ (negate l :: al) _)
+             | inleft (exist al _) => inleft _ (exist _ (negate l :: al) _)
              | inright _ => inright _ _
              end
            | inright _ => inright _ _
@@ -654,7 +654,7 @@ Defined.
 
 Definition satSolveSimple (fm : formula) :=
   match satSolve fm with
-  | inleft (exist _ a _) => Some a
+  | inleft (exist a _) => Some a
   | inright _ => None
   end.
 
diff --git a/src/pipelining/SPBase_types.ml b/src/pipelining/SPBase_types.ml
index ba92340..65c20bc 100644
--- a/src/pipelining/SPBase_types.ml
+++ b/src/pipelining/SPBase_types.ml
@@ -34,22 +34,22 @@ type resource = Reg of reg | Mem
 let inst_coq_to_caml = function 
   | RTL.Inop succ -> Inop
   | RTL.Iop (op, args, dst, succ) -> Iop (op, args, dst)
-  | RTL.Iload (chunk, mode, args, dst, succ) -> Iload (chunk, mode, args, dst)
+  | RTL.Iload (_, chunk, mode, args, dst, succ) -> Iload (chunk, mode, args, dst)
   | RTL.Istore (chunk, mode, args, src, succ) -> Istore (chunk, mode, args, src)
   | RTL.Icall (sign, id, args, dst, succ) -> Icall (sign, id, args, dst)
   | RTL.Itailcall (sign, id, args) -> Itailcall (sign, id, args)
-  | RTL.Icond (cond, args, succ1, succ2) -> Icond (cond, args)
+  | RTL.Icond (cond, args, succ1, succ2, _) -> Icond (cond, args)
   | RTL.Ireturn (res) -> Ireturn (res)
  
 let inst_caml_to_coq i (links : RTL.node list) =
   match i,links with 
   | Inop,[p] -> RTL.Inop p
   | Iop (op, args, dst),[p] -> RTL.Iop (op, args, dst,p)  
-  | Iload (chunk, mode, args, dst),[p] -> RTL.Iload (chunk, mode, args,dst,p) 
+  | Iload (chunk, mode, args, dst),[p] -> RTL.Iload (TRAP, chunk, mode, args,dst,p)
   | Istore (chunk, mode, args, src),[p] -> RTL.Istore (chunk, mode, args, src,p)  
   | Icall (sign, id, args, dst),[p] -> RTL.Icall (sign, id, args, dst,p) 
   | Itailcall (sign, id, args),[] -> RTL.Itailcall (sign, id, args) 
-  | Icond (cond, args),[p1;p2] -> RTL.Icond (cond,args,p1,p2)
+  | Icond (cond, args),[p1;p2] -> RTL.Icond (cond,args,p1,p2,None)
   | Ireturn (res),[] -> RTL.Ireturn res 
   | _,_ -> failwith "Echec lors de la conversion des instrucitons internes vers compcert"