Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 -> x86/x86_32/x86_64

Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.

This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true).  Unlike previous approaches, no other file is duplicated between these two variants of x86.

While we are at it, I renamed "ia32" into "x86" everywhere.  "ia32" is Intel speak for the 32-bit architecture.  It is not a good name to describe both the 32 and 64 bit architectures.

Finally, .depend is no longer under version control and is regenerated when the target architecture changes.  That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).

1 files changed, 264 insertions, 0 deletions

diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v
new file mode 100644
index 00000000..1021a9c8
--- /dev/null
+++ b/x86/ValueAOp.v
@@ -0,0 +1,264 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*                Xavier Leroy, INRIA Paris                            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Coqlib Compopts.
+Require Import AST Integers Floats Values Memory Globalenvs.
+Require Import Op RTL ValueDomain.
+
+(** Value analysis for x86_64 operators *)
+
+Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
+  match cond, vl with
+  | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2
+  | Ccompu c, v1 :: v2 :: nil => cmpu_bool c v1 v2
+  | Ccompimm c n, v1 :: nil => cmp_bool c v1 (I n)
+  | Ccompuimm c n, v1 :: nil => cmpu_bool c v1 (I n)
+  | Ccompl c, v1 :: v2 :: nil => cmpl_bool c v1 v2
+  | Ccomplu c, v1 :: v2 :: nil => cmplu_bool c v1 v2
+  | Ccomplimm c n, v1 :: nil => cmpl_bool c v1 (L n)
+  | Ccompluimm c n, v1 :: nil => cmplu_bool c v1 (L n)
+  | Ccompf c, v1 :: v2 :: nil => cmpf_bool c v1 v2
+  | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2)
+  | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2
+  | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2)
+  | Cmaskzero n, v1 :: nil => maskzero v1 n
+  | Cmasknotzero n, v1 :: nil => cnot (maskzero v1 n)
+  | _, _ => Bnone
+  end.
+
+Definition eval_static_addressing_32 (addr: addressing) (vl: list aval): aval :=
+  match addr, vl with
+  | Aindexed n, v1::nil => add v1 (I (Int.repr n))
+  | Aindexed2 n, v1::v2::nil => add (add v1 v2) (I (Int.repr n))
+  | Ascaled sc ofs, v1::nil => add (mul v1 (I (Int.repr sc))) (I (Int.repr ofs))
+  | Aindexed2scaled sc ofs, v1::v2::nil => add v1 (add (mul v2 (I (Int.repr sc))) (I (Int.repr ofs)))
+  | Aglobal s ofs, nil => Ptr (Gl s ofs)
+  | Abased s ofs, v1::nil => add (Ptr (Gl s ofs)) v1
+  | Abasedscaled sc s ofs, v1::nil => add (Ptr (Gl s ofs)) (mul v1 (I (Int.repr sc)))
+  | Ainstack ofs, nil => Ptr(Stk ofs)
+  | _, _ => Vbot
+  end.
+
+Definition eval_static_addressing_64 (addr: addressing) (vl: list aval): aval :=
+  match addr, vl with
+  | Aindexed n, v1::nil => addl v1 (L (Int64.repr n))
+  | Aindexed2 n, v1::v2::nil => addl (addl v1 v2) (L (Int64.repr n))
+  | Ascaled sc ofs, v1::nil => addl (mull v1 (L (Int64.repr sc))) (L (Int64.repr ofs))
+  | Aindexed2scaled sc ofs, v1::v2::nil => addl v1 (addl (mull v2 (L (Int64.repr sc))) (L (Int64.repr ofs)))
+  | Aglobal s ofs, nil => Ptr (Gl s ofs)
+  | Abased s ofs, v1::nil => addl (Ptr (Gl s ofs)) v1
+  | Abasedscaled sc s ofs, v1::nil => addl (Ptr (Gl s ofs)) (mull v1 (L (Int64.repr sc)))
+  | Ainstack ofs, nil => Ptr(Stk ofs)
+  | _, _ => Vbot
+  end.
+
+Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
+  if Archi.ptr64
+  then eval_static_addressing_64 addr vl
+  else eval_static_addressing_32 addr vl.
+
+Definition eval_static_operation (op: operation) (vl: list aval): aval :=
+  match op, vl with
+  | Omove, v1::nil => v1
+  | Ointconst n, nil => I n
+  | Olongconst n, nil => L n
+  | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop
+  | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop
+  | Oindirectsymbol id, nil => Ifptr (Gl id Ptrofs.zero)
+  | Ocast8signed, v1 :: nil => sign_ext 8 v1
+  | Ocast8unsigned, v1 :: nil => zero_ext 8 v1
+  | Ocast16signed, v1 :: nil => sign_ext 16 v1
+  | Ocast16unsigned, v1 :: nil => zero_ext 16 v1
+  | Oneg, v1::nil => neg v1
+  | Osub, v1::v2::nil => sub v1 v2
+  | Omul, v1::v2::nil => mul v1 v2
+  | Omulimm n, v1::nil => mul v1 (I n)
+  | Omulhs, v1::v2::nil => mulhs v1 v2
+  | Omulhu, v1::v2::nil => mulhu v1 v2
+  | Odiv, v1::v2::nil => divs v1 v2
+  | Odivu, v1::v2::nil => divu v1 v2
+  | Omod, v1::v2::nil => mods v1 v2
+  | Omodu, v1::v2::nil => modu v1 v2
+  | Oand, v1::v2::nil => and v1 v2
+  | Oandimm n, v1::nil => and v1 (I n)
+  | Oor, v1::v2::nil => or v1 v2
+  | Oorimm n, v1::nil => or v1 (I n)
+  | Oxor, v1::v2::nil => xor v1 v2
+  | Oxorimm n, v1::nil => xor v1 (I n)
+  | Onot, v1::nil => notint v1
+  | Oshl, v1::v2::nil => shl v1 v2
+  | Oshlimm n, v1::nil => shl v1 (I n)
+  | Oshr, v1::v2::nil => shr v1 v2
+  | Oshrimm n, v1::nil => shr v1 (I n)
+  | Oshrximm n, v1::nil => shrx v1 (I n)
+  | Oshru, v1::v2::nil => shru v1 v2
+  | Oshruimm n, v1::nil => shru v1 (I n)
+  | Ororimm n, v1::nil => ror v1 (I n)
+  | Oshldimm n, v1::v2::nil => or (shl v1 (I n)) (shru v2 (I (Int.sub Int.iwordsize n)))
+  | Olea addr, _ => eval_static_addressing_32 addr vl
+  | Omakelong, v1::v2::nil => longofwords v1 v2
+  | Olowlong, v1::nil => loword v1
+  | Ohighlong, v1::nil => hiword v1
+  | Ocast32signed, v1::nil => longofint v1
+  | Ocast32unsigned, v1::nil => longofintu v1
+  | Onegl, v1::nil => negl v1
+  | Oaddlimm n, v1::nil => addl v1 (L n)
+  | Osubl, v1::v2::nil => subl v1 v2
+  | Omull, v1::v2::nil => mull v1 v2
+  | Omullimm n, v1::nil => mull v1 (L n)
+  | Omullhs, v1::v2::nil => mullhs v1 v2
+  | Omullhu, v1::v2::nil => mullhu v1 v2
+  | Odivl, v1::v2::nil => divls v1 v2
+  | Odivlu, v1::v2::nil => divlu v1 v2
+  | Omodl, v1::v2::nil => modls v1 v2
+  | Omodlu, v1::v2::nil => modlu v1 v2
+  | Oandl, v1::v2::nil => andl v1 v2
+  | Oandlimm n, v1::nil => andl v1 (L n)
+  | Oorl, v1::v2::nil => orl v1 v2
+  | Oorlimm n, v1::nil => orl v1 (L n)
+  | Oxorl, v1::v2::nil => xorl v1 v2
+  | Oxorlimm n, v1::nil => xorl v1 (L n)
+  | Onotl, v1::nil => notl v1
+  | Oshll, v1::v2::nil => shll v1 v2
+  | Oshllimm n, v1::nil => shll v1 (I n)
+  | Oshrl, v1::v2::nil => shrl v1 v2
+  | Oshrlimm n, v1::nil => shrl v1 (I n)
+  | Oshrxlimm n, v1::nil => shrxl v1 (I n)
+  | Oshrlu, v1::v2::nil => shrlu v1 v2
+  | Oshrluimm n, v1::nil => shrlu v1 (I n)
+  | Ororlimm n, v1::nil => rorl v1 (I n)
+  | Oleal addr, _ => eval_static_addressing_64 addr vl
+  | Onegf, v1::nil => negf v1
+  | Oabsf, v1::nil => absf v1
+  | Oaddf, v1::v2::nil => addf v1 v2
+  | Osubf, v1::v2::nil => subf v1 v2
+  | Omulf, v1::v2::nil => mulf v1 v2
+  | Odivf, v1::v2::nil => divf v1 v2
+  | Onegfs, v1::nil => negfs v1
+  | Oabsfs, v1::nil => absfs v1
+  | Oaddfs, v1::v2::nil => addfs v1 v2
+  | Osubfs, v1::v2::nil => subfs v1 v2
+  | Omulfs, v1::v2::nil => mulfs v1 v2
+  | Odivfs, v1::v2::nil => divfs v1 v2
+  | Osingleoffloat, v1::nil => singleoffloat v1
+  | Ofloatofsingle, v1::nil => floatofsingle v1
+  | Ointoffloat, v1::nil => intoffloat v1
+  | Ofloatofint, v1::nil => floatofint v1
+  | Ointofsingle, v1::nil => intofsingle v1
+  | Osingleofint, v1::nil => singleofint v1
+  | Olongoffloat, v1::nil => longoffloat v1
+  | Ofloatoflong, v1::nil => floatoflong v1
+  | Olongofsingle, v1::nil => longofsingle v1
+  | Osingleoflong, v1::nil => singleoflong v1
+  | Ocmp c, _ => of_optbool (eval_static_condition c vl)
+  | _, _ => Vbot
+  end.
+
+Section SOUNDNESS.
+
+Variable bc: block_classification.
+Variable ge: genv.
+Hypothesis GENV: genv_match bc ge.
+Variable sp: block.
+Hypothesis STACK: bc sp = BCstack.
+
+Theorem eval_static_condition_sound:
+  forall cond vargs m aargs,
+  list_forall2 (vmatch bc) vargs aargs ->
+  cmatch (eval_condition cond vargs m) (eval_static_condition cond aargs).
+Proof.
+  intros until aargs; intros VM. inv VM.
+  destruct cond; auto with va.
+  inv H0.
+  destruct cond; simpl; eauto with va.
+  inv H2.
+  destruct cond; simpl; eauto with va.
+  destruct cond; auto with va.
+Qed.
+
+Lemma symbol_address_sound:
+  forall id ofs,
+  vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)).
+Proof.
+  intros; apply symbol_address_sound; apply GENV.
+Qed.
+
+Lemma symbol_address_sound_2:
+  forall id ofs,
+  vmatch bc (Genv.symbol_address ge id ofs) (Ifptr (Gl id ofs)).
+Proof.
+  intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) as [b|] eqn:F.
+  constructor. constructor. apply GENV; auto.
+  constructor.
+Qed.
+
+Hint Resolve symbol_address_sound symbol_address_sound_2: va.
+
+Ltac InvHyps :=
+  match goal with
+  | [H: None = Some _ |- _ ] => discriminate
+  | [H: Some _ = Some _ |- _] => inv H
+  | [H1: match ?vl with nil => _ | _ :: _ => _ end = Some _ ,
+     H2: list_forall2 _ ?vl _ |- _ ] => inv H2; InvHyps
+  | [H: (if Archi.ptr64 then _ else _) = Some _ |- _] => destruct Archi.ptr64 eqn:?; InvHyps
+  | _ => idtac
+  end.
+
+Theorem eval_static_addressing_32_sound:
+  forall addr vargs vres aargs,
+  eval_addressing32 ge (Vptr sp Ptrofs.zero) addr vargs = Some vres ->
+  list_forall2 (vmatch bc) vargs aargs ->
+  vmatch bc vres (eval_static_addressing_32 addr aargs).
+Proof.
+  unfold eval_addressing32, eval_static_addressing_32; intros;
+  destruct addr; InvHyps; eauto with va.
+  rewrite Ptrofs.add_zero_l; eauto with va.
+Qed.
+
+Theorem eval_static_addressing_64_sound:
+  forall addr vargs vres aargs,
+  eval_addressing64 ge (Vptr sp Ptrofs.zero) addr vargs = Some vres ->
+  list_forall2 (vmatch bc) vargs aargs ->
+  vmatch bc vres (eval_static_addressing_64 addr aargs).
+Proof.
+  unfold eval_addressing64, eval_static_addressing_64; intros;
+  destruct addr; InvHyps; eauto with va.
+  rewrite Ptrofs.add_zero_l; eauto with va.
+Qed.
+
+Theorem eval_static_addressing_sound:
+  forall addr vargs vres aargs,
+  eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = Some vres ->
+  list_forall2 (vmatch bc) vargs aargs ->
+  vmatch bc vres (eval_static_addressing addr aargs).
+Proof.
+  unfold eval_addressing, eval_static_addressing; intros.
+  destruct Archi.ptr64; eauto using eval_static_addressing_32_sound, eval_static_addressing_64_sound.
+Qed.
+
+Theorem eval_static_operation_sound:
+  forall op vargs m vres aargs,
+  eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
+  list_forall2 (vmatch bc) vargs aargs ->
+  vmatch bc vres (eval_static_operation op aargs).
+Proof.
+  unfold eval_operation, eval_static_operation; intros;
+  destruct op; InvHyps; eauto with va.
+  destruct (propagate_float_constants tt); constructor.
+  destruct (propagate_float_constants tt); constructor.
+  eapply eval_static_addressing_32_sound; eauto.
+  eapply eval_static_addressing_64_sound; eauto.
+  apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+Qed.
+
+End SOUNDNESS.
+