diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-11 10:14:09 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-12-11 10:14:09 +0100 |
| commit | 089a9c8d0eb0b44a12d4008739b7c1cbc9dccd14 (patch) | |
| tree | 8b83547ac65690b9a7cae230a9d6195766095577 /ia32 | |
| parent | b1345b1d0efec39850fb91dcc7e12d341b1a24fd (diff) | |
| parent | 0342889a01aa16162232b0a87a4eb10bdb852ba4 (diff) | |
| download | compcert-089a9c8d0eb0b44a12d4008739b7c1cbc9dccd14.tar.gz compcert-089a9c8d0eb0b44a12d4008739b7c1cbc9dccd14.zip | |
Merge branch 'master' into dwarf
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/PrintAsm.ml | 10 | ||||
| -rw-r--r-- | ia32/ValueAOp.v | 13 |
2 files changed, 17 insertions, 6 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 5c84af6b..41002bac 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -161,7 +161,7 @@ module MacOS_System = fprintf oc "_%s" s let symbol oc symb = - fprintf oc "%s" (extern_atom symb) + fprintf oc "_%s" (extern_atom symb) let label oc lbl = fprintf oc "L%d" lbl @@ -206,7 +206,8 @@ module MacOS_System = fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s; fprintf oc " .indirect_symbol %a\n" raw_symbol s; fprintf oc " .long 0\n") - !indirect_symbols + !indirect_symbols; + indirect_symbols := StringSet.empty end:SYSTEM) @@ -638,7 +639,6 @@ let print_builtin_inline oc name args res = let float64_literals : (int * int64) list ref = ref [] let float32_literals : (int * int32) list ref = ref [] let jumptables : (int * label list) list ref = ref [] -let indirect_symbols : StringSet.t ref = ref StringSet.empty (* Reminder on AT&T syntax: op source, dest *) @@ -1042,4 +1042,6 @@ let print_program oc p = Target.raw_symbol "__negs_mask"; fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" Target.raw_symbol "__abss_mask" - end + end; + Target.print_epilogue oc + diff --git a/ia32/ValueAOp.v b/ia32/ValueAOp.v index 874c2be3..53013337 100644 --- a/ia32/ValueAOp.v +++ b/ia32/ValueAOp.v @@ -58,7 +58,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ointconst n, nil => I n | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop - | Oindirectsymbol id, nil => Ptr (Gl id Int.zero) + | Oindirectsymbol id, nil => Ifptr (Gl id Int.zero) | Ocast8signed, v1 :: nil => sign_ext 8 v1 | Ocast8unsigned, v1 :: nil => zero_ext 8 v1 | Ocast16signed, v1 :: nil => sign_ext 16 v1 @@ -145,7 +145,16 @@ Proof. intros; apply symbol_address_sound; apply GENV. Qed. -Hint Resolve symbol_address_sound: va. +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 |