Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2

51 files changed, 2436 insertions, 456 deletions

diff --git a/.gitignore b/.gitignore
index eb11c837..e886bc10 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,6 +5,8 @@
 **.out
 **.tok
 *.vo
+*.vok
+*.vos
 *.glob
 *.o
 *.a
diff --git a/Changelog b/Changelog
index 935f77f2..08586da5 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,7 @@
+Coq development:
+- Compatibility with Coq version 8.11.0 (#316)
+
+	
 Release 3.6, 2019-09-17
 =======================
 
diff --git a/Makefile b/Makefile
index 27ca8e96..5566cf57 100644
--- a/Makefile
+++ b/Makefile
@@ -266,7 +266,7 @@ endif
 
 
 clean:
-	rm -f $(patsubst %, %/*.vo, $(DIRS))
+	rm -f $(patsubst %, %/*.vo*, $(DIRS))
 	rm -f $(patsubst %, %/.*.aux, $(DIRS))
 	rm -rf doc/html doc/*.glob
 	rm -f driver/Version.ml
diff --git a/Makefile.extr b/Makefile.extr
index 51e9be59..f2d06def 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -50,13 +50,12 @@ 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
-extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60
-extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60
-
+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
 cparser/pre_parser.cmx: WARNINGS += -w -41
 cparser/pre_parser.cmo: WARNINGS += -w -41
 
-COMPFLAGS+=-g $(INCLUDES) $(MENHIR_INCLUDES) $(WARNINGS)
+COMPFLAGS+=-g $(INCLUDES) -I "$(MENHIR_DIR)" $(WARNINGS)
 
 # Using .opt compilers if available
 
diff --git a/Makefile.menhir b/Makefile.menhir
index 98bfc750..7909b2f6 100644
--- a/Makefile.menhir
+++ b/Makefile.menhir
@@ -41,7 +41,11 @@ MENHIR_FLAGS = -v --no-stdlib -la 1
 # Using Menhir in --table mode requires MenhirLib.
 
 ifeq ($(MENHIR_TABLE),true)
-  MENHIR_LIBS = menhirLib.cmx
+  ifeq ($(wildcard $(MENHIR_DIR)/menhirLib.cmxa),)
+    MENHIR_LIBS = menhirLib.cmx
+  else
+    MENHIR_LIBS = menhirLib.cmxa
+  endif
 else
   MENHIR_LIBS =
 endif
diff --git a/aarch64/DuplicateOpcodeHeuristic.ml b/aarch64/DuplicateOpcodeHeuristic.ml
new file mode 100644
index 00000000..85505245
--- /dev/null
+++ b/aarch64/DuplicateOpcodeHeuristic.ml
@@ -0,0 +1,3 @@
+exception HeuristicSucceeded
+        
+let opcode_heuristic code cond ifso ifnot preferred = ()
diff --git a/arm/DuplicateOpcodeHeuristic.ml b/arm/DuplicateOpcodeHeuristic.ml
new file mode 100644
index 00000000..85505245
--- /dev/null
+++ b/arm/DuplicateOpcodeHeuristic.ml
@@ -0,0 +1,3 @@
+exception HeuristicSucceeded
+        
+let opcode_heuristic code cond ifso ifnot preferred = ()
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index c3340cca..d0b7129e 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -529,7 +529,7 @@ let tail_duplicate code preds ptree trace =
   in (new_code, new_ptree, !nb_duplicated)
 
 let superblockify_traces code preds traces =
-  let max_nb_duplicated = 2 (* FIXME - should be architecture dependent *)
+  let max_nb_duplicated = 1 (* FIXME - should be architecture dependent *)
   in let ptree = make_identity_ptree code
   in let rec f code ptree = function
     | [] -> (code, ptree, 0)
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index 902724e0..a6964233 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -1,4 +1,4 @@
-(* *********************************************************************)
+
 (*                                                                     *)
 (*              The Compcert verified compiler                         *)
 (*                                                                     *)
@@ -12,7 +12,6 @@
 
 open LTL
 open Maps
-open Camlcoq
 
 (* Trivial enumeration, in decreasing order of PC *)
 
@@ -29,6 +28,8 @@ let enumerate_aux f reach =
 
 (* More clever enumeration that flattens basic blocks *)
 
+open Camlcoq
+
 module IntSet = Set.Make(struct type t = int let compare = compare end)
 
 (* Determine join points: reachable nodes that have > 1 predecessor *)
@@ -110,5 +111,55 @@ let flatten_blocks blks =
 
 (* Build the enumeration *)
 
-let enumerate_aux f reach =
+let enumerate_aux_flat f reach =
   flatten_blocks (basic_blocks f (join_points f))
+
+(**
+ * Enumeration based on traces as identified by Duplicate.v 
+ *
+ * The Duplicate phase heuristically identifies the most frequented paths. Each
+ * Icond is modified so that the preferred condition is a fallthrough (ifnot)
+ * rather than a branch (ifso).
+ *
+ * The enumeration below takes advantage of this - preferring to layout nodes
+ * following the fallthroughs of the Lcond branches
+ *)
+
+let get_some = function
+| None -> failwith "Did not get some"
+| Some thing -> thing
+
+exception EmptyList
+
+let rec last_element = function
+  | [] -> raise EmptyList
+  | e :: [] -> e
+  | e' :: e :: l -> last_element (e::l)
+
+let dfs code entrypoint =
+  let visited = ref (PTree.map (fun n i -> false) code) in
+  let rec dfs_list code = function
+  | [] -> []
+  | node :: ln ->
+      let node_dfs =
+        if not (get_some @@ PTree.get node !visited) then begin
+          visited := PTree.set node true !visited;
+          match PTree.get node code with
+          | None -> failwith "No such node"
+          | Some bb -> [node] @ match (last_element bb) with
+            | Lop _ | Lload _ | Lgetstack _ | Lsetstack _ | Lstore _ | Lcall _
+            | Lbuiltin _ -> assert false
+            | Ltailcall _ | Lreturn -> []
+            | Lbranch n -> dfs_list code [n]
+            | Lcond (_, _, ifso, ifnot) -> dfs_list code [ifnot; ifso]
+            | Ljumptable(_, ln) -> dfs_list code ln
+          end
+        else []
+      in node_dfs @ (dfs_list code ln)
+  in dfs_list code [entrypoint]
+
+let enumerate_aux_trace f reach = dfs f.fn_code f.fn_entrypoint
+
+let enumerate_aux f reach =
+  if !Clflags.option_ftracelinearize then enumerate_aux_trace f reach
+  else enumerate_aux_flat f reach
diff --git a/configure b/configure
index 716e5e81..f13d1af3 100755
--- a/configure
+++ b/configure
@@ -568,14 +568,14 @@ missingtools=false
 echo "Testing Coq... " | tr -d '\n'
 coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p')
 case "$coq_ver" in
-  8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2)
+  8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
+            echo "Error: CompCert requires one of the following Coq versions: 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
             missingtools=true
         fi;;
   "")
@@ -591,15 +591,15 @@ case "$ocaml_ver" in
         echo "version $ocaml_ver -- UNSUPPORTED"
         echo "Error: CompCert requires OCaml version 4.05 or later."
         missingtools=true;;
-  4.0*)
+  4.*)
         echo "version $ocaml_ver -- good!";;
   ?.*)
         echo "version $ocaml_ver -- UNSUPPORTED"
-        echo "Error: CompCert requires OCaml version 4.02 or later."
+        echo "Error: CompCert requires OCaml version 4.05 or later."
         missingtools=true;;
   *)
         echo "NOT FOUND"
-        echo "Error: make sure OCaml version 4.02 or later is installed."
+        echo "Error: make sure OCaml version 4.05 or later is installed."
         missingtools=true;;
 esac
 
@@ -620,8 +620,8 @@ case "$menhir_ver" in
   20[0-9][0-9][0-9][0-9][0-9][0-9])
       if test "$menhir_ver" -ge $MENHIR_REQUIRED; then
           echo "version $menhir_ver -- good!"
-          menhir_include_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/')
-          if test -z "$menhir_include_dir"; then
+          menhir_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/')
+          if test -z "$menhir_dir"; then
               echo "Error: cannot determine the location of the Menhir API library."
               echo "This can be due to an incorrect Menhir package."
               echo "Consider using the OPAM package for Menhir."
@@ -715,7 +715,7 @@ MANDIR=$sharedir/man
 SHAREDIR=$sharedir
 COQDEVDIR=$coqdevdir
 OCAML_OPT_COMP=$ocaml_opt_comp
-MENHIR_INCLUDES=-I "$menhir_include_dir"
+MENHIR_DIR=$menhir_dir
 COMPFLAGS=-bin-annot
 EOF
 
@@ -845,7 +845,7 @@ EXECUTE=k1-cluster --syscall=libstd_scalls.so --
 CFLAGS= -D __K1C_COS__
 SIMU=k1-cluster -- 
 BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
-    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\
+    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
     Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\
     AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 9a24041b..2cb8c7d9 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -602,8 +602,13 @@ module DwarfPrinter(Target: DWARF_TARGET):
       print_sleb128 oc "" 0;
       print_label oc debug_end (* End of the debug section *)
 
-    let print_location_entry oc c_low l =
+    let print_location_entry oc needs_base c_low l =
       print_label oc (loc_to_label l.loc_id);
+      (* If we have multiple ranges per compilation unit we need to specify a base address for the location *)
+      if needs_base then begin
+        fprintf oc "	%s		-1\n" address;
+        fprintf oc "	%s		%a\n" address label c_low;
+      end;
       List.iter (fun (b,e,loc) ->
         fprintf oc "	%s		%a-%a\n" address label b label c_low;
         fprintf oc "	%s		%a-%a\n" address label e label c_low;
@@ -621,11 +626,11 @@ module DwarfPrinter(Target: DWARF_TARGET):
       fprintf oc "	%s	0\n" address
 
 
-    let print_location_list oc (c_low,l) =
-      let f =  match c_low with
-      | Some s -> print_location_entry oc s
-      | None -> print_location_entry_abs oc in
-     List.iter f l
+    let print_location_list oc needs_base l =
+      let f l =  match l.loc_sec_begin  with
+        | Some s -> print_location_entry oc needs_base s l
+        | None -> print_location_entry_abs oc l in
+      List.iter f l
 
     let list_opt l f =
       match l with
@@ -635,15 +640,15 @@ module DwarfPrinter(Target: DWARF_TARGET):
     let print_diab_entries oc entries =
       let abbrev_start = new_label () in
       abbrev_start_addr := abbrev_start;
-      List.iter (fun e -> compute_abbrev e.entry) entries;
+      List.iter (fun e -> compute_abbrev e.diab_entry) entries;
       print_abbrev oc;
       List.iter (fun e ->
         let name = if e.section_name <> ".text" then Some e.section_name else None in
         section oc (Section_debug_info name);
-        print_debug_info oc e.start_label e.line_label e.entry) entries;
-      if List.exists (fun e -> match e.dlocs with _,[] -> false | _,_ -> true) entries then begin
+        print_debug_info oc e.start_label e.line_label e.diab_entry) entries;
+      if List.exists (fun e -> match e.diab_locs with [] -> false | _ -> true) entries then begin
         section oc Section_debug_loc;
-        List.iter (fun e -> print_location_list oc e.dlocs) entries
+        List.iter (fun e -> print_location_list oc false e.diab_locs) entries
       end
 
     let print_ranges oc r =
@@ -665,8 +670,8 @@ module DwarfPrinter(Target: DWARF_TARGET):
           fprintf oc "	%s	0\n" address;
           fprintf oc "	%s	0\n" address)  r
 
-    let print_gnu_entries oc cp (lpc,loc) s r =
-      compute_abbrev cp;
+    let print_gnu_entries oc entries =
+      compute_abbrev entries.gnu_entry;
       let line_start = new_label ()
       and start = new_label ()
       and  abbrev_start = new_label ()
@@ -674,18 +679,18 @@ module DwarfPrinter(Target: DWARF_TARGET):
       debug_ranges_addr := range_label;
       abbrev_start_addr := abbrev_start;
       section oc (Section_debug_info None);
-      print_debug_info oc start line_start cp;
+      print_debug_info oc start line_start entries.gnu_entry;
       print_abbrev oc;
-      list_opt loc (fun () ->
+      list_opt entries.gnu_locs (fun () ->
         section oc Section_debug_loc;
-        print_location_list oc (lpc,loc));
-      list_opt r (fun () ->
-        print_ranges oc r);
+        print_location_list oc entries.several_secs entries.gnu_locs);
+      list_opt entries.range_table (fun () ->
+        print_ranges oc entries.range_table);
       section oc (Section_debug_line None);
       print_label oc line_start;
-      list_opt s (fun () ->
+      list_opt entries.string_table (fun () ->
         section oc Section_debug_str;
-        let s = List.sort (fun (a,_) (b,_) -> compare a b) s in
+        let s = List.sort (fun (a,_) (b,_) -> compare a b) entries.string_table in
         List.iter (fun (id,s) ->
           print_label oc (loc_to_label id);
           fprintf oc "	.asciz		%S\n" s) s)
@@ -698,6 +703,6 @@ module DwarfPrinter(Target: DWARF_TARGET):
       Hashtbl.clear loc_labels;
       match debug with
       | Diab entries -> print_diab_entries oc entries
-      | Gnu (cp,loc,s,r) -> print_gnu_entries oc cp loc s r
+      | Gnu entries -> print_gnu_entries oc entries
 
   end
diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli
index e1e10601..78dc05fb 100644
--- a/debug/DwarfPrinter.mli
+++ b/debug/DwarfPrinter.mli
@@ -12,7 +12,7 @@
 
 open DwarfTypes
 
-module DwarfPrinter: functor (Target: DWARF_TARGET) ->
+module DwarfPrinter: DWARF_TARGET ->
   sig
     val print_debug: out_channel -> debug_entries -> unit
   end
diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli
index 5a2bce3b..567c65cd 100644
--- a/debug/DwarfTypes.mli
+++ b/debug/DwarfTypes.mli
@@ -266,11 +266,13 @@ type dw_entry =
 
 (* The type for the location list. *)
 type location_entry =
-    {
-     loc:     (address * address * location_value) list;
-     loc_id:  reference;
-   }
-type dw_locations = constant option * location_entry list
+  {
+    loc:     (address * address * location_value) list;
+    loc_id:  reference;
+    loc_sec_begin :  address option;
+  }
+
+type dw_locations = location_entry list
 
 type range_entry =
   | AddressRange  of (address * address) list
@@ -285,13 +287,20 @@ type diab_entry =
      section_name: string;
      start_label:  int;
      line_label:   int;
-     entry:        dw_entry;
-     dlocs:        dw_locations;
+     diab_entry:   dw_entry;
+     diab_locs:    dw_locations;
    }
 
 type diab_entries =  diab_entry list
 
-type gnu_entries = dw_entry * dw_locations * dw_string * dw_ranges
+type gnu_entries =
+  {
+    string_table: dw_string;
+    range_table:  dw_ranges;
+    gnu_locs:     dw_locations;
+    gnu_entry:    dw_entry;
+    several_secs: bool;
+  }
 
 type debug_entries =
   | Diab of diab_entries
diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml
index e1b71f13..6c1d0846 100644
--- a/debug/Dwarfgen.ml
+++ b/debug/Dwarfgen.ml
@@ -408,7 +408,7 @@ module Dwarfgenaux (Target: TARGET) =
                   and lo = translate_label f_id lo in
                   hi,lo,range_entry_loc i.var_loc) l in
                 let id = next_id () in
-                Some (LocRef id),[{loc = l;loc_id = id;}]
+                Some (LocRef id),[{loc_sec_begin = !current_section_start; loc = l;loc_id = id;}]
           end
         with Not_found -> None,[]
       else
@@ -574,8 +574,8 @@ let diab_gen_compilation_section sec_name s defs acc =
     section_name = s;
     start_label = debug_start;
     line_label = line_start;
-    entry = cp;
-    dlocs = Some low_pc,accu.locs;
+    diab_entry = cp;
+    diab_locs = accu.locs;
   }::acc
 
 let gen_diab_debug_info sec_name var_section : debug_entries =
@@ -643,6 +643,12 @@ let gen_gnu_debug_info sec_name var_section : debug_entries =
   } in
   let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in
   let cp = add_children cp (types@defs) in
-  let loc_pc = if StringSet.cardinal sec > 1 then None else low_pc in
   let string_table = Hashtbl.fold (fun s i acc -> (i,s)::acc) string_table [] in
-  Gnu (cp,(loc_pc,accu.locs),string_table,snd accu.ranges)
+  let cp = {
+    string_table = string_table;
+    range_table = snd accu.ranges;
+    gnu_locs = accu.locs;
+    gnu_entry = cp;
+    several_secs = StringSet.cardinal sec > 1}
+  in
+  Gnu cp
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index e373b2e1..6d6f1df4 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -30,6 +30,7 @@ let option_fcse2 = ref true
 let option_fredundancy = ref true
 let option_fduplicate = ref false
 let option_finvertcond = ref true (* only active if option_fduplicate is also true *)
+let option_ftracelinearize = ref false
 let option_fpostpass = ref true
 let option_fpostpass_sched = ref "list"
 let option_fifconversion = ref true
diff --git a/driver/Driver.ml b/driver/Driver.ml
index ffe1fc4b..db71aef9 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -203,6 +203,8 @@ Processing options:
   -fduplicate    Perform tail duplication to form superblocks on predicted traces
     -finvertcond    Invert conditions based on predicted paths (to prefer fallthrough).
                     Requires -fduplicate to be also activated [on]
+    -ftracelinearize Linearizes based on the traces identified by duplicate phase
+                    It is recommended to also activate -fduplicate with this pass [off]
   -fforward-moves   Forward moves after CSE
   -finline       Perform inlining of functions [on]
   -finline-functions-called-once Integrate functions only required by their
@@ -393,6 +395,7 @@ let cmdline_actions =
   @ f_opt "postpass" option_fpostpass
   @ f_opt "duplicate" option_fduplicate
   @ f_opt "invertcond" option_finvertcond
+  @ f_opt "tracelinearize" option_ftracelinearize
   @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched
   @ f_opt "inline" option_finline
   @ f_opt "inline-functions-called-once" option_finline_functions_called_once
diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v
index c9e7bad5..e8c1d831 100644
--- a/lib/BoolEqual.v
+++ b/lib/BoolEqual.v
@@ -106,8 +106,8 @@ Ltac bool_eq_refl_case :=
   end.
 
 Ltac bool_eq_refl :=
-  let H := fresh "Hrec" in let x := fresh "x" in
-  fix H 1; intros x; destruct x; simpl; bool_eq_refl_case.
+  let Hrec := fresh "Hrec" in let x := fresh "x" in
+  fix Hrec 1; intros x; destruct x; simpl; bool_eq_refl_case.
 
 Lemma false_not_true:
   forall (P: Prop), false = true -> P.
@@ -124,7 +124,6 @@ Qed.
 
 Ltac bool_eq_sound_case :=
   match goal with
-  | [ H: false = true |- _ ] => exact (false_not_true _ H)
   | [ H: _ && _ = true |- _ ] => apply andb_prop in H; destruct H; bool_eq_sound_case
   | [ H: proj_sumbool ?a = true |- _ ] => apply proj_sumbool_true in H; bool_eq_sound_case
   | [ |- ?C ?x1 ?x2 ?x3 ?x4 = ?C ?y1 ?y2 ?y3 ?y4 ] => apply f_equal4; auto
@@ -137,7 +136,9 @@ Ltac bool_eq_sound_case :=
 
 Ltac bool_eq_sound :=
   let Hrec := fresh "Hrec" in let x := fresh "x" in let y := fresh "y" in
-  fix Hrec 1; intros x y; destruct x, y; simpl; intro; bool_eq_sound_case.
+  let H := fresh "EQ" in
+  fix Hrec 1; intros x y; destruct x, y; intro H;
+  try (apply (false_not_true _ H)); simpl in H; bool_eq_sound_case.
 
 Lemma dec_eq_from_bool_eq:
   forall (A: Type) (f: A -> A -> bool)
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 91e5ac89..a05d4726 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -33,6 +33,19 @@ Require Import Conventions.
 Require Import Errors.
 Require Export Asmvliw.
 
+(* Notations necessary to hook Asmvliw definitions *)
+Notation undef_caller_save_regs := Asmvliw.undef_caller_save_regs.
+Notation regset := Asmvliw.regset.
+Notation extcall_arg := Asmvliw.extcall_arg.
+Notation extcall_arg_pair := Asmvliw.extcall_arg_pair.
+Notation extcall_arguments := Asmvliw.extcall_arguments.
+Notation set_res := Asmvliw.set_res.
+Notation function := Asmvliw.function.
+Notation bblocks := Asmvliw.bblocks.
+Notation header := Asmvliw.header.
+Notation body := Asmvliw.body.
+Notation exit := Asmvliw.exit.
+Notation correct := Asmvliw.correct.
 
 (** * Auxiliary utilies on basic blocks *)
 
@@ -294,6 +307,31 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
      end
   end.
 
+
+Theorem builtin_body_nil:
+  forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
+Proof.
+  intros. destruct bb as [hd bdy ex WF]. simpl in *.
+  apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
+  eapply H1; eauto.
+Qed.
+
+Theorem exec_body_app:
+  forall l l' rs m rs'' m'',
+  exec_body (l ++ l') rs m = Next rs'' m'' ->
+  exists rs' m',
+       exec_body l rs m = Next rs' m'
+    /\ exec_body l' rs' m' = Next rs'' m''.
+Proof.
+  induction l.
+  - intros. simpl in H. repeat eexists. auto.
+  - intros. rewrite <- app_comm_cons in H. simpl in H.
+    destruct (exec_basic_instr a rs m) eqn:EXEBI.
+    + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).
+      repeat eexists. simpl. rewrite EXEBI. eauto. auto.
+    + discriminate.
+Qed.
+
 (** Position corresponding to a label *)
 
 Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := par_goto_label f lbl rs rs m.
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 584f2339..02f9141b 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -7,7 +7,7 @@
 
 Require Import AST.
 Require Import Asmblock.
-Require Import Asmblockgenproof0.
+Require Import Asmblockgenproof0 Asmblockprops.
 Require Import Values.
 Require Import Globalenvs.
 Require Import Memory.
@@ -1429,7 +1429,7 @@ Lemma bblock_simu_reduce:
   forall p1 p2 ge fn,
   Ge = Genv ge fn ->
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
-  Asmblockgenproof0.bblock_simu ge fn p1 p2.
+  Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
   unfold bblock_simu, res_eq; intros p1 p2 ge fn H1 H2 rs m DONTSTUCK.
   generalize (H2 (trans_state (State rs m))); clear H2.
@@ -1787,7 +1787,7 @@ Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool :=
 Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp.
 
 Theorem bblock_simu_test_correct verb p1 p2 :
-  WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockgenproof0.bblock_simu ge fn p1 p2.
+  WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
   wlp_simplify.
 Qed.
@@ -1803,7 +1803,7 @@ Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool :=
   | None => false
   end.
 
-Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
+Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
    unfold pure_bblock_simu_test. 
    destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate.
@@ -1813,7 +1813,7 @@ Qed.
 
 Definition bblock_simub: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_simu_test true.
 
-Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
+Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
  eapply (pure_bblock_simu_test_correct true).
 Qed.
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index e130df45..1a427112 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -16,7 +16,7 @@ Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock.
-Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1.
+Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
 Require Import Axioms.
 
 Module MB := Machblock.
@@ -1353,19 +1353,6 @@ Proof.
     rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto.
 Qed.
 
-Lemma exec_body_pc:
-  forall l rs1 m1 rs2 m2,
-  exec_body tge l rs1 m1 = Next rs2 m2 ->
-  rs2 PC = rs1 PC.
-Proof.
-  induction l.
-  - intros. inv H. auto.
-  - intros until m2. intro EXEB.
-    inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.
-    eapply IHl in H0. rewrite H0.
-    erewrite exec_basic_instr_pc; eauto.
-Qed.
-
 Lemma exec_body_control:
   forall b rs1 m1 rs2 m2 rs3 m3 fn,
   exec_body tge (body b) rs1 m1 = Next rs2 m2 ->
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index c0a05ab3..ecb4629b 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -20,7 +20,7 @@
 Require Import Coqlib Errors Maps.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Machblock Conventions.
-Require Import Asmblock Asmblockgen Asmblockgenproof0.
+Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
 Require Import Chunks.
 
 (** Decomposition of integer constants. *)
diff --git a/mppa_k1c/Asmblockprops.v b/mppa_k1c/Asmblockprops.v
new file mode 100644
index 00000000..3c6ba534
--- /dev/null
+++ b/mppa_k1c/Asmblockprops.v
@@ -0,0 +1,343 @@
+(** Common definition and proofs on Asmblock required by various modules *)
+
+Require Import Coqlib.
+Require Import Integers.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Values.
+Require Import Asmblock.
+Require Import Axioms.
+
+Definition bblock_simu (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
+  forall rs m,
+    exec_bblock ge f bb rs m <> Stuck ->
+    exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m.
+    
+Hint Extern 2 (_ <> _) => congruence: asmgen.
+
+Lemma preg_of_data:
+  forall r, data_preg (preg_of r) = true.
+Proof.
+  intros. destruct r; reflexivity.
+Qed.
+Hint Resolve preg_of_data: asmgen.
+
+Lemma data_diff:
+  forall r r',
+  data_preg r = true -> data_preg r' = false -> r <> r'.
+Proof.
+  congruence.
+Qed.
+Hint Resolve data_diff: asmgen.
+
+Lemma preg_of_not_PC:
+  forall r, preg_of r <> PC.
+Proof.
+  intros. apply data_diff; auto with asmgen.
+Qed.
+
+Lemma preg_of_not_SP:
+  forall r, preg_of r <> SP.
+Proof.
+  intros. unfold preg_of; destruct r; simpl; congruence.
+Qed.
+
+Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
+
+
+Lemma nextblock_pc:
+  forall b rs, (nextblock b rs)#PC = Val.offset_ptr rs#PC (Ptrofs.repr (size b)).
+Proof.
+  intros. apply Pregmap.gss.
+Qed.
+
+Lemma nextblock_inv:
+  forall b r rs, r <> PC -> (nextblock b rs)#r = rs#r.
+Proof.
+  intros. unfold nextblock. apply Pregmap.gso. red; intro; subst. auto.
+Qed.
+
+Lemma nextblock_inv1:
+  forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r.
+Proof.
+  intros. apply nextblock_inv. red; intro; subst; discriminate.
+Qed.
+
+Ltac Simplif :=
+  ((rewrite nextblock_inv by eauto with asmgen)
+  || (rewrite nextblock_inv1 by eauto with asmgen)
+  || (rewrite Pregmap.gss)
+  || (rewrite nextblock_pc)
+  || (rewrite Pregmap.gso by eauto with asmgen)
+  ); auto with asmgen.
+
+Ltac Simpl := repeat Simplif.
+
+(* For Asmblockgenproof0 *)
+
+Theorem exec_basic_instr_pc:
+  forall ge b rs1 m1 rs2 m2,
+  exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  intros. destruct b; try destruct i; try destruct i.
+  all: try (inv H; Simpl).
+  1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+
+  1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+
+  { (* PLoadQRRO *)
+    unfold  parexec_load_q_offset in H1.
+    destruct (gpreg_q_expand _) as [r0 r1] in H1.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    inv H1. Simpl. }
+  { (* PLoadORRO *)
+    unfold  parexec_load_o_offset in H1.
+    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    inv H1. Simpl. }
+  1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
+  1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
+  1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
+  
+  { (* PStoreQRRO *)
+    unfold  parexec_store_q_offset in H1.
+    destruct (gpreg_q_expand _) as [r0 r1] in H1.
+    unfold eval_offset in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    inv H1. Simpl. reflexivity. }
+  { (* PStoreORRO *)
+    unfold  parexec_store_o_offset in H1.
+    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
+    unfold eval_offset in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    inv H1. Simpl. reflexivity. }
+  - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
+  - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
+    destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
+  - destruct rs; try discriminate. inv H1. Simpl.
+  - destruct rd; try discriminate. inv H1; Simpl.
+  - reflexivity.
+Qed.
+
+(* For PostpassSchedulingproof *)
+
+Lemma regset_double_set:
+  forall r1 r2 (rs: regset) v1 v2,
+  r1 <> r2 ->
+  (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1).
+Proof.
+  intros. apply functional_extensionality. intros r. destruct (preg_eq r r1).
+  - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto.
+  - destruct (preg_eq r r2).
+    + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto.
+    + repeat (rewrite Pregmap.gso; auto).
+Qed.
+
+Lemma next_eq:
+  forall (rs rs': regset) m m',
+  rs = rs' -> m = m' -> Next rs m = Next rs' m'.
+Proof.
+  intros; apply f_equal2; auto.
+Qed.
+
+Lemma exec_load_offset_pc_var:
+  forall trap t rs m rd ra ofs rs' m' v,
+  exec_load_offset trap t rs m rd ra ofs = Next rs' m' ->
+  exec_load_offset trap t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate.
+  destruct (Mem.loadv _ _ _).
+  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
+  - unfold parexec_incorrect_load in *.
+    destruct trap; try discriminate.
+    inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
+Qed.
+
+Lemma exec_load_reg_pc_var:
+  forall trap t rs m rd ra ro rs' m' v,
+    exec_load_reg trap t rs m rd ra ro = Next rs' m' ->
+    exec_load_reg trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate.
+  destruct (Mem.loadv _ _ _).
+  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
+  - unfold parexec_incorrect_load in *.
+    destruct trap; try discriminate.
+    inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
+Qed.
+
+Lemma exec_load_regxs_pc_var:
+  forall trap t rs m rd ra ro rs' m' v,
+  exec_load_regxs trap t rs m rd ra ro = Next rs' m' ->
+  exec_load_regxs trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate.
+  destruct (Mem.loadv _ _ _).
+  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
+  - unfold parexec_incorrect_load in *.
+    destruct trap; try discriminate.
+    inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
+Qed.
+
+Lemma exec_load_offset_q_pc_var:
+  forall rs m rd ra ofs rs' m' v,
+  exec_load_q_offset rs m rd ra ofs = Next rs' m' ->
+  exec_load_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_load_q_offset in *. unfold parexec_load_q_offset in *.
+  destruct (gpreg_q_expand rd) as [rd0 rd1].
+  (* destruct (ireg_eq rd0 ra); try discriminate. *)
+  rewrite Pregmap.gso; try discriminate.
+  destruct (Mem.loadv _ _ _); try discriminate.
+  inv H.
+  destruct (Mem.loadv _ _ _); try discriminate.
+  inv H1. f_equal.
+  rewrite (regset_double_set PC rd0) by discriminate.
+  rewrite (regset_double_set PC rd1) by discriminate.
+  reflexivity.
+Qed.
+
+Lemma exec_load_offset_o_pc_var:
+  forall rs m rd ra ofs rs' m' v,
+  exec_load_o_offset rs m rd ra ofs = Next rs' m' ->
+  exec_load_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_load_o_offset in *. unfold parexec_load_o_offset in *.
+  destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3].
+(*
+  destruct (ireg_eq rd0 ra); try discriminate.
+  destruct (ireg_eq rd1 ra); try discriminate.
+  destruct (ireg_eq rd2 ra); try discriminate.
+*)
+  rewrite Pregmap.gso; try discriminate.
+  simpl in *.
+  destruct (Mem.loadv _ _ _); try discriminate.
+  destruct (Mem.loadv _ _ _); try discriminate.
+  destruct (Mem.loadv _ _ _); try discriminate.
+  destruct (Mem.loadv _ _ _); try discriminate.
+  rewrite (regset_double_set PC rd0) by discriminate.
+  rewrite (regset_double_set PC rd1) by discriminate.
+  rewrite (regset_double_set PC rd2) by discriminate.
+  rewrite (regset_double_set PC rd3) by discriminate.
+  inv H.
+  trivial.
+Qed.
+
+Lemma exec_store_offset_pc_var:
+  forall t rs m rd ra ofs rs' m' v,
+  exec_store_offset t rs m rd ra ofs = Next rs' m' ->
+  exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate.
+  destruct (eval_offset ofs); try discriminate.
+  destruct (Mem.storev _ _ _).
+  - inv H. apply next_eq; auto.
+  - discriminate.
+Qed.
+
+Lemma exec_store_q_offset_pc_var:
+  forall rs m rd ra ofs rs' m' v,
+  exec_store_q_offset rs m rd ra ofs = Next rs' m' ->
+  exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate.
+  simpl in *.
+  destruct (gpreg_q_expand _) as [s0 s1].
+  destruct (Mem.storev _ _ _); try discriminate.
+  destruct (Mem.storev _ _ _); try discriminate.
+  inv H. apply next_eq; auto.
+Qed.
+
+Lemma exec_store_o_offset_pc_var:
+  forall rs m rd ra ofs rs' m' v,
+  exec_store_o_offset rs m rd ra ofs = Next rs' m' ->
+  exec_store_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+  intros.
+  unfold exec_store_o_offset in *. unfold parexec_store_o_offset in *.
+  destruct (gpreg_o_expand _) as [[[s0 s1] s2] s3].
+  destruct (Mem.storev _ _ _); try discriminate.
+  destruct (Mem.storev _ _ _); try discriminate.
+  destruct (Mem.storev _ _ _); try discriminate.
+  destruct (Mem.storev _ _ _); try discriminate.
+  inv H.
+  trivial.
+Qed.
+  
+Lemma exec_store_reg_pc_var:
+  forall t rs m rd ra ro rs' m' v,
+  exec_store_reg t rs m rd ra ro = Next rs' m' ->
+  exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_store_reg in *. unfold parexec_store_reg in *. rewrite Pregmap.gso; try discriminate.
+  destruct (Mem.storev _ _ _).
+  - inv H. apply next_eq; auto.
+  - discriminate.
+Qed.
+
+Lemma exec_store_regxs_pc_var:
+  forall t rs m rd ra ro rs' m' v,
+  exec_store_regxs t rs m rd ra ro = Next rs' m' ->
+  exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate.
+  destruct (Mem.storev _ _ _).
+  - inv H. apply next_eq; auto.
+  - discriminate.
+Qed.
+
+Theorem exec_basic_instr_pc_var:
+  forall ge i rs m rs' m' v,
+  exec_basic_instr ge i rs m = Next rs' m' ->
+  exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
+Proof.
+  intros. unfold exec_basic_instr in *. unfold bstep in *. destruct i.
+  - unfold exec_arith_instr in *. destruct i; destruct i.
+      all: try (exploreInst; inv H; apply next_eq; auto;
+      apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
+(* 
+      (* Some cases treated seperately because exploreInst destructs too much *)
+      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). *)
+  - destruct i.
+    + exploreInst; apply exec_load_offset_pc_var; auto.
+    + exploreInst; apply exec_load_reg_pc_var; auto.
+    + exploreInst; apply exec_load_regxs_pc_var; auto.
+    + apply exec_load_offset_q_pc_var; auto.
+    + apply exec_load_offset_o_pc_var; auto.
+  - destruct i.
+    + exploreInst; apply exec_store_offset_pc_var; auto.
+    + exploreInst; apply exec_store_reg_pc_var; auto.
+    + exploreInst; apply exec_store_regxs_pc_var; auto.
+    + apply exec_store_q_offset_pc_var; auto.
+    + apply exec_store_o_offset_pc_var; auto.
+  - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
+    destruct (Mem.storev _ _ _ _); try discriminate.
+    inv H. apply next_eq; auto. apply functional_extensionality. intros.
+    rewrite (regset_double_set GPR32 PC); try discriminate.
+    rewrite (regset_double_set GPR12 PC); try discriminate.
+    rewrite (regset_double_set FP PC); try discriminate. reflexivity.
+  - repeat (rewrite Pregmap.gso; try discriminate).
+    destruct (Mem.loadv _ _ _); try discriminate.
+    destruct (rs GPR12); try discriminate.
+    destruct (Mem.free _ _ _ _); try discriminate.
+    inv H. apply next_eq; auto.
+    rewrite (regset_double_set GPR32 PC).
+    rewrite (regset_double_set GPR12 PC). reflexivity.
+    all: discriminate.
+  - destruct rs0; try discriminate. inv H. apply next_eq; auto.
+    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
+  - destruct rd; try discriminate. inv H. apply next_eq; auto.
+    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
+  - inv H. apply next_eq; auto.
+Qed.
+
+
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 8b6de1e2..31180cea 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -12,7 +12,7 @@
 
 Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
-Require Import Asmblockdeps Asmblockgenproof0.
+Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops.
 Require Peephole.
 
 Local Open Scope error_monad_scope.
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 867c10c5..fbb06c9b 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -14,7 +14,7 @@ Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Machblock Conventions Asmblock.
-Require Import Asmblockgenproof0.
+Require Import Asmblockgenproof0 Asmblockprops.
 Require Import PostpassScheduling.
 Require Import Asmblockgenproof.
 Require Import Axioms.
@@ -30,62 +30,6 @@ Proof.
   intros. eapply match_transform_partial_program; eauto.
 Qed.
 
-Remark builtin_body_nil:
-  forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil.
-Proof.
-  intros. destruct bb as [hd bdy ex WF]. simpl in *.
-  apply wf_bblock_refl in WF. inv WF. unfold builtin_alone in H1.
-  eapply H1; eauto.
-Qed.
-
-Lemma exec_body_app:
-  forall l l' ge rs m rs'' m'',
-  exec_body ge (l ++ l') rs m = Next rs'' m'' ->
-  exists rs' m',
-       exec_body ge l rs m = Next rs' m'
-    /\ exec_body ge l' rs' m' = Next rs'' m''.
-Proof.
-  induction l.
-  - intros. simpl in H. repeat eexists. auto.
-  - intros. rewrite <- app_comm_cons in H. simpl in H.
-    destruct (exec_basic_instr ge a rs m) eqn:EXEBI.
-    + apply IHl in H. destruct H as (rs1 & m1 & EXEB1 & EXEB2).
-      repeat eexists. simpl. rewrite EXEBI. eauto. auto.
-    + discriminate.
-Qed.
-
-Lemma exec_body_pc:
-  forall l ge rs1 m1 rs2 m2,
-  exec_body ge l rs1 m1 = Next rs2 m2 ->
-  rs2 PC = rs1 PC.
-Proof.
-  induction l.
-  - intros. inv H. auto.
-  - intros until m2. intro EXEB.
-    inv EXEB. destruct (exec_basic_instr _ _ _) eqn:EBI; try discriminate.
-    eapply IHl in H0. rewrite H0.
-    erewrite exec_basic_instr_pc; eauto.
-Qed.
-
-Lemma next_eq:
-  forall (rs rs': regset) m m',
-  rs = rs' -> m = m' -> Next rs m = Next rs' m'.
-Proof.
-  intros; apply f_equal2; auto.
-Qed.
-
-Lemma regset_double_set:
-  forall r1 r2 (rs: regset) v1 v2,
-  r1 <> r2 ->
-  (rs # r1 <- v1 # r2 <- v2) = (rs # r2 <- v2 # r1 <- v1).
-Proof.
-  intros. apply functional_extensionality. intros r. destruct (preg_eq r r1).
-  - subst. rewrite Pregmap.gso; auto. repeat (rewrite Pregmap.gss). auto.
-  - destruct (preg_eq r r2).
-    + subst. rewrite Pregmap.gss. rewrite Pregmap.gso; auto. rewrite Pregmap.gss. auto.
-    + repeat (rewrite Pregmap.gso; auto).
-Qed.
-
 Lemma regset_double_set_id:
   forall r (rs: regset) v1 v2,
   (rs # r <- v1 # r <- v2) = (rs # r <- v2).
@@ -95,197 +39,6 @@ Proof.
   - repeat (rewrite Pregmap.gso); auto.
 Qed.
 
-Lemma exec_load_offset_pc_var:
-  forall trap t rs m rd ra ofs rs' m' v,
-  exec_load_offset trap t rs m rd ra ofs = Next rs' m' ->
-  exec_load_offset trap t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
-  intros. unfold exec_load_offset in *. unfold parexec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ofs); try discriminate.
-  destruct (Mem.loadv _ _ _).
-  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
-  - unfold parexec_incorrect_load in *.
-    destruct trap; try discriminate.
-    inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
-Qed.
-
-Lemma exec_load_reg_pc_var:
-  forall trap t rs m rd ra ro rs' m' v,
-    exec_load_reg trap t rs m rd ra ro = Next rs' m' ->
-    exec_load_reg trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
-Proof.
-  intros. unfold exec_load_reg in *. unfold parexec_load_reg in *. rewrite Pregmap.gso; try discriminate.
-  destruct (Mem.loadv _ _ _).
-  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
-  - unfold parexec_incorrect_load in *.
-    destruct trap; try discriminate.
-    inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
-Qed.
-
-Lemma exec_load_regxs_pc_var:
-  forall trap t rs m rd ra ro rs' m' v,
-  exec_load_regxs trap t rs m rd ra ro = Next rs' m' ->
-  exec_load_regxs trap t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
-Proof.
-  intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate.
-  destruct (Mem.loadv _ _ _).
-  - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
-  - unfold parexec_incorrect_load in *.
-    destruct trap; try discriminate.
-    inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
-Qed.
-
-Lemma exec_load_offset_q_pc_var:
-  forall rs m rd ra ofs rs' m' v,
-  exec_load_q_offset rs m rd ra ofs = Next rs' m' ->
-  exec_load_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
-  intros. unfold exec_load_q_offset in *. unfold parexec_load_q_offset in *.
-  destruct (gpreg_q_expand rd) as [rd0 rd1].
-  (* destruct (ireg_eq rd0 ra); try discriminate. *)
-  rewrite Pregmap.gso; try discriminate.
-  destruct (Mem.loadv _ _ _); try discriminate.
-  inv H.
-  destruct (Mem.loadv _ _ _); try discriminate.
-  inv H1. f_equal.
-  rewrite (regset_double_set PC rd0) by discriminate.
-  rewrite (regset_double_set PC rd1) by discriminate.
-  reflexivity.
-Qed.
-
-Lemma exec_load_offset_o_pc_var:
-  forall rs m rd ra ofs rs' m' v,
-  exec_load_o_offset rs m rd ra ofs = Next rs' m' ->
-  exec_load_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
-  intros. unfold exec_load_o_offset in *. unfold parexec_load_o_offset in *.
-  destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3].
-(*
-  destruct (ireg_eq rd0 ra); try discriminate.
-  destruct (ireg_eq rd1 ra); try discriminate.
-  destruct (ireg_eq rd2 ra); try discriminate.
-*)
-  rewrite Pregmap.gso; try discriminate.
-  simpl in *.
-  destruct (Mem.loadv _ _ _); try discriminate.
-  destruct (Mem.loadv _ _ _); try discriminate.
-  destruct (Mem.loadv _ _ _); try discriminate.
-  destruct (Mem.loadv _ _ _); try discriminate.
-  rewrite (regset_double_set PC rd0) by discriminate.
-  rewrite (regset_double_set PC rd1) by discriminate.
-  rewrite (regset_double_set PC rd2) by discriminate.
-  rewrite (regset_double_set PC rd3) by discriminate.
-  inv H.
-  trivial.
-Qed.
-
-Lemma exec_store_offset_pc_var:
-  forall t rs m rd ra ofs rs' m' v,
-  exec_store_offset t rs m rd ra ofs = Next rs' m' ->
-  exec_store_offset t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
-  intros. unfold exec_store_offset in *. unfold parexec_store_offset in *. rewrite Pregmap.gso; try discriminate.
-  destruct (eval_offset ofs); try discriminate.
-  destruct (Mem.storev _ _ _).
-  - inv H. apply next_eq; auto.
-  - discriminate.
-Qed.
-
-Lemma exec_store_q_offset_pc_var:
-  forall rs m rd ra ofs rs' m' v,
-  exec_store_q_offset rs m rd ra ofs = Next rs' m' ->
-  exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
-  intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate.
-  simpl in *.
-  destruct (gpreg_q_expand _) as [s0 s1].
-  destruct (Mem.storev _ _ _); try discriminate.
-  destruct (Mem.storev _ _ _); try discriminate.
-  inv H. apply next_eq; auto.
-Qed.
-
-Lemma exec_store_o_offset_pc_var:
-  forall rs m rd ra ofs rs' m' v,
-  exec_store_o_offset rs m rd ra ofs = Next rs' m' ->
-  exec_store_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
-Proof.
-  intros.
-  unfold exec_store_o_offset in *. unfold parexec_store_o_offset in *.
-  destruct (gpreg_o_expand _) as [[[s0 s1] s2] s3].
-  destruct (Mem.storev _ _ _); try discriminate.
-  destruct (Mem.storev _ _ _); try discriminate.
-  destruct (Mem.storev _ _ _); try discriminate.
-  destruct (Mem.storev _ _ _); try discriminate.
-  inv H.
-  trivial.
-Qed.
-  
-Lemma exec_store_reg_pc_var:
-  forall t rs m rd ra ro rs' m' v,
-  exec_store_reg t rs m rd ra ro = Next rs' m' ->
-  exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
-Proof.
-  intros. unfold exec_store_reg in *. unfold parexec_store_reg in *. rewrite Pregmap.gso; try discriminate.
-  destruct (Mem.storev _ _ _).
-  - inv H. apply next_eq; auto.
-  - discriminate.
-Qed.
-
-Lemma exec_store_regxs_pc_var:
-  forall t rs m rd ra ro rs' m' v,
-  exec_store_regxs t rs m rd ra ro = Next rs' m' ->
-  exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
-Proof.
-  intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate.
-  destruct (Mem.storev _ _ _).
-  - inv H. apply next_eq; auto.
-  - discriminate.
-Qed.
-
-Lemma exec_basic_instr_pc_var:
-  forall ge i rs m rs' m' v,
-  exec_basic_instr ge i rs m = Next rs' m' ->
-  exec_basic_instr ge i (rs # PC <- v) m = Next (rs' # PC <- v) m'.
-Proof.
-  intros. unfold exec_basic_instr in *. unfold bstep in *. destruct i.
-  - unfold exec_arith_instr in *. destruct i; destruct i.
-      all: try (exploreInst; inv H; apply next_eq; auto;
-      apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
-(* 
-      (* Some cases treated seperately because exploreInst destructs too much *)
-      all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate). *)
-  - destruct i.
-    + exploreInst; apply exec_load_offset_pc_var; auto.
-    + exploreInst; apply exec_load_reg_pc_var; auto.
-    + exploreInst; apply exec_load_regxs_pc_var; auto.
-    + apply exec_load_offset_q_pc_var; auto.
-    + apply exec_load_offset_o_pc_var; auto.
-  - destruct i.
-    + exploreInst; apply exec_store_offset_pc_var; auto.
-    + exploreInst; apply exec_store_reg_pc_var; auto.
-    + exploreInst; apply exec_store_regxs_pc_var; auto.
-    + apply exec_store_q_offset_pc_var; auto.
-    + apply exec_store_o_offset_pc_var; auto.
-  - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
-    destruct (Mem.storev _ _ _ _); try discriminate.
-    inv H. apply next_eq; auto. apply functional_extensionality. intros.
-    rewrite (regset_double_set GPR32 PC); try discriminate.
-    rewrite (regset_double_set GPR12 PC); try discriminate.
-    rewrite (regset_double_set FP PC); try discriminate. reflexivity.
-  - repeat (rewrite Pregmap.gso; try discriminate).
-    destruct (Mem.loadv _ _ _); try discriminate.
-    destruct (rs GPR12); try discriminate.
-    destruct (Mem.free _ _ _ _); try discriminate.
-    inv H. apply next_eq; auto.
-    rewrite (regset_double_set GPR32 PC).
-    rewrite (regset_double_set GPR12 PC). reflexivity.
-    all: discriminate.
-  - destruct rs0; try discriminate. inv H. apply next_eq; auto.
-    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
-  - destruct rd; try discriminate. inv H. apply next_eq; auto.
-    repeat (rewrite Pregmap.gso; try discriminate). apply regset_double_set; discriminate.
-  - inv H. apply next_eq; auto.
-Qed.
-
 Lemma exec_body_pc_var:
   forall l ge rs m rs' m' v,
   exec_body ge l rs m = Next rs' m' ->
@@ -782,12 +535,8 @@ Qed.
 
 End PRESERVATION_ASMBLOCK.
 
-
-
-
 Require Import Asmvliw.
 
-
 Lemma verified_par_checks_alls_bundles lb x: forall bundle,
   verify_par lb = OK x ->
   List.In bundle lb -> verify_par_bblock bundle = OK tt.
@@ -798,7 +547,6 @@ Proof.
   destruct x0; auto.
 Qed.
 
-
 Lemma verified_schedule_nob_checks_alls_bundles bb lb bundle:
   verified_schedule_nob bb = OK lb ->
   List.In bundle lb -> verify_par_bblock bundle = OK tt.
@@ -920,9 +668,6 @@ Qed.
 
 End PRESERVATION_ASMVLIW.
 
-
-
-
 Section PRESERVATION.
 
 Variables prog tprog: program.
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 07c445e2..940c6563 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -22,16 +22,10 @@ Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
 Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
+Require Import Asmblockprops.
 
 Module MB:=Machblock.
-Module AB:=Asmvliw.
-
-Hint Extern 2 (_ <> _) => congruence: asmgen.
-
-Definition bblock_simu (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
-  forall rs m,
-    exec_bblock ge f bb rs m <> Stuck ->
-    exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m.
+Module AB:=Asmblock.
 
 Lemma ireg_of_eq:
   forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
@@ -51,53 +45,6 @@ Proof.
   destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
 Qed.
 
-Lemma preg_of_data:
-  forall r, data_preg (preg_of r) = true.
-Proof.
-  intros. destruct r; reflexivity.
-Qed.
-Hint Resolve preg_of_data: asmgen.
-
-Lemma data_diff:
-  forall r r',
-  data_preg r = true -> data_preg r' = false -> r <> r'.
-Proof.
-  congruence.
-Qed.
-Hint Resolve data_diff: asmgen.
-
-Lemma preg_of_not_SP:
-  forall r, preg_of r <> SP.
-Proof.
-  intros. unfold preg_of; destruct r; simpl; congruence.
-Qed.
-
-Lemma preg_of_not_PC:
-  forall r, preg_of r <> PC.
-Proof.
-  intros. apply data_diff; auto with asmgen.
-Qed.
-
-Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
-
-Lemma nextblock_pc:
-  forall b rs, (nextblock b rs)#PC = Val.offset_ptr rs#PC (Ptrofs.repr (size b)).
-Proof.
-  intros. apply Pregmap.gss.
-Qed.
-
-Lemma nextblock_inv:
-  forall b r rs, r <> PC -> (nextblock b rs)#r = rs#r.
-Proof.
-  intros. unfold nextblock. apply Pregmap.gso. red; intro; subst. auto.
-Qed.
-
-Lemma nextblock_inv1:
-  forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r.
-Proof.
-  intros. apply nextblock_inv. red; intro; subst; discriminate.
-Qed.
-
 Lemma undef_regs_other:
   forall r rl rs,
   (forall r', In r' rl -> r <> r') ->
@@ -294,9 +241,9 @@ Qed.
 Lemma agree_undef_caller_save_regs:
   forall ms sp rs,
   agree ms sp rs ->
-  agree (Mach.undef_caller_save_regs ms) sp (Asmvliw.undef_caller_save_regs rs).
+  agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs).
 Proof.
-  intros. destruct H. unfold Mach.undef_caller_save_regs, Asmvliw.undef_caller_save_regs; split.
+  intros. destruct H. unfold Mach.undef_caller_save_regs, 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). 
@@ -752,6 +699,19 @@ Proof.
   intros. destruct H. auto.
 Qed.
 
+Lemma exec_body_pc:
+  forall ge l rs1 m1 rs2 m2,
+  exec_body ge l rs1 m1 = Next rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  induction l.
+  - intros. inv H. auto.
+  - intros until m2. intro EXEB.
+    inv EXEB. destruct (exec_basic_instr _ _ _ _) eqn:EBI; try discriminate.
+    eapply IHl in H0. rewrite H0.
+    erewrite exec_basic_instr_pc; eauto.
+Qed.
+
 Section STRAIGHTLINE.
 
 Variable ge: genv.
@@ -880,69 +840,6 @@ Qed.
 
 (** Linking exec_straight with exec_straight_blocks *)
 
-Ltac Simplif :=
-  ((rewrite nextblock_inv by eauto with asmgen)
-  || (rewrite nextblock_inv1 by eauto with asmgen)
-  || (rewrite Pregmap.gss)
-  || (rewrite nextblock_pc)
-  || (rewrite Pregmap.gso by eauto with asmgen)
-  ); auto with asmgen.
-
-Ltac Simpl := repeat Simplif.
-
-Lemma exec_basic_instr_pc:
-  forall b rs1 m1 rs2 m2,
-  exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
-  rs2 PC = rs1 PC.
-Proof.
-  intros. destruct b; try destruct i; try destruct i.
-  all: try (inv H; Simpl).
-  1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  { (* PLoadQRRO *)
-    unfold  parexec_load_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  { (* PLoadORRO *)
-    unfold  parexec_load_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
-  1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  
-  { (* PStoreQRRO *)
-    unfold  parexec_store_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  { (* PStoreORRO *)
-    unfold  parexec_store_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
-  - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
-    destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
-  - destruct rs; try discriminate. inv H1. Simpl.
-  - destruct rd; try discriminate. inv H1; Simpl.
-  - reflexivity.
-Qed.
-
 Lemma exec_straight_pc:
   forall c c' rs1 m1 rs2 m2,
   exec_straight c rs1 m1 c' rs2 m2 ->
diff --git a/powerpc/DuplicateOpcodeHeuristic.ml b/powerpc/DuplicateOpcodeHeuristic.ml
new file mode 100644
index 00000000..85505245
--- /dev/null
+++ b/powerpc/DuplicateOpcodeHeuristic.ml
@@ -0,0 +1,3 @@
+exception HeuristicSucceeded
+        
+let opcode_heuristic code cond ifso ifnot preferred = ()
diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml
index 3e734747..1df63308 100644
--- a/riscV/Asmexpand.ml
+++ b/riscV/Asmexpand.ml
@@ -483,7 +483,7 @@ let expand_instruction instr =
       emit (Pmv (X30, X2));
       if sg.sig_cc.cc_vararg then begin
         let n = arguments_size sg in
-        let extra_sz = if n >= 8 then 0 else align 16 ((8 - n) * wordsize) in
+        let extra_sz = if n >= 8 then 0 else align ((8 - n) * wordsize) 16 in
         let full_sz = Z.add sz (Z.of_uint extra_sz) in
         expand_addptrofs X2 X2 (Ptrofs.repr (Z.neg full_sz));
         expand_storeind_ptr X30 X2 ofs;
@@ -501,7 +501,7 @@ let expand_instruction instr =
      let extra_sz =
       if sg.sig_cc.cc_vararg then begin
         let n = arguments_size sg in
-        if n >= 8 then 0 else align 16 ((8 - n) * wordsize)
+        if n >= 8 then 0 else align ((8 - n) * wordsize) 16
       end else 0 in
      expand_addptrofs X2 X2 (Ptrofs.repr (Z.add sz (Z.of_uint extra_sz)))
 
diff --git a/riscV/DuplicateOpcodeHeuristic.ml b/riscV/DuplicateOpcodeHeuristic.ml
new file mode 100644
index 00000000..85505245
--- /dev/null
+++ b/riscV/DuplicateOpcodeHeuristic.ml
@@ -0,0 +1,3 @@
+exception HeuristicSucceeded
+        
+let opcode_heuristic code cond ifso ifnot preferred = ()
diff --git a/runtime/powerpc/i64_dtos.s b/runtime/powerpc/i64_dtos.s
new file mode 100644
index 00000000..85c60b27
--- /dev/null
+++ b/runtime/powerpc/i64_dtos.s
@@ -0,0 +1,100 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Conversion from double float to signed long	
+
+        .balign 16
+        .globl __compcert_i64_dtos
+__compcert_i64_dtos:
+        stfdu f1, -16(r1)       # extract LO (r4) and HI (r3) halves of double
+        lwz r3, 0(r1)
+        lwz r4, 4(r1)
+        addi r1, r1, 16
+        srawi r10, r3, 31       # save sign of double in r10
+ # extract unbiased exponent  ((HI & 0x7FF00000) >> 20) - (1023 + 52)
+        rlwinm r5, r3, 12, 21, 31
+        addi r5, r5, -1075
+ # check range of exponent
+        cmpwi r5, -52           # if EXP < -52, abs(double) is < 1.0
+        blt 1f
+        cmpwi r5, 11            # if EXP >= 63 - 52, abs(double) is >= 2^63
+        bge 2f
+  # extract true mantissa
+        rlwinm r3, r3, 0, 12, 31  # HI &= ~0xFFF00000
+        oris r3, r3, 0x10         # HI |=  0x00100000
+  # shift it appropriately
+        cmpwi r5, 0
+        blt 3f
+  # if EXP >= 0, shift left by EXP.  Note that EXP < 11.
+        subfic r6, r5, 32       # r6 = 32 - EXP
+        slw r3, r3, r5
+        srw r0, r4, r6
+        or r3, r3, r0
+        slw r4, r4, r5
+        b 4f
+  # if EXP < 0, shift right by -EXP.  Note that -EXP <= 52 but can be >= 32.
+3:      subfic r5, r5, 0        # r5 = -EXP = shift amount
+        subfic r6, r5, 32       # r6 = 32 - amount
+        addi r7, r5, -32        # r7 = amount - 32  (see i64_shr.s)
+        srw r4, r4, r5
+        slw r0, r3, r6
+        or r4, r4, r0
+        srw r0, r3, r7
+        or r4, r4, r0
+        srw r3, r3, r5
+  # apply sign to result	
+4:      xor r4, r4, r10
+        xor r3, r3, r10
+        subfc r4, r10, r4
+        subfe r3, r10, r3
+        blr
+  # Special cases
+1:      li r3, 0                # result is 0
+        li r4, 0
+        blr
+2:      li r4, -1               # result is MAX_SINT or MIN_SINT
+        bge 5f                  # depending on sign
+        li r4, -1               # result is MAX_SINT =  0x7FFF_FFFF
+        srwi r3, r4, 1
+        blr
+5:      lis r3, 0x8000          # result is MIN_SINT = 0x8000_0000
+        li r4, 0
+        blr
+        .type __compcert_i64_dtos, @function
+        .size __compcert_i64_dtos, .-__compcert_i64_dtos
+        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_dtou.s b/runtime/powerpc/i64_dtou.s
new file mode 100644
index 00000000..67a721d4
--- /dev/null
+++ b/runtime/powerpc/i64_dtou.s
@@ -0,0 +1,92 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Conversion from double float to unsigned long	
+
+        .balign 16
+        .globl __compcert_i64_dtou
+__compcert_i64_dtou:
+        stfdu f1, -16(r1)       # extract LO (r4) and HI (r3) halves of double
+        lwz r3, 0(r1)
+        lwz r4, 4(r1)
+        addi r1, r1, 16
+        cmpwi r3, 0             # is double < 0?
+        blt 1f                  # then it converts to 0
+  # extract unbiased exponent  ((HI & 0x7FF00000) >> 20) - (1023 + 52)
+        rlwinm r5, r3, 12, 21, 31
+        addi r5, r5, -1075
+  # check range of exponent
+        cmpwi r5, -52           # if EXP < -52, double is < 1.0
+        blt 1f
+        cmpwi r5, 12            # if EXP >= 64 - 52, double is >= 2^64
+        bge 2f
+  # extract true mantissa
+        rlwinm r3, r3, 0, 12, 31  # HI &= ~0xFFF00000
+        oris r3, r3, 0x10         # HI |=  0x00100000
+  # shift it appropriately
+        cmpwi r5, 0
+        blt 3f
+  # if EXP >= 0, shift left by EXP.  Note that EXP < 12.
+        subfic r6, r5, 32       # r6 = 32 - EXP
+        slw r3, r3, r5
+        srw r0, r4, r6
+        or r3, r3, r0
+        slw r4, r4, r5
+        blr
+  # if EXP < 0, shift right by -EXP.  Note that -EXP <= 52 but can be >= 32.
+3:      subfic r5, r5, 0        # r5 = -EXP = shift amount
+        subfic r6, r5, 32       # r6 = 32 - amount
+        addi r7, r5, -32        # r7 = amount - 32 (see i64_shr.s)
+        srw r4, r4, r5
+        slw r0, r3, r6
+        or r4, r4, r0
+        srw r0, r3, r7
+        or r4, r4, r0
+        srw r3, r3, r5
+        blr
+  # Special cases
+1:      li r3, 0                # result is 0
+        li r4, 0
+        blr
+2:      li r3, -1               # result is MAX_UINT
+        li r4, -1
+        blr
+        .type __compcert_i64_dtou, @function
+        .size __compcert_i64_dtou, .-__compcert_i64_dtou
+
+        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_sar.s b/runtime/powerpc/i64_sar.s
new file mode 100644
index 00000000..c7da448f
--- /dev/null
+++ b/runtime/powerpc/i64_sar.s
@@ -0,0 +1,60 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+# Shift right signed	
+	
+        .balign 16
+        .globl __compcert_i64_sar
+__compcert_i64_sar:
+        andi. r5, r5, 63        # take amount modulo 64
+        cmpwi r5, 32
+        bge 1f                  # amount < 32?
+        subfic r6, r5, 32       # r6 = 32 - amount
+        srw r4, r4, r5          # RH = XH >>s amount
+        slw r0, r3, r6          # RL = XL >>u amount | XH << (32 - amount)
+        or r4, r4, r0
+        sraw r3, r3, r5
+        blr
+1:      addi r6, r5, -32        # amount >= 32
+        sraw r4, r3, r6         # RL = XH >>s (amount - 32)
+        srawi r3, r3, 31        # RL = sign extension of XH
+        blr
+        .type __compcert_i64_sar, @function
+        .size __compcert_i64_sar, .-__compcert_i64_sar
+
+        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_sdiv.s b/runtime/powerpc/i64_sdiv.s
new file mode 100644
index 00000000..9787ea3b
--- /dev/null
+++ b/runtime/powerpc/i64_sdiv.s
@@ -0,0 +1,71 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Signed division	
+	
+        .balign 16
+        .globl __compcert_i64_sdiv
+__compcert_i64_sdiv:
+	mflr r0
+        stw r0, 4(r1)           # save return address in caller's frame
+        xor r0, r3, r5          # compute sign of result (top bit)
+	mtctr r0                # save it in CTR (why not?)
+        srawi r0, r3, 31        # take absolute value of N
+        xor r4, r4, r0          # (i.e.  N = N ^ r0 - r0,
+        xor r3, r3, r0          #  where r0 = 0 if N >= 0 and r0 = -1 if N < 0)
+        subfc r4, r0, r4
+        subfe r3, r0, r3
+        srawi r0, r5, 31        # take absolute value of D
+        xor r6, r6, r0          # (same trick)
+        xor r5, r5, r0
+        subfc r6, r0, r6
+        subfe r5, r0, r5
+        bl __compcert_i64_udivmod        # do unsigned division
+        lwz r0, 4(r1)
+        mtlr r0                 # restore return address
+        mfctr r0
+        srawi r0, r0, 31        # apply expected sign to quotient
+        xor r6, r6, r0          # RES = Q if CTR >= 0, -Q if CTR < 0
+        xor r5, r5, r0
+        subfc r4, r0, r6
+        subfe r3, r0, r5
+        blr
+        .type __compcert_i64_sdiv, @function
+        .size __compcert_i64_sdiv, .-__compcert_i64_sdiv
+	
+        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_shl.s b/runtime/powerpc/i64_shl.s
new file mode 100644
index 00000000..f6edb6c2
--- /dev/null
+++ b/runtime/powerpc/i64_shl.s
@@ -0,0 +1,64 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+# Shift left
+	
+        .balign 16
+        .globl __compcert_i64_shl
+__compcert_i64_shl:
+# On PowerPC, shift instructions with amount mod 64 >= 32 return 0
+# hi = (hi << amount) | (lo >> (32 - amount)) | (lo << (amount - 32))
+# lo = lo << amount
+# if 0 <= amount < 32:
+#    (amount - 32) mod 64 >= 32, hence lo << (amount - 32) == 0
+# if 32 <= amount < 64:
+#    lo << amount == 0
+#    (32 - amount) mod 64 >= 32, hence lo >> (32 - amount) == 0
+        andi. r5, r5, 63        # take amount modulo 64
+        subfic r6, r5, 32       # r6 = 32 - amount
+        addi r7, r5, -32        # r7 = amount - 32
+        slw r3, r3, r5
+        srw r0, r4, r6
+        or r3, r3, r0
+        slw r0, r4, r7
+        or r3, r3, r0
+        slw r4, r4, r5
+        blr
+        .type __compcert_i64_shl, @function
+        .size __compcert_i64_shl, .-__compcert_i64_shl
+        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_shr.s b/runtime/powerpc/i64_shr.s
new file mode 100644
index 00000000..b634aafd
--- /dev/null
+++ b/runtime/powerpc/i64_shr.s
@@ -0,0 +1,65 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+# Shift right unsigned
+	
+        .balign 16
+        .globl __compcert_i64_shr
+__compcert_i64_shr:
+# On PowerPC, shift instructions with amount mod 64 >= 32 return 0
+# lo = (lo >> amount) | (hi << (32 - amount)) | (hi >> (amount - 32))
+# hi = hi >> amount
+# if 0 <= amount < 32:
+#    (amount - 32) mod 64 >= 32, hence hi >> (amount - 32) == 0
+# if 32 <= amount < 64:
+#    hi >> amount == 0
+#    (32 - amount) mod 64 >= 32, hence hi << (32 - amount) == 0
+        andi. r5, r5, 63        # take amount modulo 64
+        subfic r6, r5, 32       # r6 = 32 - amount
+        addi r7, r5, -32        # r7 = amount - 32
+        srw r4, r4, r5
+        slw r0, r3, r6
+        or r4, r4, r0
+        srw r0, r3, r7
+        or r4, r4, r0
+        srw r3, r3, r5
+        blr
+        .type __compcert_i64_shr, @function
+        .size __compcert_i64_shr, .-__compcert_i64_shr
+	
+        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_smod.s b/runtime/powerpc/i64_smod.s
new file mode 100644
index 00000000..6b4e1f89
--- /dev/null
+++ b/runtime/powerpc/i64_smod.s
@@ -0,0 +1,70 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+## Signed remainder	
+	
+        .balign 16
+        .globl __compcert_i64_smod
+__compcert_i64_smod:
+	mflr r0
+        stw r0, 4(r1)           # save return address in caller's frame
+	mtctr r3                # save sign of result in CTR (sign of N)
+        srawi r0, r3, 31        # take absolute value of N
+        xor r4, r4, r0          # (i.e.  N = N ^ r0 - r0,
+        xor r3, r3, r0          #  where r0 = 0 if N >= 0 and r0 = -1 if N < 0)
+        subfc r4, r0, r4
+        subfe r3, r0, r3
+        srawi r0, r5, 31        # take absolute value of D
+        xor r6, r6, r0          # (same trick)
+        xor r5, r5, r0
+        subfc r6, r0, r6
+        subfe r5, r0, r5
+        bl __compcert_i64_udivmod        # do unsigned division
+        lwz r0, 4(r1)
+        mtlr r0                 # restore return address
+        mfctr r0
+        srawi r0, r0, 31        # apply expected sign to remainder
+        xor r4, r4, r0          # RES = R if CTR >= 0, -Q if CTR < 0
+        xor r3, r3, r0
+        subfc r4, r0, r4
+        subfe r3, r0, r3
+        blr
+        .type __compcert_i64_smod, @function
+        .size __compcert_i64_smod, .-__compcert_i64_smod
+
+        
\ No newline at end of file
diff --git a/runtime/powerpc/i64_smulh.s b/runtime/powerpc/i64_smulh.s
new file mode 100644
index 00000000..73393fce
--- /dev/null
+++ b/runtime/powerpc/i64_smulh.s
@@ -0,0 +1,80 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris
+#
+# Copyright (c) 2016 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Signed multiply-high
+
+# Hacker's Delight section 8.3:
+# - compute high 64 bits of the unsigned product X * Y  (see i64_umulh.S)
+# - subtract X if Y < 0
+# - subtract Y if X < 0
+
+        .balign 16
+        .globl __compcert_i64_smulh
+__compcert_i64_smulh:
+# r7:r8:r9 accumulate bits 127:32 of the full unsigned product
+        mulhwu  r9, r4, r6        # r9 = high half of XL.YL
+        mullw   r0, r4, r5        # r0 = low half of XL.YH
+        addc    r9, r9, r0
+        mulhwu  r0, r4, r5        # r0 = high half of XL.YH
+        addze   r8, r0
+        mullw   r0, r3, r6        # r0 = low half of XH.YL
+        addc    r9, r9, r0
+        mulhwu  r0, r3, r6        # r0 = high half of XH.YL
+        adde    r8, r8, r0
+        li      r7, 0
+        addze   r7, r7
+        mullw   r0, r3, r5        # r0 = low half of XH.YH
+        addc    r8, r8, r0
+        mulhwu  r0, r3, r5        # r0 = high half of XH.YH
+        adde    r7, r7, r0
+# Here r7:r8 contains the high 64 bits of the unsigned product.
+# Now, test signs and subtract if needed
+        srawi   r0, r3, 31        # r0 = -1 if X < 0, r0 = 0 if X >= 0
+        srawi   r9, r5, 31        # r9 = -1 if Y < 0, r9 = 0 if Y >= 0
+        and     r3, r3, r9        # set X = 0 if Y >= 0
+        and     r4, r4, r9
+        and     r5, r5, r0        # set Y = 0 if X >= 0
+        and     r6, r6, r0
+        subfc   r8, r4, r8        # subtract X
+        subfe   r7, r3, r7
+        subfc   r4, r6, r8        # subtract Y
+        subfe   r3, r5, r7
+        blr
+        .type __compcert_i64_smulh, @function
+        .size __compcert_i64_smulh, .-__compcert_i64_smulh
+
diff --git a/runtime/powerpc/i64_stod.s b/runtime/powerpc/i64_stod.s
new file mode 100644
index 00000000..0c1ab720
--- /dev/null
+++ b/runtime/powerpc/i64_stod.s
@@ -0,0 +1,67 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+### Conversion from signed long to double float	
+
+        .balign 16
+        .globl __compcert_i64_stod
+__compcert_i64_stod:
+        addi r1, r1, -16
+        lis r5, 0x4330
+        li r6, 0
+        stw r5, 0(r1)
+        stw r4, 4(r1)           # 0(r1) = 2^52 + (double) XL
+        stw r5, 8(r1)
+        stw r6, 12(r1)          # 8(r1) = 2^52
+        lfd f1, 0(r1)
+        lfd f2, 8(r1)
+        fsub f1, f1, f2         # f1 is XL (unsigned) as a double
+        lis r5, 0x4530
+        lis r6, 0x8000
+        stw r5, 0(r1)           # 0(r1) = 2^84 + ((double)XH - 2^31) * 2^32
+        add r3, r3, r6
+        stw r3, 4(r1)
+        stw r5, 8(r1)           # 8(r1) = 2^84 + 2^31 * 2^32
+        stw r6, 12(r1)
+        lfd f2, 0(r1)
+        lfd f3, 8(r1)
+        fsub f2, f2, f3         # f2 is XH (signed) * 2^32 as a double
+        fadd f1, f1, f2         # add both to get result
+        addi r1, r1, 16
+        blr
+        .type __compcert_i64_stod, @function
+        .size __compcert_i64_stod, .-__compcert_i64_stod
+
diff --git a/runtime/powerpc/i64_stof.s b/runtime/powerpc/i64_stof.s
new file mode 100644
index 00000000..97fa6bb8
--- /dev/null
+++ b/runtime/powerpc/i64_stof.s
@@ -0,0 +1,68 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Conversion from signed long to single float	
+
+        .balign 16
+        .globl __compcert_i64_stof
+__compcert_i64_stof:
+	mflr r9
+   # Check whether -2^53 <= X < 2^53	
+        srawi r5, r3, 31
+        srawi r6, r3, 21        # (r5,r6) = X >> 53
+        addic r6, r6, 1
+        addze r5, r5            # (r5,r6) = (X >> 53) + 1
+        cmplwi r5, 2
+        blt 1f
+   # X is large enough that double rounding can occur.
+   # Avoid it by nudging X away from the points where double rounding
+   # occurs (the "round to odd" technique)
+        rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
+        addi r0, r0, 0x7FF      # r0 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-31 of r0 are 0
+        or r4, r4, r0           # correct bit number 12 of X
+        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single	
+1:      bl __compcert_i64_stod
+        mtlr r9
+        frsp f1, f1
+        blr
+        .type __compcert_i64_stof, @function
+        .size __compcert_i64_stof, .-__compcert_i64_stof
+	
diff --git a/runtime/powerpc/i64_udiv.s b/runtime/powerpc/i64_udiv.s
new file mode 100644
index 00000000..e2da855a
--- /dev/null
+++ b/runtime/powerpc/i64_udiv.s
@@ -0,0 +1,54 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Unsigned division	
+
+        .balign 16
+        .globl __compcert_i64_udiv
+__compcert_i64_udiv:
+	mflr r0
+        stw r0, 4(r1)           # save return address in caller's frame
+        bl __compcert_i64_udivmod        # unsigned divide
+        lwz r0, 4(r1)
+        mtlr r0                 # restore return address
+        mr r3, r5               # result = quotient
+        mr r4, r6
+        blr
+        .type __compcert_i64_udiv, @function
+        .size __compcert_i64_udiv, .-__compcert_i64_udiv
+
diff --git a/runtime/powerpc/i64_udivmod.s b/runtime/powerpc/i64_udivmod.s
new file mode 100644
index 00000000..e81c6cef
--- /dev/null
+++ b/runtime/powerpc/i64_udivmod.s
@@ -0,0 +1,234 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+	.text
+	
+# Unsigned division and modulus
+
+# This function computes both the quotient and the remainder of two
+# unsigned 64-bit integers.
+
+# Input:  numerator N in (r3,r4), divisor D in (r5,r6)
+# Output: quotient Q in (r5,r6),  remainder R in (r3,r4)
+# Destroys: all integer caller-save registers
+	
+	.globl  __compcert_i64_udivmod
+	.balign 16
+__compcert_i64_udivmod:
+        cmplwi  r5, 0           # DH == 0 ?
+	stwu    r1, -32(r1)
+        mflr    r0
+        stw     r0, 8(r1)
+        stw     r31, 12(r1)
+        beq     1f
+# The general case	
+        stw     r30, 16(r1)
+        stw     r29, 20(r1)
+        stw     r28, 24(r1)
+        mr      r28, r3         # Save N in (r28, r29)
+        mr      r29, r4
+        mr      r30, r5         # Save D in (r30, r31)
+        mr      r31, r6 
+  # Scale N and D down, giving N' and D', such that 2^31 <= D' < 2^32
+        cntlzw  r7, r5          # r7 = leading zeros in DH = 32 - shift amount
+        subfic  r8, r7, 32      # r8 = shift amount
+	slw     r0, r3, r7      # N' = N >> shift amount
+        srw     r3, r3, r8
+        srw     r4, r4, r8
+        or      r4, r4, r0
+	slw     r0, r5, r7      # D' = D >> shift amount
+        srw     r6, r6, r8
+        or      r5, r6, r0
+  # Divide N' by D' to get an approximate quotient Q
+        bl      __compcert_i64_udiv6432  # r3 = quotient, r4 = remainder
+        mr      r6, r3          # low half of quotient Q
+        li      r5, 0           # high half of quotient is 0
+  # Tentative quotient is either correct or one too high
+  # Compute Q * D in (r7, r8)
+4:      mullw   r7, r6, r30     # r7 = Q * DH
+        mullw   r8, r6, r31     # r8 = low 32 bits of Q * DL
+        mulhwu  r0, r6, r31     # r0 = high 32 bits of Q * DL
+        addc    r7, r7, r0
+        subfe.  r0, r0, r0      # test carry: EQ iff carry
+        beq     2f              # handle overflow case
+   # Compute R = N - Q * D, with borrow
+        subfc   r4, r8, r29
+        subfe   r3, r7, r28
+        subfe.  r0, r0, r0      # test borrow: EQ iff no borrow
+        beq     3f              # no borrow: N >= Q * D, we are good
+        addi    r6, r6, -1      # borrow: adjust Q down by 1
+        addc    r4, r4, r31     # and R up by D
+        adde    r3, r3, r30
+   # Finished	
+3:      lwz     r0, 8(r1)
+        mtlr    r0
+        lwz     r31, 12(r1)
+        lwz     r30, 16(r1)
+        lwz     r29, 20(r1)
+        lwz     r28, 24(r1)
+        addi    r1, r1, 32
+        blr
+   # Special case when Q * D overflows
+2:      addi    r6, r6, -1      # adjust Q down by 1
+        b       4b              # and redo computation and check of remainder
+	.balign 16
+# Special case 64 bits divided by 32 bits
+1:      cmplwi  r3, 0           # NH == 0?
+        beq     4f
+        divwu   r31, r3, r6     # Divide NH by DL, quotient QH in r31
+        mullw   r0, r31, r6
+        subf    r3, r0, r3      # NH is remainder of this division
+        mr      r5, r6
+        bl      __compcert_i64_udiv6432  # divide NH : NL by DL
+        mr      r5, r31         # high word of quotient
+        mr      r6, r3          # low word of quotient
+                                # r4 contains low word of remainder
+        li      r3, 0           # high word of remainder = 0
+	lwz     r0, 8(r1)
+        mtlr    r0
+        lwz     r31, 12(r1)
+        addi    r1, r1, 32
+        blr
+	.balign 16
+# Special case 32 bits divided by 32 bits
+4:      mr      r0, r6
+	divwu   r6, r4, r6      # low word of quotient
+	li      r5, 0           # high word of quotient is 0
+        mullw   r0, r6, r0
+        subf    r4, r0, r4      # low word of remainder
+        li      r3, 0           # high word of remainder is 0
+        addi    r1, r1, 32
+        blr
+        
+        .type __compcert_i64_udivmod, @function
+        .size __compcert_i64_udivmod, .-__compcert_i64_udivmod
+
+# Auxiliary division function: 64 bit integer divided by 32 bit integer	
+# Not exported
+# Input:  numerator N in (r3,r4), divisor D in r5
+# Output: quotient Q in r3, remainder R in r4
+# Destroys: all integer caller-save registers
+# Assumes: high word of N is less than D	
+        
+	.balign 16
+__compcert_i64_udiv6432: 
+# Algorithm 9.3 from Hacker's Delight, section 9.4	
+# Initially: u1 in r3, u0 in r4, v in r5
+#   s = __builtin_clz(v);
+	cntlzw  r6, r5          # s in r6
+#   v = v << s;
+        slw     r5, r5, r6
+#   vn1 = v >> 16;              # vn1 in r7
+        srwi    r7, r5, 16
+#   vn0 = v & 0xFFFF;           # vn0 in r8
+        rlwinm  r8, r5, 0, 16, 31
+#   un32 = (u1 << s) | (u0 >> 32 - s);
+	subfic  r0, r6, 32
+        srw     r0, r4, r0
+        slw     r3, r3, r6     # u1 dies, un32 in r3
+        or      r3, r3, r0
+#   un10 = u0 << s;
+        slw     r4, r4, r6     # u0 dies, un10 in r4
+#   un1 = un10 >> 16;
+        srwi    r9, r4, 16     # un1 in r9
+#   un0 = un10 & 0xFFFF;
+        rlwinm  r4, r4, 0, 16, 31 # un10 dies, un0 in r4
+#   q1 = un32/vn1;
+        divwu   r10, r3, r7    # q in r10
+#   rhat = un32 - q1*vn1;
+        mullw   r0, r10, r7
+        subf    r11, r0, r3    # rhat in r11
+#  again1:
+1:      
+#   if (q1 >= b || q1*vn0 > b*rhat + un1) {
+        cmplwi  r10, 0xFFFF
+        bgt     2f
+        mullw   r0, r10, r8
+        slwi    r12, r11, 16
+        add     r12, r12, r9
+        cmplw   r0, r12
+        ble     3f
+2:      
+#     q1 = q1 - 1;
+        addi    r10, r10, -1
+#     rhat = rhat + vn1;
+        add     r11, r11, r7
+#     if (rhat < b) goto again1;}
+        cmplwi  r11, 0xFFFF
+        ble     1b
+3:      
+#   un21 = un32*b + un1 - q1*v;
+        slwi    r0, r3, 16     # un32 dies
+        add     r9, r0, r9     # un1 dies
+        mullw   r0, r10, r5
+        subf    r9, r0, r9     # un21 in r9
+#   q0 = un21/vn1;
+	divwu   r3, r9, r7     # q0 in r3
+#   rhat = un21 - q0*vn1;
+        mullw   r0, r3, r7
+        subf    r11, r0, r9    # rhat in r11
+# again2:
+4:      
+#   if (q0 >= b || q0*vn0 > b*rhat + un0) {
+        cmplwi  r3, 0xFFFF
+        bgt     5f
+        mullw   r0, r3, r8
+        slwi    r12, r11, 16
+        add     r12, r12, r4
+        cmplw   r0, r12
+        ble     6f
+5:      
+#     q0 = q0 - 1;
+	addi    r3, r3, -1
+#     rhat = rhat + vn1;
+        add     r11, r11, r7
+#     if (rhat < b) goto again2;}
+	cmplwi  r11, 0xFFFF
+        ble     4b
+6:      
+#   remainder = (un21*b + un0 - q0*v) >> s;
+        slwi    r0, r9, 16
+        add     r4, r0, r4  # un0 dies, remainder in r4
+        mullw   r0, r3, r5
+        subf    r4, r0, r4
+        srw     r4, r4, r6
+#   quotient = q1*b + q0;
+        slwi    r0, r10, 16
+        add     r3, r0, r3
+        blr
+
+	.type	__compcert_i64_udiv6432, @function
+	.size	__compcert_i64_udiv6432,.-__compcert_i64_udiv6432
diff --git a/runtime/powerpc/i64_umod.s b/runtime/powerpc/i64_umod.s
new file mode 100644
index 00000000..bf8d6121
--- /dev/null
+++ b/runtime/powerpc/i64_umod.s
@@ -0,0 +1,47 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Unsigned modulus
+
+        .balign 16
+        .globl __compcert_i64_umod
+__compcert_i64_umod:
+        b __compcert_i64_udivmod
+        .type __compcert_i64_umod, @function
+        .size __compcert_i64_umod, .-__compcert_i64_umod
+
diff --git a/runtime/powerpc/i64_umulh.s b/runtime/powerpc/i64_umulh.s
new file mode 100644
index 00000000..53b72948
--- /dev/null
+++ b/runtime/powerpc/i64_umulh.s
@@ -0,0 +1,65 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris
+#
+# Copyright (c) 2016 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Unsigned multiply-high
+
+# X * Y = 2^64 XH.YH + 2^32 (XH.YL + XL.YH) + XL.YL
+
+        .balign 16
+        .globl __compcert_i64_umulh
+__compcert_i64_umulh:
+# r7:r8:r9 accumulate bits 127:32 of the full product
+        mulhwu  r9, r4, r6        # r9 = high half of XL.YL
+        mullw   r0, r4, r5        # r0 = low half of XL.YH
+        addc    r9, r9, r0
+        mulhwu  r0, r4, r5        # r0 = high half of XL.YH
+        addze   r8, r0
+        mullw   r0, r3, r6        # r0 = low half of XH.YL
+        addc    r9, r9, r0
+        mulhwu  r0, r3, r6        # r0 = high half of XH.YL
+        adde    r8, r8, r0
+        li      r7, 0
+        addze   r7, r7
+        mullw   r0, r3, r5        # r0 = low half of XH.YH
+        addc    r4, r8, r0
+        mulhwu  r0, r3, r5        # r0 = high half of XH.YH
+        adde    r3, r7, r0
+        blr
+        .type __compcert_i64_umulh, @function
+        .size __compcert_i64_umulh, .-__compcert_i64_umulh
+
diff --git a/runtime/powerpc/i64_utod.s b/runtime/powerpc/i64_utod.s
new file mode 100644
index 00000000..69de6fdb
--- /dev/null
+++ b/runtime/powerpc/i64_utod.s
@@ -0,0 +1,66 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Conversion from unsigned long to double float	
+
+        .balign 16
+        .globl __compcert_i64_utod
+__compcert_i64_utod:
+        addi r1, r1, -16
+        lis r5, 0x4330
+        li r6, 0
+        stw r5, 0(r1)
+        stw r4, 4(r1)           # 0(r1) = 2^52 + (double) XL
+        stw r5, 8(r1)
+        stw r6, 12(r1)          # 8(r1) = 2^52
+        lfd f1, 0(r1)
+        lfd f2, 8(r1)
+        fsub f1, f1, f2         # f1 is (double) XL
+        lis r5, 0x4530
+        stw r5, 0(r1)           # 0(r1) = 2^84 + (double) XH * 2^32
+        stw r3, 4(r1)
+        stw r5, 8(r1)           # 8(r1) = 2^84
+        lfd f2, 0(r1)
+        lfd f3, 8(r1)
+        fsub f2, f2, f3         # f2 is XH * 2^32 as a double
+        fadd f1, f1, f2         # add both to get result
+        addi r1, r1, 16
+        blr
+        .type __compcert_i64_utod, @function
+        .size __compcert_i64_utod, .-__compcert_i64_utod
+	
diff --git a/runtime/powerpc/i64_utof.s b/runtime/powerpc/i64_utof.s
new file mode 100644
index 00000000..cdb2f867
--- /dev/null
+++ b/runtime/powerpc/i64_utof.s
@@ -0,0 +1,64 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Conversion from unsigned long to single float	
+
+        .balign 16
+        .globl __compcert_i64_utof
+__compcert_i64_utof:
+	mflr r9
+   # Check whether X < 2^53	
+        andis. r0, r3, 0xFFE0       # test bits 53...63 of X
+        beq 1f
+   # X is large enough that double rounding can occur.
+   # Avoid it by nudging X away from the points where double rounding
+   # occurs (the "round to odd" technique)
+        rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
+        addi r0, r0, 0x7FF      # r0 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-31 of r0 are 0
+        or r4, r4, r0           # correct bit number 12 of X
+        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single	
+1:      bl __compcert_i64_utod
+        mtlr r9
+        frsp f1, f1
+        blr
+        .type __compcert_i64_utof, @function
+        .size __compcert_i64_utof, .-__compcert_i64_utof
+	
diff --git a/runtime/powerpc/vararg.s b/runtime/powerpc/vararg.s
new file mode 100644
index 00000000..8d7e62c8
--- /dev/null
+++ b/runtime/powerpc/vararg.s
@@ -0,0 +1,163 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for variadic functions <stdarg.h>.  IA32 version
+
+# typedef struct {
+#   unsigned char ireg;    // index of next integer register
+#   unsigned char freg;    // index of next FP register
+#   char * stk;            // pointer to next argument in stack
+#   struct {
+#     int iregs[8];
+#     double fregs[8];
+#   } * regs;              // pointer to saved register area
+# } va_list[1];
+#
+# unsigned int __compcert_va_int32(va_list ap);
+# unsigned long long __compcert_va_int64(va_list ap);
+# double __compcert_va_float64(va_list ap);
+
+        .text
+
+        .balign 16
+        .globl __compcert_va_int32
+__compcert_va_int32:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 0(r3)       # r4 = ap->ireg = next integer register
+        cmplwi  r4, 8
+        bge     1f
+  # Next argument was passed in an integer register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+        rlwinm  r6, r4, 2, 0, 29 # r6 = r4 * 4
+	addi    r4, r4, 1       # increment ap->ireg
+        stb     r4, 0(r3)
+        lwzx    r3, r5, r6      # load argument in r3
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+        addi    r5, r5, 4       # advance ap->stk by 4
+        stw     r5, 4(r3)
+	lwz     r3, -4(r5)      # load argument in r3
+        blr
+        .type   __compcert_va_int32, @function
+        .size   __compcert_va_int32, .-__compcert_va_int32
+
+        .balign 16
+        .globl __compcert_va_int64
+__compcert_va_int64:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 0(r3)       # r4 = ap->ireg = next integer register
+        cmplwi  r4, 7
+        bge     1f
+  # Next argument was passed in two consecutive integer register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+	addi    r4, r4, 3       # round r4 up to an even number and add 2
+        rlwinm  r4, r4, 0, 0, 30 
+        rlwinm  r6, r4, 2, 0, 29 # r6 = r4 * 4
+	add     r5, r5, r6      # r5 = address of argument + 8
+        stb     r4, 0(r3)       # update ap->ireg
+        lwz     r3, -8(r5)      # load argument in r3:r4
+        lwz     r4, -4(r5)
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+	li      r4, 8
+        stb     r4, 0(r3)       # set ap->ireg = 8 so that no ireg is left
+	addi    r5, r5, 15      # round r5 to a multiple of 8 and add 8
+        rlwinm  r5, r5, 0, 0, 28
+	stw     r5, 4(r3)       # update ap->stk
+        lwz     r3, -8(r5)      # load argument in r3:r4
+        lwz     r4, -4(r5)
+        blr
+        .type   __compcert_va_int64, @function
+        .size   __compcert_va_int64, .-__compcert_va_int64
+
+        .balign 16
+        .globl __compcert_va_float64
+__compcert_va_float64:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 1(r3)       # r4 = ap->freg = next float register
+        cmplwi  r4, 8
+        bge     1f
+  # Next argument was passed in a FP register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+        rlwinm  r6, r4, 3, 0, 28 # r6 = r4 * 8
+	add     r5, r5, r6
+        lfd     f1, 32(r5)      # load argument in f1
+	addi    r4, r4, 1       # increment ap->freg
+        stb     r4, 1(r3)
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+	addi    r5, r5, 15      # round r5 to a multiple of 8 and add 8
+        rlwinm  r5, r5, 0, 0, 28
+        lfd     f1, -8(r5)      # load argument in f1
+	stw     r5, 4(r3)       # update ap->stk
+        blr
+        .type   __compcert_va_float64, @function
+        .size   __compcert_va_float64, .-__compcert_va_int64
+
+        .balign 16
+        .globl __compcert_va_composite
+__compcert_va_composite:
+	b       __compcert_va_int32
+        .type   __compcert_va_composite, @function
+        .size   __compcert_va_composite, .-__compcert_va_composite
+
+# Save integer and FP registers at beginning of vararg function        
+
+        .balign 16
+        .globl  __compcert_va_saveregs
+__compcert_va_saveregs:
+        lwz     r11, 0(r1)      # r11 point to top of our frame
+        stwu    r3, -96(r11)    # register save area is 96 bytes below
+        stw     r4, 4(r11)
+        stw     r5, 8(r11)
+        stw     r6, 12(r11)
+        stw     r7, 16(r11)
+        stw     r8, 20(r11)
+        stw     r9, 24(r11)
+        stw     r10, 28(r11)
+	bf      6, 1f           # don't save FP regs if CR6 bit is clear
+        stfd    f1, 32(r11)
+        stfd    f2, 40(r11)
+        stfd    f3, 48(r11)
+        stfd    f4, 56(r11)
+        stfd    f5, 64(r11)
+        stfd    f6, 72(r11)
+        stfd    f7, 80(r11)
+        stfd    f8, 88(r11)
+1:      blr
+        .type   __compcert_va_saveregs, @function
+        .size   __compcert_va_saveregs, .-__compcert_va_saveregs
diff --git a/runtime/powerpc64/i64_dtou.s b/runtime/powerpc64/i64_dtou.s
new file mode 100644
index 00000000..e58bcfaf
--- /dev/null
+++ b/runtime/powerpc64/i64_dtou.s
@@ -0,0 +1,66 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+
+        .text
+
+### Conversion from double float to unsigned long	
+
+        .balign 16
+        .globl __compcert_i64_dtou
+__compcert_i64_dtou:
+        lis r0, 0x5f00          # 0x5f00_0000 = 2^63 in binary32 format
+        stwu r0, -16(r1)
+        lfs f2, 0(r1)           # f2 = 2^63
+        fcmpu cr0, f1, f2       # crbit 0 is f1 < f2
+        bf 0, 1f                # branch if f1 >= 2^63 (or f1 is NaN)
+	fctidz f1, f1           # convert as signed
+        stfd f1, 0(r1)
+        lwz r3, 0(r1)
+        lwz r4, 4(r1)
+        addi r1, r1, 16
+        blr
+1:      fsub f1, f1, f2         # shift argument down by 2^63
+	fctidz f1, f1           # convert as signed
+        stfd f1, 0(r1)
+        lwz r3, 0(r1)
+        lwz r4, 4(r1)
+        addis r3, r3, 0x8000    # shift result up by 2^63
+        addi r1, r1, 16
+        blr
+        .type __compcert_i64_dtou, @function
+        .size __compcert_i64_dtou, .-__compcert_i64_dtou
+
+        
diff --git a/runtime/powerpc64/i64_stof.s b/runtime/powerpc64/i64_stof.s
new file mode 100644
index 00000000..779cbc18
--- /dev/null
+++ b/runtime/powerpc64/i64_stof.s
@@ -0,0 +1,68 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+
+        .text
+
+### Conversion from signed long to single float	
+
+        .balign 16
+        .globl __compcert_i64_stof
+__compcert_i64_stof:
+        rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
+   # Check whether -2^53 <= X < 2^53	
+        sradi r5, r4, 53
+        addi r5, r5, 1
+        cmpldi r5, 2
+	blt 1f
+   # X is large enough that double rounding can occur.
+   # Avoid it by nudging X away from the points where double rounding
+   # occurs (the "round to odd" technique)
+        rldicl r5, r4, 0, 53     # extract bits 0 to 11 of X
+        addi r5, r5, 0x7FF       # r5 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r5 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-63 of r5 are 0
+        or r4, r4, r5            # correct bit number 12 of X
+        rldicr r4, r4, 0, 52     # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single
+1:      stdu r4, -16(r1)
+        lfd f1, 0(r1)
+        fcfid f1, f1
+	frsp f1, f1
+        addi r1, r1, 16
+        blr
+        .type __compcert_i64_stof, @function
+        .size __compcert_i64_stof, .-__compcert_i64_stof
+	
diff --git a/runtime/powerpc64/i64_utod.s b/runtime/powerpc64/i64_utod.s
new file mode 100644
index 00000000..491ee26b
--- /dev/null
+++ b/runtime/powerpc64/i64_utod.s
@@ -0,0 +1,79 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC 64 version.
+
+        .text
+
+### Conversion from unsigned long to double float	
+
+        .balign 16
+        .globl __compcert_i64_utod
+__compcert_i64_utod:
+	rldicl r3, r3, 0, 32    # clear top 32 bits
+	rldicl r4, r4, 0, 32    # clear top 32 bits
+	lis r5, 0x4f80          # 0x4f80_0000 = 2^32 in binary32 format
+        stdu r3, -32(r1)
+        std r4, 8(r1)
+        stw r5, 16(r1)
+        lfd f1, 0(r1)           # high 32 bits of argument
+        lfd f2, 8(r1)           # low 32 bits of argument
+	lfs f3, 16(r1)          # 2^32
+        fcfid f1, f1            # convert both 32-bit halves to FP (exactly)
+	fcfid f2, f2
+        fmadd f1, f1, f3, f2    # compute hi * 2^32 + lo
+        addi r1, r1, 32
+        blr
+        .type __compcert_i64_utod, @function
+        .size __compcert_i64_utod, .-__compcert_i64_utod
+	
+# Alternate implementation using round-to-odd:
+#       rldimi r4, r3, 32, 0   # reassemble (r3,r4) as a 64-bit integer in r4
+#       cmpdi r4, 0            # is r4 >= 2^63 ?
+#       blt 1f
+#	stdu r4, -16(r1)       # r4 < 2^63: convert as signed
+#       lfd f1, 0(r1)
+#       fcfid f1, f1
+#       addi r1, r1, 16
+#       blr
+#1:     rldicl r0, r4, 0, 63   # extract low bit of r4
+#       srdi r4, r4, 1
+#       or r4, r4, r0          # round r4 to 63 bits, using round-to-odd
+#	stdu r4, -16(r1)       # convert to binary64
+#       lfd f1, 0(r1)
+#       fcfid f1, f1
+#       fadd f1, f1, f1        # multiply result by 2
+#       addi r1, r1, 16
+#       blr
+        
\ No newline at end of file
diff --git a/runtime/powerpc64/i64_utof.s b/runtime/powerpc64/i64_utof.s
new file mode 100644
index 00000000..cdb2f867
--- /dev/null
+++ b/runtime/powerpc64/i64_utof.s
@@ -0,0 +1,64 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for 64-bit integer arithmetic.  PowerPC version.
+
+        .text
+
+### Conversion from unsigned long to single float	
+
+        .balign 16
+        .globl __compcert_i64_utof
+__compcert_i64_utof:
+	mflr r9
+   # Check whether X < 2^53	
+        andis. r0, r3, 0xFFE0       # test bits 53...63 of X
+        beq 1f
+   # X is large enough that double rounding can occur.
+   # Avoid it by nudging X away from the points where double rounding
+   # occurs (the "round to odd" technique)
+        rlwinm r0, r4, 0, 21, 31 # extract bits 0 to 11 of X
+        addi r0, r0, 0x7FF      # r0 = (X & 0x7FF) + 0x7FF
+   # bit 12 of r0 is 0 if all low 12 bits of X are 0, 1 otherwise
+   # bits 13-31 of r0 are 0
+        or r4, r4, r0           # correct bit number 12 of X
+        rlwinm r4, r4, 0, 0, 20 # set to 0 bits 0 to 11 of X
+   # Convert to double, then round to single	
+1:      bl __compcert_i64_utod
+        mtlr r9
+        frsp f1, f1
+        blr
+        .type __compcert_i64_utof, @function
+        .size __compcert_i64_utof, .-__compcert_i64_utof
+	
diff --git a/runtime/powerpc64/vararg.s b/runtime/powerpc64/vararg.s
new file mode 100644
index 00000000..8d7e62c8
--- /dev/null
+++ b/runtime/powerpc64/vararg.s
@@ -0,0 +1,163 @@
+# *****************************************************************
+#
+#               The Compcert verified compiler
+#
+#           Xavier Leroy, INRIA Paris-Rocquencourt
+#
+# Copyright (c) 2013 Institut National de Recherche en Informatique et
+#  en Automatique.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#     * Redistributions of source code must retain the above copyright
+#       notice, this list of conditions and the following disclaimer.
+#     * Redistributions in binary form must reproduce the above copyright
+#       notice, this list of conditions and the following disclaimer in the
+#       documentation and/or other materials provided with the distribution.
+#     * Neither the name of the <organization> nor the
+#       names of its contributors may be used to endorse or promote products
+#       derived from this software without specific prior written permission.
+# 
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT
+# HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# *********************************************************************
+
+# Helper functions for variadic functions <stdarg.h>.  IA32 version
+
+# typedef struct {
+#   unsigned char ireg;    // index of next integer register
+#   unsigned char freg;    // index of next FP register
+#   char * stk;            // pointer to next argument in stack
+#   struct {
+#     int iregs[8];
+#     double fregs[8];
+#   } * regs;              // pointer to saved register area
+# } va_list[1];
+#
+# unsigned int __compcert_va_int32(va_list ap);
+# unsigned long long __compcert_va_int64(va_list ap);
+# double __compcert_va_float64(va_list ap);
+
+        .text
+
+        .balign 16
+        .globl __compcert_va_int32
+__compcert_va_int32:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 0(r3)       # r4 = ap->ireg = next integer register
+        cmplwi  r4, 8
+        bge     1f
+  # Next argument was passed in an integer register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+        rlwinm  r6, r4, 2, 0, 29 # r6 = r4 * 4
+	addi    r4, r4, 1       # increment ap->ireg
+        stb     r4, 0(r3)
+        lwzx    r3, r5, r6      # load argument in r3
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+        addi    r5, r5, 4       # advance ap->stk by 4
+        stw     r5, 4(r3)
+	lwz     r3, -4(r5)      # load argument in r3
+        blr
+        .type   __compcert_va_int32, @function
+        .size   __compcert_va_int32, .-__compcert_va_int32
+
+        .balign 16
+        .globl __compcert_va_int64
+__compcert_va_int64:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 0(r3)       # r4 = ap->ireg = next integer register
+        cmplwi  r4, 7
+        bge     1f
+  # Next argument was passed in two consecutive integer register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+	addi    r4, r4, 3       # round r4 up to an even number and add 2
+        rlwinm  r4, r4, 0, 0, 30 
+        rlwinm  r6, r4, 2, 0, 29 # r6 = r4 * 4
+	add     r5, r5, r6      # r5 = address of argument + 8
+        stb     r4, 0(r3)       # update ap->ireg
+        lwz     r3, -8(r5)      # load argument in r3:r4
+        lwz     r4, -4(r5)
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+	li      r4, 8
+        stb     r4, 0(r3)       # set ap->ireg = 8 so that no ireg is left
+	addi    r5, r5, 15      # round r5 to a multiple of 8 and add 8
+        rlwinm  r5, r5, 0, 0, 28
+	stw     r5, 4(r3)       # update ap->stk
+        lwz     r3, -8(r5)      # load argument in r3:r4
+        lwz     r4, -4(r5)
+        blr
+        .type   __compcert_va_int64, @function
+        .size   __compcert_va_int64, .-__compcert_va_int64
+
+        .balign 16
+        .globl __compcert_va_float64
+__compcert_va_float64:
+	                        # r3 = ap = address of va_list structure
+        lbz     r4, 1(r3)       # r4 = ap->freg = next float register
+        cmplwi  r4, 8
+        bge     1f
+  # Next argument was passed in a FP register
+        lwz     r5, 8(r3)       # r5 = ap->regs = base of saved register area
+        rlwinm  r6, r4, 3, 0, 28 # r6 = r4 * 8
+	add     r5, r5, r6
+        lfd     f1, 32(r5)      # load argument in f1
+	addi    r4, r4, 1       # increment ap->freg
+        stb     r4, 1(r3)
+        blr
+  # Next argument was passed on stack
+1:      lwz     r5, 4(r3)       # r5 = ap->stk = next argument passed on stack
+	addi    r5, r5, 15      # round r5 to a multiple of 8 and add 8
+        rlwinm  r5, r5, 0, 0, 28
+        lfd     f1, -8(r5)      # load argument in f1
+	stw     r5, 4(r3)       # update ap->stk
+        blr
+        .type   __compcert_va_float64, @function
+        .size   __compcert_va_float64, .-__compcert_va_int64
+
+        .balign 16
+        .globl __compcert_va_composite
+__compcert_va_composite:
+	b       __compcert_va_int32
+        .type   __compcert_va_composite, @function
+        .size   __compcert_va_composite, .-__compcert_va_composite
+
+# Save integer and FP registers at beginning of vararg function        
+
+        .balign 16
+        .globl  __compcert_va_saveregs
+__compcert_va_saveregs:
+        lwz     r11, 0(r1)      # r11 point to top of our frame
+        stwu    r3, -96(r11)    # register save area is 96 bytes below
+        stw     r4, 4(r11)
+        stw     r5, 8(r11)
+        stw     r6, 12(r11)
+        stw     r7, 16(r11)
+        stw     r8, 20(r11)
+        stw     r9, 24(r11)
+        stw     r10, 28(r11)
+	bf      6, 1f           # don't save FP regs if CR6 bit is clear
+        stfd    f1, 32(r11)
+        stfd    f2, 40(r11)
+        stfd    f3, 48(r11)
+        stfd    f4, 56(r11)
+        stfd    f5, 64(r11)
+        stfd    f6, 72(r11)
+        stfd    f7, 80(r11)
+        stfd    f8, 88(r11)
+1:      blr
+        .type   __compcert_va_saveregs, @function
+        .size   __compcert_va_saveregs, .-__compcert_va_saveregs
diff --git a/x86/DuplicateOpcodeHeuristic.ml b/x86/DuplicateOpcodeHeuristic.ml
new file mode 100644
index 00000000..85505245
--- /dev/null
+++ b/x86/DuplicateOpcodeHeuristic.ml
@@ -0,0 +1,3 @@
+exception HeuristicSucceeded
+        
+let opcode_heuristic code cond ifso ifnot preferred = ()