Merge remote-tracking branch 'refs/remotes/origin/mppa-duplicate-oracle' into mppa-duplicate-oracle

4 files changed, 11 insertions, 130 deletions

diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 069741de..82d1f8ef 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -244,13 +244,9 @@ let rec make_identity_ptree_rec = function
 | [] -> PTree.empty
 | m::lm -> let (n, _) = m in PTree.set n n (make_identity_ptree_rec lm)
 
-let make_identity_ptree f = make_identity_ptree_rec (PTree.elements (fn_code f))
+let make_identity_ptree f = make_identity_ptree_rec (PTree.elements f.fn_code)
 
 (* For now, identity function *)
 let duplicate_aux f =
-  let pTreeId = make_identity_ptree f in
-  let traces = select_traces (to_ttl_code @@ fn_code f) (fn_entrypoint f)
-  in begin
-    print_traces traces;
-    (((fn_code f), (fn_entrypoint f)), pTreeId)
-  end
+  let pTreeId = make_identity_ptree f
+  in ((f.fn_code, f.fn_entrypoint), pTreeId)
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index b60c1cb7..c4efaf18 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -744,7 +744,7 @@ Lemma match_stacks_free_right:
   match_stacks F m m1' stk stk' sp.
 Proof.
   intros. eapply match_stacks_invariant; eauto.
-  intros. eapply Mem.perm_free_1; eauto.
+  intros. eapply Mem.perm_free_1; eauto with ordered_type.
   intros. eapply Mem.perm_free_3; eauto.
 Qed.
 
@@ -1097,7 +1097,7 @@ Proof.
   eapply match_stacks_bound with (bound := sp').
   eapply match_stacks_invariant; eauto.
     intros. eapply Mem.perm_free_3; eauto.
-    intros. eapply Mem.perm_free_1; eauto.
+    intros. eapply Mem.perm_free_1; eauto with ordered_type.
     intros. eapply Mem.perm_free_3; eauto.
   erewrite Mem.nextblock_free; eauto. red in VB; xomega.
   eapply agree_val_regs; eauto.
@@ -1189,7 +1189,7 @@ Proof.
   eapply match_stacks_bound with (bound := sp').
   eapply match_stacks_invariant; eauto.
     intros. eapply Mem.perm_free_3; eauto.
-    intros. eapply Mem.perm_free_1; eauto.
+    intros. eapply Mem.perm_free_1; eauto with ordered_type.
     intros. eapply Mem.perm_free_3; eauto.
   erewrite Mem.nextblock_free; eauto. red in VB; xomega.
   destruct or; simpl. apply agree_val_reg; auto. auto.
@@ -1236,7 +1236,7 @@ Proof.
     subst b1. rewrite D in H8; inv H8. eelim Plt_strict; eauto.
     intros. eapply Mem.perm_alloc_1; eauto.
     intros. exploit Mem.perm_alloc_inv. eexact A. eauto.
-    rewrite dec_eq_false; auto.
+    rewrite dec_eq_false; auto with ordered_type.
   auto. auto. auto. eauto. auto.
   rewrite H5. apply agree_regs_init_regs. eauto. auto. inv H1; auto. congruence. auto.
   eapply Mem.valid_new_block; eauto.
diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
deleted file mode 100644
index 4e8efd16..00000000
--- a/backend/PrintLTLin.ml
+++ /dev/null
@@ -1,115 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(** Pretty-printer for LTLin code *)
-
-open Format
-open Camlcoq
-open Datatypes
-open Maps
-open AST
-open Integers
-open Locations
-open Machregsaux
-open LTLin
-open PrintAST
-open PrintOp
-
-let reg pp loc =
-  match loc with
-  | R r ->
-      begin match name_of_register r with
-      | Some s -> fprintf pp "%s" s
-      | None -> fprintf pp "<unknown reg>"
-      end
-  | S (Local(ofs, ty)) ->
-      fprintf pp "local(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
-  | S (Incoming(ofs, ty)) ->
-      fprintf pp "incoming(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
-  | S (Outgoing(ofs, ty)) ->
-      fprintf pp "outgoing(%s,%ld)" (name_of_type ty) (camlint_of_coqint ofs)
-
-let rec regs pp = function
-  | [] -> ()
-  | [r] -> reg pp r
-  | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
-
-let ros pp = function
-  | Coq_inl r -> reg pp r
-  | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
-
-let print_instruction pp i =
-  match i with
-  | Lop(op, args, res) ->
-      fprintf pp "%a = %a@ "
-         reg res (PrintOp.print_operation reg) (op, args)
-  | Lload(chunk, addr, args, dst) ->
-      fprintf pp "%a = %s[%a]@ "
-         reg dst (name_of_chunk chunk)
-         (PrintOp.print_addressing reg) (addr, args)
-  | Lstore(chunk, addr, args, src) ->
-      fprintf pp "%s[%a] = %a@ "
-         (name_of_chunk chunk)
-         (PrintOp.print_addressing reg) (addr, args)
-         reg src
-  | Lcall(sg, fn, args, res) ->
-      fprintf pp "%a = %a(%a)@ "
-        reg res ros fn regs args
-  | Ltailcall(sg, fn, args) ->
-      fprintf pp "tailcall %a(%a)@ "
-        ros fn regs args
-  | Lbuiltin(ef, args, res) ->
-      fprintf pp "%a = builtin %s(%a)@ "
-        reg res (name_of_external ef) regs args
-  | Llabel lbl ->
-      fprintf pp "%ld:@ " (P.to_int32 lbl)
-  | Lgoto lbl ->
-      fprintf pp "goto %ld@ " (P.to_int32 lbl)
-  | Lcond(cond, args, lbl) ->
-      fprintf pp "if (%a) goto %ld@ "
-        (PrintOp.print_condition reg) (cond, args)
-        (P.to_int32 lbl)
-  | Ljumptable(arg, tbl) ->
-      let tbl = Array.of_list tbl in
-      fprintf pp "@[<v 2>jumptable (%a)" reg arg;
-      for i = 0 to Array.length tbl - 1 do
-        fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i))
-      done;
-      fprintf pp "@]@ "
-  | Lreturn None ->
-      fprintf pp "return@ "
-  | Lreturn (Some arg) ->
-      fprintf pp "return %a@ " reg arg
-
-let print_function pp id f =
-  fprintf pp "@[<v 2>%s(%a) {@ " (extern_atom id) regs f.fn_params;
-  List.iter (print_instruction pp) f.fn_code;
-  fprintf pp "@;<0 -2>}@]@."
-
-let print_globdef pp (id, gd) =
-  match gd with
-  | Gfun(Internal f) -> print_function pp id f
-  | _ -> ()
-
-let print_program pp prog =
-  List.iter (print_globdef pp) prog.prog_defs
-
-let destination : string option ref = ref None
-
-let print_if prog =
-  match !destination with
-  | None -> ()
-  | Some f ->
-      let oc = open_out f in
-      let pp = formatter_of_out_channel oc in
-      print_program pp prog;
-      close_out oc
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 084a4548..9a33768c 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1153,10 +1153,10 @@ Proof.
 - constructor.
 - assert (Plt sp bound') by eauto with va.
   eapply sound_stack_public_call; eauto. apply IHsound_stack; intros.
-  apply INV. xomega. rewrite SAME; auto. xomega. auto. auto.
+  apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto.
 - assert (Plt sp bound') by eauto with va.
   eapply sound_stack_private_call; eauto. apply IHsound_stack; intros.
-  apply INV. xomega. rewrite SAME; auto. xomega. auto. auto.
+  apply INV. xomega. rewrite SAME; auto with ordered_type. xomega. auto. auto.
   apply bmatch_ext with m; auto. intros. apply INV. xomega. auto. auto. auto.
 Qed.
 
@@ -1385,7 +1385,7 @@ Proof.
   apply sound_stack_exten with bc.
   apply sound_stack_inv with m. auto.
   intros. apply Q. red. eapply Plt_trans; eauto.
-  rewrite C; auto.
+  rewrite C; auto with ordered_type.
   exact AA.
 * (* public builtin call *)
   exploit anonymize_stack; eauto.
@@ -1404,7 +1404,7 @@ Proof.
   apply sound_stack_exten with bc.
   apply sound_stack_inv with m. auto.
   intros. apply Q. red. eapply Plt_trans; eauto.
-  rewrite C; auto.
+  rewrite C; auto with ordered_type.
   exact AA.
   }
   unfold transfer_builtin in TR.