Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

10 files changed, 148 insertions, 54 deletions

diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 70c4323c..3638c465 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -897,6 +897,55 @@ Proof.
   apply code_tail_next_int with i; auto.
 Qed.
 
+(** A variant that supports zero steps of execution *)
+
+Inductive exec_straight_opt: code -> regset -> mem -> code -> regset -> mem -> Prop :=
+  | exec_straight_opt_refl: forall c rs m,
+      exec_straight_opt c rs m c rs m
+  | exec_straight_opt_intro: forall c1 rs1 m1 c2 rs2 m2,
+      exec_straight c1 rs1 m1 c2 rs2 m2 ->
+      exec_straight_opt c1 rs1 m1 c2 rs2 m2.
+
+Lemma exec_straight_opt_left:
+  forall c3 rs3 m3 c1 rs1 m1 c2 rs2 m2,
+  exec_straight c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight_opt c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight c1 rs1 m1 c3 rs3 m3.
+Proof.
+  destruct 2; intros. auto. eapply exec_straight_trans; eauto. 
+Qed.
+
+Lemma exec_straight_opt_right:
+  forall c3 rs3 m3 c1 rs1 m1 c2 rs2 m2,
+  exec_straight_opt c1 rs1 m1 c2 rs2 m2 ->
+  exec_straight c2 rs2 m2 c3 rs3 m3 ->
+  exec_straight c1 rs1 m1 c3 rs3 m3.
+Proof.
+  destruct 1; intros. auto. eapply exec_straight_trans; eauto. 
+Qed.
+
+Lemma exec_straight_opt_step:
+  forall i c rs1 m1 rs2 m2 c' rs3 m3,
+  exec_instr ge fn i rs1 m1 = Next rs2 m2 ->
+  rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one ->
+  exec_straight_opt c rs2 m2 c' rs3 m3 ->
+  exec_straight (i :: c) rs1 m1 c' rs3 m3.
+Proof.
+  intros. inv H1. 
+- apply exec_straight_one; auto.
+- eapply exec_straight_step; eauto.
+Qed.
+
+Lemma exec_straight_opt_step_opt:
+  forall i c rs1 m1 rs2 m2 c' rs3 m3,
+  exec_instr ge fn i rs1 m1 = Next rs2 m2 ->
+  rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one ->
+  exec_straight_opt c rs2 m2 c' rs3 m3 ->
+  exec_straight_opt (i :: c) rs1 m1 c' rs3 m3.
+Proof.
+  intros. apply exec_straight_opt_intro. eapply exec_straight_opt_step; eauto.
+Qed.
+
 End STRAIGHTLINE.
 
 (** * Properties of the Mach call stack *)
diff --git a/backend/Json.ml b/backend/Json.ml
index b8f66c08..bd4d6ff9 100644
--- a/backend/Json.ml
+++ b/backend/Json.ml
@@ -10,7 +10,6 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-open Format
 open Camlcoq
 
 
@@ -18,16 +17,21 @@ open Camlcoq
 
 (* Print a string as json string *)
 let pp_jstring oc s =
-  fprintf oc "\"%s\"" s
+  output_string oc "\"";
+  output_string oc s;
+  output_string oc "\""
 
 (* Print a bool as json bool *)
-let pp_jbool oc = fprintf oc "%B"
+let pp_jbool oc b = output_string oc (string_of_bool b)
 
 (* Print an int as json int *)
-let pp_jint oc = fprintf oc "%d"
+let pp_jint oc i = output_string oc (string_of_int i)
 
 (* Print an int32 as json int *)
-let pp_jint32 oc = fprintf oc "%ld"
+let pp_jint32 oc i = output_string oc (Int32.to_string i)
+
+(* Print an int64 as json int *)
+let pp_jint64 oc i = output_string oc (Int64.to_string i)
 
 (* Print optional value *)
 let pp_jopt pp_elem oc = function
@@ -36,15 +40,19 @@ let pp_jopt pp_elem oc = function
 
 (* Print opening and closing curly braces for json dictionaries *)
 let pp_jobject_start pp =
-  fprintf pp "@[<v 1>{"
+  output_string pp "\n{"
 
 let pp_jobject_end pp =
-  fprintf pp "@;<0 -1>}@]"
+  output_string pp "}"
 
 (* Print a member of a json dictionary *)
 let pp_jmember ?(first=false) pp name pp_mem mem =
-  let sep = if first then "" else "," in
-  fprintf pp "%s@ \"%s\": %a" sep name pp_mem mem
+  if not first then output_string pp ",";
+  output_string pp " ";
+  pp_jstring pp name;
+  output_string pp " :";
+  pp_mem pp mem;
+  output_string pp "\n"
 
 (* Print singleton object *)
 let pp_jsingle_object pp name pp_mem mem =
@@ -54,29 +62,31 @@ let pp_jsingle_object pp name pp_mem mem =
 
 (* Print a list as json array *)
 let pp_jarray elem pp l =
-  match l with
-  | []  ->  fprintf pp "[]";
+  let pp_sep () = output_string pp ", " in
+  output_string pp "[";
+  begin match l with
+  | []  -> ()
   | hd::tail ->
-    fprintf pp "@[<v 1>[";
-    fprintf pp "%a" elem hd;
-    List.iter (fun l -> fprintf pp ",@ %a" elem l) tail;
-  fprintf pp "@;<0 -1>]@]"
+    elem pp hd;
+    List.iter (fun l -> pp_sep (); elem pp l) tail;
+  end;
+  output_string pp "]"
 
 (* Helper functions for printing coq integer and floats *)
 let pp_int pp i =
-  fprintf pp "%ld" (camlint_of_coqint i)
+  pp_jint32 pp (camlint_of_coqint i)
 
 let pp_int64 pp i =
-  fprintf pp "%Ld" (camlint64_of_coqint i)
+  pp_jint64 pp (camlint64_of_coqint i)
 
 let pp_float32 pp f =
-  fprintf pp "%ld" (camlint_of_coqint (Floats.Float32.to_bits f))
+  pp_jint32 pp (camlint_of_coqint (Floats.Float32.to_bits f))
 
 let pp_float64 pp f =
-  fprintf pp "%Ld" (camlint64_of_coqint (Floats.Float.to_bits f))
+  pp_jint64 pp (camlint64_of_coqint (Floats.Float.to_bits f))
 
 let pp_z pp z =
-  fprintf pp "%s" (Z.to_string z)
+  output_string pp (Z.to_string z)
 
 (* Helper functions for printing assembler constructs *)
 let pp_atom pp a =
@@ -106,4 +116,4 @@ let reset_id () =
 
 let pp_id_const pp () =
   let i = next_id () in
-  pp_jsingle_object pp "Integer" (fun pp i -> fprintf pp "%d" i) i
+  pp_jsingle_object pp "Integer" pp_jint i
diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml
index 4e57106f..8905e252 100644
--- a/backend/JsonAST.ml
+++ b/backend/JsonAST.ml
@@ -15,7 +15,6 @@ open Asm
 open AST
 open C2C
 open Json
-open Format
 open Sections
 
 
@@ -54,8 +53,8 @@ let pp_section pp sec =
   | Section_ais_annotation -> () (* There should be no info in the debug sections *)
 
 let pp_int_opt pp = function
-  | None -> fprintf pp "0"
-  | Some i -> fprintf pp "%d" i
+  | None -> output_string pp "0"
+  | Some i -> pp_jint pp i
 
 let pp_fundef pp_inst pp (name,fn) =
   let alignment = atom_alignof name
@@ -119,9 +118,8 @@ let pp_program pp pp_inst prog =
   pp_jobject_end pp
 
 let pp_mnemonics pp mnemonic_names =
-  let mnemonic_names = List.sort (String.compare) mnemonic_names in
-  let new_line pp () = pp_print_string pp "\n" in
-  pp_print_list ~pp_sep:new_line pp_print_string pp mnemonic_names
+  let new_line pp () = Format.pp_print_string pp "\n" in
+  Format.pp_print_list ~pp_sep:new_line Format.pp_print_string pp mnemonic_names
 
 let jdump_magic_number = "CompCertJDUMPRelease: " ^ Version.version
 
@@ -153,4 +151,4 @@ let pp_ast pp pp_inst ast sourcename =
     pp_jmember pp "Compilation Unit" pp_jstring sourcename;
     pp_jmember pp "Asm Ast" (fun pp prog -> pp_program pp pp_inst prog) ast;
     pp_jobject_end pp;
-    Format.pp_print_flush pp ()
+    flush pp
diff --git a/backend/JsonAST.mli b/backend/JsonAST.mli
index 7afdce51..c32439e4 100644
--- a/backend/JsonAST.mli
+++ b/backend/JsonAST.mli
@@ -13,4 +13,4 @@
 
 
 val pp_mnemonics : Format.formatter -> string list -> unit
-val pp_ast : Format.formatter -> (Format.formatter  -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program  -> string -> unit
+val pp_ast : out_channel -> (out_channel  -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program  -> string -> unit
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 1fe23a9d..0e3b7c8e 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -321,11 +321,11 @@ Local Opaque mreg_type.
   + (* other ops *)
     destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
     econstructor; eauto.
-    apply wt_setreg; auto; try (apply wt_undef_regs; auto).
-    eapply Val.has_subtype; eauto.
+    apply wt_setreg. eapply Val.has_subtype; eauto.
     change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
     red; intros; subst op. simpl in ISMOVE.
-    destruct args; try discriminate. destruct args; discriminate. 
+    destruct args; try discriminate. destruct args; discriminate.
+    apply wt_undef_regs; auto.
 - (* load *)
   simpl in *; InvBooleans.
   econstructor; eauto.
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index b35c90b2..3c2d8e20 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -594,7 +594,8 @@ Proof.
 Qed.
 
 (** Modular arithmetic operations: add, mul, opposite.
-    (But not subtraction because of the pointer - pointer case. *)
+    Also subtraction, but only on 64-bit targets, otherwise
+    the pointer - pointer case does not fit. *)
 
 Definition modarith (x: nval) :=
   match x with
@@ -615,6 +616,19 @@ Proof.
 - inv H; auto. inv H0; auto. destruct w1; auto.
 Qed.
 
+Lemma sub_sound:
+  forall v1 w1 v2 w2 x,
+  vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
+  Archi.ptr64 = true ->
+  vagree (Val.sub v1 v2) (Val.sub w1 w2) x.
+Proof.
+  unfold modarith; intros. destruct x; simpl in *.
+- auto.
+- unfold Val.sub; rewrite H1; InvAgree.
+  apply eqmod_iagree. apply eqmod_sub; apply iagree_eqmod; auto.
+- inv H; auto. inv H0; auto. destruct w1; auto.
+Qed.
+
 Remark modarith_idem: forall nv, modarith (modarith nv) = modarith nv.
 Proof.
   destruct nv; simpl; auto. f_equal; apply complete_mask_idem.
@@ -680,7 +694,7 @@ Definition sign_ext (n: Z) (x: nval) :=
 Lemma sign_ext_sound:
   forall v w x n,
   vagree v w (sign_ext n x) ->
-  0 < n < Int.zwordsize ->
+  0 < n ->
   vagree (Val.sign_ext n v) (Val.sign_ext n w) x.
 Proof.
   unfold sign_ext; intros. destruct x; simpl in *.
@@ -889,7 +903,8 @@ Lemma default_needs_of_operation_sound:
   eval_operation ge (Vptr sp Ptrofs.zero) op args1 m1 = Some v1 ->
   vagree_list args1 args2 nil
   \/ vagree_list args1 args2 (default nv :: nil)
-  \/ vagree_list args1 args2 (default nv :: default nv :: nil) ->
+  \/ vagree_list args1 args2 (default nv :: default nv :: nil)
+  \/ vagree_list args1 args2 (default nv :: default nv :: default nv :: nil) ->
   nv <> Nothing ->
   exists v2,
      eval_operation ge (Vptr sp Ptrofs.zero) op args2 m2 = Some v2
@@ -901,7 +916,8 @@ Proof.
   {
     destruct H0. auto with na.
     destruct H0. inv H0; constructor; auto with na.
-    inv H0; constructor; auto with na. inv H8; constructor; auto with na.
+    destruct H0. inv H0. constructor. inv H8; constructor; auto with na. 
+    inv H0; constructor; auto with na. inv H8; constructor; auto with na. inv H9; constructor; auto with na.
   }
   exploit (@eval_operation_inj _ _ _ _ ge ge inject_id).
   eassumption. auto. auto. auto.
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index a8ee8453..1873da4d 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -764,8 +764,8 @@ Lemma eval_divlu_mull:
 Proof.
   intros. unfold divlu_mull. exploit (divlu_mul_shift x); eauto. intros [A B].
   assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)) by (constructor; auto).
-  exploit eval_mullhu. eauto. eexact A0. instantiate (1 := Int64.repr M). intros (v1 & A1 & B1).
-  exploit eval_shrluimm. eauto. eexact A1. instantiate (1 := Int.repr p). intros (v2 & A2 & B2).
+  exploit eval_mullhu. try apply HELPERS. eexact A0. instantiate (1 := Int64.repr M). intros (v1 & A1 & B1).
+  exploit eval_shrluimm. try apply HELPERS. eexact A1. instantiate (1 := Int.repr p). intros (v2 & A2 & B2).
   simpl in B1; inv B1. simpl in B2. replace (Int.ltu (Int.repr p) Int64.iwordsize') with true in B2. inv B2.
   rewrite B. assumption.
   unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto.
@@ -835,17 +835,17 @@ Proof.
   intros. unfold divls_mull.
   assert (A0: eval_expr ge sp e m le (Eletvar O) (Vlong x)).
   { constructor; auto. }
-  exploit eval_mullhs. eauto. eexact A0. instantiate (1 := Int64.repr M).  intros (v1 & A1 & B1).
-  exploit eval_addl; auto; try apply HELPERS. eexact A1. eexact A0. intros (v2 & A2 & B2).
-  exploit eval_shrluimm. eauto. eexact A0. instantiate (1 := Int.repr 63). intros (v3 & A3 & B3).
+  exploit eval_mullhs. try apply HELPERS. eexact A0. instantiate (1 := Int64.repr M).  intros (v1 & A1 & B1).
+  exploit eval_addl. auto. eexact A1. eexact A0. intros (v2 & A2 & B2).
+  exploit eval_shrluimm. try apply HELPERS. eexact A0. instantiate (1 := Int.repr 63). intros (v3 & A3 & B3).
   set (a4 := if zlt M Int64.half_modulus
              then mullhs (Eletvar 0) (Int64.repr M)
              else addl (mullhs (Eletvar 0) (Int64.repr M)) (Eletvar 0)).
   set (v4 := if zlt M Int64.half_modulus then v1 else v2).
   assert (A4: eval_expr ge sp e m le a4 v4).
   { unfold a4, v4; destruct (zlt M Int64.half_modulus); auto. }
-  exploit eval_shrlimm. eauto. eexact A4. instantiate (1 := Int.repr p). intros (v5 & A5 & B5).
-  exploit eval_addl; auto; try apply HELPERS. eexact A5. eexact A3. intros (v6 & A6 & B6).
+  exploit eval_shrlimm. try apply HELPERS. eexact A4. instantiate (1 := Int.repr p). intros (v5 & A5 & B5).
+  exploit eval_addl. auto. eexact A5. eexact A3. intros (v6 & A6 & B6).
   assert (RANGE: forall x, 0 <= x < 64 -> Int.ltu (Int.repr x) Int64.iwordsize' = true).
   { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto.
     assert (64 < Int.max_unsigned) by (compute; auto). omega. }
@@ -949,8 +949,7 @@ Proof.
   intros until y. unfold divf. destruct (divf_match b); intros.
 - unfold divfimm. destruct (Float.exact_inverse n2) as [n2' | ] eqn:EINV.
   + inv H0. inv H4. simpl in H6. inv H6. econstructor; split.
-    EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
-    simpl; eauto.
+    repeat (econstructor; eauto). 
     destruct x; simpl; auto. erewrite Float.div_mul_inverse; eauto.
   + apply eval_divf_base; trivial.
 - apply eval_divf_base; trivial.
@@ -965,8 +964,7 @@ Proof.
   intros until y. unfold divfs. destruct (divfs_match b); intros.
 - unfold divfsimm. destruct (Float32.exact_inverse n2) as [n2' | ] eqn:EINV.
   + inv H0. inv H4. simpl in H6. inv H6. econstructor; split.
-    EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
-    simpl; eauto.
+    repeat (econstructor; eauto). 
     destruct x; simpl; auto. erewrite Float32.div_mul_inverse; eauto.
   + apply eval_divfs_base; trivial.
 - apply eval_divfs_base; trivial.
diff --git a/backend/Selectionaux.ml b/backend/Selectionaux.ml
index 574c31f0..26a79fd7 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -68,6 +68,8 @@ let rec cost_expr = function
 
 let fast_cmove ty =
   match Configuration.arch, Configuration.model with
+  | "aarch64", _ ->
+      (match ty with Tint | Tlong | Tfloat | Tsingle -> true | _ -> false)
   | "arm", _ ->
       (match ty with Tint | Tfloat | Tsingle -> true | _ -> false)
   | "powerpc", "e5500" -> 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 8a827af2..aa53c9cb 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -1258,8 +1258,8 @@ Proof.
   econstructor; eauto.
   econstructor; eauto. apply set_var_lessdef; auto.
 - (* store *)
-  exploit sel_expr_correct. eauto. eauto. eexact H. eauto. eauto. intros [vaddr' [A B]].
-  exploit sel_expr_correct. eauto. eauto. eexact H0. eauto. eauto. intros [v' [C D]].
+  exploit sel_expr_correct. try apply LINK. try apply HF. eexact H. eauto. eauto. intros [vaddr' [A B]].
+  exploit sel_expr_correct. try apply LINK. try apply HF. eexact H0. eauto. eauto. intros [v' [C D]].
   exploit Mem.storev_extends; eauto. intros [m2' [P Q]].
   left; econstructor; split.
   eapply eval_store; eauto.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index fd3bd5ae..c132ce7c 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -2093,6 +2093,7 @@ Proof.
 Qed.
 
 Definition sign_ext (nbits: Z) (v: aval) :=
+  if zle nbits 0 then Uns (provenance v) 0 else
   match v with
   | I i => I (Int.sign_ext nbits i)
   | Uns p n => if zlt n nbits then Uns p n else sgn p nbits
@@ -2101,20 +2102,39 @@ Definition sign_ext (nbits: Z) (v: aval) :=
   end.
 
 Lemma sign_ext_sound:
-  forall nbits v x, 0 < nbits -> vmatch v x -> vmatch (Val.sign_ext nbits v) (sign_ext nbits x).
+  forall nbits v x, vmatch v x -> vmatch (Val.sign_ext nbits v) (sign_ext nbits x).
 Proof.
   assert (DFL: forall p nbits i, 0 < nbits -> vmatch (Vint (Int.sign_ext nbits i)) (sgn p nbits)).
   {
     intros. apply vmatch_sgn. apply is_sign_ext_sgn; auto with va.
   }
-  intros. inv H0; simpl; auto with va.
-- destruct (zlt n nbits); eauto with va.
+  intros. unfold sign_ext. destruct (zle nbits 0).
+- destruct v; simpl; auto with va. constructor. omega. 
+  rewrite Int.sign_ext_below by auto. red; intros; apply Int.bits_zero.
+- inv H; simpl; auto with va.
++ destruct (zlt n nbits); eauto with va.
   constructor; auto. eapply is_sign_ext_uns; eauto with va.
-- destruct (zlt n nbits); auto with va.
-- apply vmatch_sgn. apply is_sign_ext_sgn; auto with va.
++ destruct (zlt n nbits); auto with va.
++ apply vmatch_sgn. apply is_sign_ext_sgn; auto with va.
   apply Z.min_case; auto with va.
 Qed.
 
+Definition zero_ext_l (s: Z) := unop_long (Int64.zero_ext s).
+
+Lemma zero_ext_l_sound:
+  forall s v x, vmatch v x -> vmatch (Val.zero_ext_l s v) (zero_ext_l s x).
+Proof.
+  intros s. exact (unop_long_sound (Int64.zero_ext s)).
+Qed.
+
+Definition sign_ext_l (s: Z) := unop_long (Int64.sign_ext s).
+
+Lemma sign_ext_l_sound:
+  forall s v x, vmatch v x -> vmatch (Val.sign_ext_l s v) (sign_ext_l s x).
+Proof.
+  intros s. exact (unop_long_sound (Int64.sign_ext s)).
+Qed.
+
 Definition longofint (v: aval) :=
   match v with
   | I i => L (Int64.repr (Int.signed i))
@@ -4712,6 +4732,7 @@ Hint Resolve cnot_sound symbol_address_sound
        negfs_sound absfs_sound
        addfs_sound subfs_sound mulfs_sound divfs_sound
        zero_ext_sound sign_ext_sound longofint_sound longofintu_sound
+       zero_ext_l_sound sign_ext_l_sound
        singleoffloat_sound floatofsingle_sound
        intoffloat_sound intuoffloat_sound floatofint_sound floatofintu_sound
        intofsingle_sound intuofsingle_sound singleofint_sound singleofintu_sound