From 866e612bf63568cbe9871bb1d6724323493651e7 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Dec 2014 09:29:48 +0100 Subject: Preserve single quotes (e.g. in CPREPRO) when generating compcert.ini --- Makefile | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/Makefile b/Makefile index 3f87287e..896a456e 100644 --- a/Makefile +++ b/Makefile @@ -222,16 +222,16 @@ latexdoc: @chmod -w $*.v compcert.ini: Makefile.config VERSION - (echo stdlib_path=$(LIBDIR); \ - echo prepro=$(CPREPRO); \ - echo asm=$(CASM); \ - echo linker=$(CLINKER); \ - echo arch=$(ARCH); \ - echo model=$(MODEL); \ - echo abi=$(ABI); \ - echo system=$(SYSTEM); \ - echo has_runtime_lib=$(HAS_RUNTIME_LIB); \ - echo asm_supports_cfi=$(ASM_SUPPORTS_CFI); \ + (echo "stdlib_path=$(LIBDIR)"; \ + echo "prepro=$(CPREPRO)"; \ + echo "asm=$(CASM)"; \ + echo "linker=$(CLINKER)"; \ + echo "arch=$(ARCH)"; \ + echo "model=$(MODEL)"; \ + echo "abi=$(ABI)"; \ + echo "system=$(SYSTEM)"; \ + echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \ + echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \ version=`cat VERSION`; \ echo version=$$version) \ > compcert.ini -- cgit From 4d1e02eb67a027d968979ed37f9d90426c634ccd Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Dec 2014 09:30:51 +0100 Subject: Prevent constant propagation on Oindirectsymbol addresses. (Otherwise they are turned into Oaddrsymbol or global addressing modes, causing linking issues on MacOS X.) --- ia32/ValueAOp.v | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) 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 -- cgit From 0342889a01aa16162232b0a87a4eb10bdb852ba4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Dec 2014 09:32:09 +0100 Subject: Update the IA32/MacOS X port. - Prefix symbols with _ - Print indirect symbol definitions - Suppress __asm() macros in system header files --- configure | 2 +- ia32/PrintAsm.ml | 10 ++++++---- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/configure b/configure index fda59dab..80cb2bcd 100755 --- a/configure +++ b/configure @@ -154,7 +154,7 @@ case "$target" in abi="standard" system="macosx" cc="${toolprefix}gcc -arch i386" - cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' -E" + cprepro="${toolprefix}gcc -arch i386 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' -E" casm="${toolprefix}gcc -arch i386 -c" case `uname -r` in [1-9].*|10.*|11.*) # up to MacOS 10.7 included 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 + -- cgit From 2fa738f7c3ea91734752bc47b14d8a461e4fd5c2 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 15 Dec 2014 16:18:05 +0100 Subject: Stdlib path is ignored when the configuration has_runtime_lib is set to false. --- driver/Configuration.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/driver/Configuration.ml b/driver/Configuration.ml index aff638e7..e73125f7 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -58,8 +58,6 @@ let get_config key = let bad_config key v = Printf.eprintf "Invalid value `%s' for configuation option `%s'\n" v key; exit 2 -let stdlib_path = get_config "stdlib_path" - let prepro = get_config "prepro" let asm = get_config "asm" let linker = get_config "linker" @@ -81,6 +79,13 @@ let has_runtime_lib = | "false" -> false | v -> bad_config "has_runtime_lib" v + +let stdlib_path = + if has_runtime_lib then + get_config "stdlib_path" + else + "" + let asm_supports_cfi = match get_config "asm_supports_cfi" with | "true" -> true -- cgit