From e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:25:18 +0200 Subject: Support for 64-bit architectures: generic support - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly. --- driver/Configuration.ml | 2 +- driver/Ctydescr.ml | 456 ++++++++++++++++++++++++++++++++++++++++++++++++ driver/Driver.ml | 9 +- 3 files changed, 463 insertions(+), 4 deletions(-) create mode 100644 driver/Ctydescr.ml (limited to 'driver') diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 87e29e0f..85a163bf 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -117,7 +117,7 @@ let linker = let arch = match get_config_string "arch" with - | "powerpc"|"arm"|"ia32" as a -> a + | "powerpc"|"arm"|"ia32"|"x86_64"|"x86" as a -> a | v -> bad_config "arch" [v] let model = get_config_string "model" let abi = get_config_string "abi" diff --git a/driver/Ctydescr.ml b/driver/Ctydescr.ml new file mode 100644 index 00000000..8091257b --- /dev/null +++ b/driver/Ctydescr.ml @@ -0,0 +1,456 @@ +open Printf +open Camlcoq +open Tydesc + +let check ty x = TyIO.check x ty; true + +(* From stdlib *) + +let list t = List t +let pair t1 t2 = Tuple [t1;t2] + +let rec repr_nat = Sum("nat", [ + "O", []; + "S", [repr_nat] +]) + +let nat = Base { + base_name = "nat"; + base_check = check repr_nat; + base_parse = (fun synt s -> assert false); + base_print = (fun synt x -> + let s = string_of_int (Nat.to_int x) in + match synt with + | `Coq -> s ^ "%nat" + | _ -> s) +} + +let rec repr_positive = Sum("positive", [ + "xI", [repr_positive]; + "xO", [repr_positive]; + "xH", [] +]) + +let positive = Base { + base_name = "positive"; + base_check = check repr_positive; + base_parse = (fun synt s -> assert false); + base_print = (fun synt x -> Z.to_string (Z.Zpos x)) +} + +let repr_N = Sum("N", [ + "N0", []; + "Npos", [repr_positive] +]) + +let _N = Base { + base_name = "N"; + base_check = check repr_N; + base_parse = (fun synt s -> assert false); + base_print = (fun synt x -> + let y = match x with N.N0 -> Z.Z0 | N.Npos p -> Z.Zpos p in + let s = Z.to_string y in + match synt with + | `Coq -> s ^ "%N" + | _ -> s) +} + +let repr_Z = Sum("Z", [ + "Z0", []; + "Zpos", [repr_positive]; + "Zneg", [repr_positive] +]) + +let _Z = Base { + base_name = "Z"; + base_check = check repr_Z; + base_parse = (fun synt s -> assert false); + base_print = (fun synt x -> + let s = Z.to_string x in + match synt with + | `Coq -> s ^ "%Z" + | _ -> s) +} + +(* From Integers *) + +let int = Base { + base_name = "int"; + base_check = check repr_Z; + base_parse = (fun synt s -> + let (n, s') = get_number s in + try (coqint_of_camlint (Int32.of_string n), s') + with Failure _ -> + raise (Parsing_failure(get_position s, sprintf "bad 'int' literal %S" n))); + base_print = (fun synt x -> + let s = Z.to_string x in + match synt with + | `Coq -> "(mkint " ^ s ^ "%Z)" + | _ -> s) +} + +let int64 = Base { + base_name = "int64"; + base_check = check repr_Z; + base_parse = (fun synt s -> + let (n, s') = get_number s in + try (coqint_of_camlint64 (Int64.of_string n), s') + with Failure _ -> + raise (Parsing_failure(get_position s, sprintf "bad 'int64' literal %S" n))); + base_print = (fun synt x -> + let s = Z.to_string x in + match synt with + | `Coq -> "(mkint64 " ^ s ^ "%Z)" + | _ -> s) +} + +(* From Floats *) + +let nan_pl = positive + +let binary_float = Sum("binary_float", [ + "B754_zero", [bool]; + "B754_infinity", [bool]; + "B754_nan", [bool; nan_pl]; + "B754_finite", [bool; positive; _Z] +]) + +let float = Base { + base_name = "float"; + base_check = check binary_float; + base_parse = (fun synt s -> + let (n, s') = get_number s in + try (Floats.Float.of_bits (coqint_of_camlint64 (Int64.of_string n)), s') + with Failure _ -> + raise (Parsing_failure(get_position s, sprintf "bad 'float' literal %S" n))); + base_print = (fun synt x -> + let s = Z.to_string (Floats.Float.to_bits x) in + match synt with + | `Coq -> "(mkfloat " ^ s ^ "%Z)" + | _ -> s) +} + +let float32 = Base { + base_name = "float32"; + base_check = check binary_float; + base_parse = (fun synt s -> + let (n, s') = get_number s in + try (Floats.Float32.of_bits (coqint_of_camlint (Int32.of_string n)), s') + with Failure _ -> + raise (Parsing_failure(get_position s, sprintf "bad 'float32' literal %S" n))); + base_print = (fun synt x -> + let s = Z.to_string (Floats.Float.to_bits x) in + match synt with + | `Coq -> "(mkfloat32 " ^ s ^ "%Z)" + | _ -> s) +} + +(* From Maps *) + +let ptree a = + let rec t = Sum(sprintf "PTree.t[%s]" (describe_ty a), [ + "Leaf", []; + "Node", [t; option a; t] + ]) in t + +(* From AST *) + +let ident = positive + +let typ = Sum("typ", [ + "AST.Tint", []; + "AST.Tfloat", []; + "AST.Tlong", []; + "AST.Tsingle", []; + "AST.Tany32", []; + "AST.Tany64", []; +]) + +let calling_convention = Record("calling_convention", [ + "cc_vararg", bool; + "cc_structret", bool; +]) + +let default_calling_convention = { + dfl_val = AST.cc_default; + dfl_print = (function `Coq -> Some "cc_default" | _ -> None) +} + +let calling_convention_d = + Default(calling_convention, default_calling_convention) + +let signature = Record("signature", [ + "sig_args", list typ; + "sig_res", option typ; + "sig_cc", calling_convention_d; +]) + +let memory_chunk = Sum("memory_chunk", [ + "Mint8signed", []; + "Mint8unsigned", []; + "Mint16signed", []; + "Mint16unsigned", []; + "Mint32", []; + "Mint64", []; + "Mfloat32", []; + "Mfloat64", []; + "Many32", []; + "Many64", []; +]) + +let init_data = Sum("init_data", [ + "Init_int8", [int]; + "Init_int16", [int]; + "Init_int32", [int]; + "Init_int64", [int64]; + "Init_float32", [float32]; + "Init_float64", [float]; + "Init_space", [_Z]; + "Init_addrof", [ident; int]; +]) + +let globvar v = Record(sprintf "globvar[%s]" (describe_ty v), [ + "gvar_info", v; + "gvar_init", list init_data; + "gvar_readonly", bool; + "gvar_volatile", bool; +]) + +let globdef f v = Sum(sprintf "globdef[%s][%s]" (describe_ty f) (describe_ty v), [ + "Gfun", [f]; + "Gvar", [globvar v]; +]) + +let external_function = Sum("external_function", [ + "EF_external", [ident; signature]; + "EF_builtin", [ident; signature]; + "EF_vload", [memory_chunk]; + "EF_vstore", [memory_chunk]; + "EF_vload_global", [memory_chunk; ident; int]; + "EF_vstore_global", [memory_chunk; ident; int]; + "EF_malloc", []; + "EF_free", []; + "EF_memcpy", [_Z; _Z]; + "EF_annot", [ident; list typ]; + "EF_annot_val", [ident; typ]; + "EF_inline_asm", [ident; signature; list string]; +]) + +(* From Values *) + +let block = positive + +let val_ = Sum("val", [ + "Vundef", []; + "Vint", [int]; + "Vlong", [int64]; + "Vfloat", [float]; + "Vsingle", [float32]; + "Vptr", [block; int]; +]) + +(* From Ctypes *) + +let signedness = Sum("signedness", [ + "Signed", []; + "Unsigned", []; +]) + +let intsize = Sum("intsize", [ + "I8", []; + "I16", []; + "I32", []; + "IBool", []; +]) + +let floatsize = Sum("floatsize", [ + "F32", []; + "F64", []; +]) + +let attr = Record("attr", [ + "attr_volatile", bool; + "attr_alignas", option _N; +]) + +let attr_default = { + dfl_val = Ctypes.noattr; + dfl_print = (function `Coq -> Some "noattr" | _ -> None) +} + +let attr_d = Default(attr, attr_default) + +let rec type_ = Sum("type", [ + "Tvoid", []; + "Tint", [intsize; signedness; attr_d]; + "Tlong", [signedness; attr_d]; + "Tfloat", [floatsize; attr_d]; + "Tpointer", [type_; attr_d]; + "Tarray", [type_; _Z; attr_d]; + "Tfunction", [typelist; type_; calling_convention_d]; + "Tstruct", [ident; attr_d]; + "Tunion", [ident; attr_d]; +]) +and typelist = Sum("typelist", [ + "Tnil", []; + "Tcons", [type_; typelist]; +]) + +let struct_or_union = Sum("struct_or_union", [ + "Struct", []; + "Union", []; +]) + +let members = list (pair ident type_) + +let composite_definition = Sum("composite_definition", [ + "Composite", [ident; struct_or_union; members; attr_d]; +]) + +let composite = Record("composite",[ + "co_su", struct_or_union; + "co_members", members; + "co_attr", attr; + "co_sizeof", _Z; + "co_alignof", _Z; + "co_rank", nat +]) + +let composite_env = ptree composite + +(* From Cop *) + +let unary_operation = Sum("unary_operation", [ + "Onotbool", []; + "Onotint", []; + "Oneg", []; + "Oabsfloat", []; +]) + +let binary_operation = Sum("binary_operation", [ + "Oadd", []; + "Osub", []; + "Omul", []; + "Odiv", []; + "Omod", []; + "Oand", []; + "Oor", []; + "Oxor", []; + "Oshl", []; + "Oshr", []; + "Oeq", []; + "One", []; + "Olt", []; + "Ogt", []; + "Ole", []; + "Oge", []; +]) + +let incr_or_decr = Sum("incr_or_decr", [ + "Incr", []; + "Decr", []; +]) + +(* From Csyntax *) + +let rec expr = Sum("expr", [ + "Eval", [val_; type_]; + "Evar", [ident; type_]; + "Efield", [expr; ident; type_]; + "Evalof", [expr; type_]; + "Ederef", [expr; type_]; + "Eaddrof", [expr; type_]; + "Eunop", [unary_operation; expr; type_]; + "Ebinop", [binary_operation; expr; expr; type_]; + "Ecast", [expr; type_]; + "Eseqand", [expr; expr; type_]; + "Eseqor", [expr; expr; type_]; + "Econdition", [expr; expr; expr; type_]; + "Esizeof", [type_; type_]; + "Ealignof", [type_; type_]; + "Eassign", [expr; expr; type_]; + "Eassignop", [binary_operation; expr; expr; type_; type_]; + "Epostincr", [incr_or_decr; expr; type_]; + "Ecomma", [expr; expr; type_]; + "Ecall", [expr; exprlist; type_]; + "Ebuiltin", [external_function; typelist; exprlist; type_]; + "Eloc", [block; int; type_]; + "Eparen", [expr; type_; type_]; +]) +and exprlist = Sum("exprlist", [ + "Enil", []; + "Econs", [expr; exprlist]; +]) + +let label = ident + +let rec statement = Sum("statement", [ + "Sskip", []; + "Sdo", [expr]; + "Ssequence", [statement; statement]; + "Sifthenelse", [expr; statement; statement]; + "Swhile", [expr; statement]; + "Sdowhile", [expr; statement]; + "Sfor", [statement; expr; statement; statement]; + "Sbreak", []; + "Scontinue", []; + "Sreturn", [option expr]; + "Sswitch", [expr; labeled_statements]; + "Slabel", [label; statement]; + "Sgoto", [label]; +]) +and labeled_statements = Sum("labeled_statements", [ + "LSnil", []; + "LScons", [option _Z; statement; labeled_statements]; +]) + +let function_ = Record("function", [ + "fn_return", type_; + "fn_callconv", calling_convention_d; + "fn_params", list (pair ident type_); + "fn_vars", list (pair ident type_); + "fn_body", statement; +]) + +let fundef = Sum("fundef", [ + "Internal", [function_]; + "External", [external_function; typelist; type_; calling_convention_d]; +]) + +let repr_program = Record("program", [ + "prog_defs", list (pair ident (globdef fundef type_)); + "prog_public", list ident; + "prog_main", ident; + "prog_types", list composite_definition; + "prog_comp_env", composite_env +]) + +type program2 = Program of + (AST.ident * (Csyntax.fundef, Ctypes.coq_type) AST.globdef) list + * AST.ident list + * AST.ident + * Ctypes.composite_definition list + +let program2 = Sum("program2", [ + "mkprogram", [list (pair ident (globdef fundef type_)); + list ident; + ident; + list composite_definition] +]) + +let program2_of_program p = + Csyntax.(Program(p.prog_defs, p.prog_public, p.prog_main, p.prog_types)) +let program_of_program2 (Program(d,p,m,t)) = + Csyntax.( + match Ctypes.build_composite_env t with + | Errors.Error _ -> assert false + | Errors.OK e -> {prog_defs = d; prog_public = p; prog_main = m; + prog_types = t; prog_comp_env = e}) + +let program = As(program2, { + conv_name = "program"; + conv_check = check repr_program; + conv_out = program2_of_program; + conv_in = program_of_program2 +}) + diff --git a/driver/Driver.ml b/driver/Driver.ml index b89d93c1..4bd08a88 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -536,9 +536,12 @@ let _ = | "arm" -> if Configuration.is_big_endian then Machine.arm_bigendian else Machine.arm_littleendian - | "ia32" -> if Configuration.abi = "macosx" - then Machine.x86_32_macosx - else Machine.x86_32 + | "ia32" -> if Configuration.model = "64" then + Machine.x86_64 + else + if Configuration.abi = "macosx" + then Machine.x86_32_macosx + else Machine.x86_32 | _ -> assert false end; Builtins.set C2C.builtins; -- cgit From 3bef0962079cf971673b4267b0142bd5fe092509 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:26:46 +0200 Subject: Support for 64-bit architectures: update the PowerPC port The PowerPC port remains 32-bit only, no support is added for PPC 64. This shows how much work is needed to update an existing port a minima. --- driver/Ctydescr.ml | 456 ----------------------------------------------------- 1 file changed, 456 deletions(-) delete mode 100644 driver/Ctydescr.ml (limited to 'driver') diff --git a/driver/Ctydescr.ml b/driver/Ctydescr.ml deleted file mode 100644 index 8091257b..00000000 --- a/driver/Ctydescr.ml +++ /dev/null @@ -1,456 +0,0 @@ -open Printf -open Camlcoq -open Tydesc - -let check ty x = TyIO.check x ty; true - -(* From stdlib *) - -let list t = List t -let pair t1 t2 = Tuple [t1;t2] - -let rec repr_nat = Sum("nat", [ - "O", []; - "S", [repr_nat] -]) - -let nat = Base { - base_name = "nat"; - base_check = check repr_nat; - base_parse = (fun synt s -> assert false); - base_print = (fun synt x -> - let s = string_of_int (Nat.to_int x) in - match synt with - | `Coq -> s ^ "%nat" - | _ -> s) -} - -let rec repr_positive = Sum("positive", [ - "xI", [repr_positive]; - "xO", [repr_positive]; - "xH", [] -]) - -let positive = Base { - base_name = "positive"; - base_check = check repr_positive; - base_parse = (fun synt s -> assert false); - base_print = (fun synt x -> Z.to_string (Z.Zpos x)) -} - -let repr_N = Sum("N", [ - "N0", []; - "Npos", [repr_positive] -]) - -let _N = Base { - base_name = "N"; - base_check = check repr_N; - base_parse = (fun synt s -> assert false); - base_print = (fun synt x -> - let y = match x with N.N0 -> Z.Z0 | N.Npos p -> Z.Zpos p in - let s = Z.to_string y in - match synt with - | `Coq -> s ^ "%N" - | _ -> s) -} - -let repr_Z = Sum("Z", [ - "Z0", []; - "Zpos", [repr_positive]; - "Zneg", [repr_positive] -]) - -let _Z = Base { - base_name = "Z"; - base_check = check repr_Z; - base_parse = (fun synt s -> assert false); - base_print = (fun synt x -> - let s = Z.to_string x in - match synt with - | `Coq -> s ^ "%Z" - | _ -> s) -} - -(* From Integers *) - -let int = Base { - base_name = "int"; - base_check = check repr_Z; - base_parse = (fun synt s -> - let (n, s') = get_number s in - try (coqint_of_camlint (Int32.of_string n), s') - with Failure _ -> - raise (Parsing_failure(get_position s, sprintf "bad 'int' literal %S" n))); - base_print = (fun synt x -> - let s = Z.to_string x in - match synt with - | `Coq -> "(mkint " ^ s ^ "%Z)" - | _ -> s) -} - -let int64 = Base { - base_name = "int64"; - base_check = check repr_Z; - base_parse = (fun synt s -> - let (n, s') = get_number s in - try (coqint_of_camlint64 (Int64.of_string n), s') - with Failure _ -> - raise (Parsing_failure(get_position s, sprintf "bad 'int64' literal %S" n))); - base_print = (fun synt x -> - let s = Z.to_string x in - match synt with - | `Coq -> "(mkint64 " ^ s ^ "%Z)" - | _ -> s) -} - -(* From Floats *) - -let nan_pl = positive - -let binary_float = Sum("binary_float", [ - "B754_zero", [bool]; - "B754_infinity", [bool]; - "B754_nan", [bool; nan_pl]; - "B754_finite", [bool; positive; _Z] -]) - -let float = Base { - base_name = "float"; - base_check = check binary_float; - base_parse = (fun synt s -> - let (n, s') = get_number s in - try (Floats.Float.of_bits (coqint_of_camlint64 (Int64.of_string n)), s') - with Failure _ -> - raise (Parsing_failure(get_position s, sprintf "bad 'float' literal %S" n))); - base_print = (fun synt x -> - let s = Z.to_string (Floats.Float.to_bits x) in - match synt with - | `Coq -> "(mkfloat " ^ s ^ "%Z)" - | _ -> s) -} - -let float32 = Base { - base_name = "float32"; - base_check = check binary_float; - base_parse = (fun synt s -> - let (n, s') = get_number s in - try (Floats.Float32.of_bits (coqint_of_camlint (Int32.of_string n)), s') - with Failure _ -> - raise (Parsing_failure(get_position s, sprintf "bad 'float32' literal %S" n))); - base_print = (fun synt x -> - let s = Z.to_string (Floats.Float.to_bits x) in - match synt with - | `Coq -> "(mkfloat32 " ^ s ^ "%Z)" - | _ -> s) -} - -(* From Maps *) - -let ptree a = - let rec t = Sum(sprintf "PTree.t[%s]" (describe_ty a), [ - "Leaf", []; - "Node", [t; option a; t] - ]) in t - -(* From AST *) - -let ident = positive - -let typ = Sum("typ", [ - "AST.Tint", []; - "AST.Tfloat", []; - "AST.Tlong", []; - "AST.Tsingle", []; - "AST.Tany32", []; - "AST.Tany64", []; -]) - -let calling_convention = Record("calling_convention", [ - "cc_vararg", bool; - "cc_structret", bool; -]) - -let default_calling_convention = { - dfl_val = AST.cc_default; - dfl_print = (function `Coq -> Some "cc_default" | _ -> None) -} - -let calling_convention_d = - Default(calling_convention, default_calling_convention) - -let signature = Record("signature", [ - "sig_args", list typ; - "sig_res", option typ; - "sig_cc", calling_convention_d; -]) - -let memory_chunk = Sum("memory_chunk", [ - "Mint8signed", []; - "Mint8unsigned", []; - "Mint16signed", []; - "Mint16unsigned", []; - "Mint32", []; - "Mint64", []; - "Mfloat32", []; - "Mfloat64", []; - "Many32", []; - "Many64", []; -]) - -let init_data = Sum("init_data", [ - "Init_int8", [int]; - "Init_int16", [int]; - "Init_int32", [int]; - "Init_int64", [int64]; - "Init_float32", [float32]; - "Init_float64", [float]; - "Init_space", [_Z]; - "Init_addrof", [ident; int]; -]) - -let globvar v = Record(sprintf "globvar[%s]" (describe_ty v), [ - "gvar_info", v; - "gvar_init", list init_data; - "gvar_readonly", bool; - "gvar_volatile", bool; -]) - -let globdef f v = Sum(sprintf "globdef[%s][%s]" (describe_ty f) (describe_ty v), [ - "Gfun", [f]; - "Gvar", [globvar v]; -]) - -let external_function = Sum("external_function", [ - "EF_external", [ident; signature]; - "EF_builtin", [ident; signature]; - "EF_vload", [memory_chunk]; - "EF_vstore", [memory_chunk]; - "EF_vload_global", [memory_chunk; ident; int]; - "EF_vstore_global", [memory_chunk; ident; int]; - "EF_malloc", []; - "EF_free", []; - "EF_memcpy", [_Z; _Z]; - "EF_annot", [ident; list typ]; - "EF_annot_val", [ident; typ]; - "EF_inline_asm", [ident; signature; list string]; -]) - -(* From Values *) - -let block = positive - -let val_ = Sum("val", [ - "Vundef", []; - "Vint", [int]; - "Vlong", [int64]; - "Vfloat", [float]; - "Vsingle", [float32]; - "Vptr", [block; int]; -]) - -(* From Ctypes *) - -let signedness = Sum("signedness", [ - "Signed", []; - "Unsigned", []; -]) - -let intsize = Sum("intsize", [ - "I8", []; - "I16", []; - "I32", []; - "IBool", []; -]) - -let floatsize = Sum("floatsize", [ - "F32", []; - "F64", []; -]) - -let attr = Record("attr", [ - "attr_volatile", bool; - "attr_alignas", option _N; -]) - -let attr_default = { - dfl_val = Ctypes.noattr; - dfl_print = (function `Coq -> Some "noattr" | _ -> None) -} - -let attr_d = Default(attr, attr_default) - -let rec type_ = Sum("type", [ - "Tvoid", []; - "Tint", [intsize; signedness; attr_d]; - "Tlong", [signedness; attr_d]; - "Tfloat", [floatsize; attr_d]; - "Tpointer", [type_; attr_d]; - "Tarray", [type_; _Z; attr_d]; - "Tfunction", [typelist; type_; calling_convention_d]; - "Tstruct", [ident; attr_d]; - "Tunion", [ident; attr_d]; -]) -and typelist = Sum("typelist", [ - "Tnil", []; - "Tcons", [type_; typelist]; -]) - -let struct_or_union = Sum("struct_or_union", [ - "Struct", []; - "Union", []; -]) - -let members = list (pair ident type_) - -let composite_definition = Sum("composite_definition", [ - "Composite", [ident; struct_or_union; members; attr_d]; -]) - -let composite = Record("composite",[ - "co_su", struct_or_union; - "co_members", members; - "co_attr", attr; - "co_sizeof", _Z; - "co_alignof", _Z; - "co_rank", nat -]) - -let composite_env = ptree composite - -(* From Cop *) - -let unary_operation = Sum("unary_operation", [ - "Onotbool", []; - "Onotint", []; - "Oneg", []; - "Oabsfloat", []; -]) - -let binary_operation = Sum("binary_operation", [ - "Oadd", []; - "Osub", []; - "Omul", []; - "Odiv", []; - "Omod", []; - "Oand", []; - "Oor", []; - "Oxor", []; - "Oshl", []; - "Oshr", []; - "Oeq", []; - "One", []; - "Olt", []; - "Ogt", []; - "Ole", []; - "Oge", []; -]) - -let incr_or_decr = Sum("incr_or_decr", [ - "Incr", []; - "Decr", []; -]) - -(* From Csyntax *) - -let rec expr = Sum("expr", [ - "Eval", [val_; type_]; - "Evar", [ident; type_]; - "Efield", [expr; ident; type_]; - "Evalof", [expr; type_]; - "Ederef", [expr; type_]; - "Eaddrof", [expr; type_]; - "Eunop", [unary_operation; expr; type_]; - "Ebinop", [binary_operation; expr; expr; type_]; - "Ecast", [expr; type_]; - "Eseqand", [expr; expr; type_]; - "Eseqor", [expr; expr; type_]; - "Econdition", [expr; expr; expr; type_]; - "Esizeof", [type_; type_]; - "Ealignof", [type_; type_]; - "Eassign", [expr; expr; type_]; - "Eassignop", [binary_operation; expr; expr; type_; type_]; - "Epostincr", [incr_or_decr; expr; type_]; - "Ecomma", [expr; expr; type_]; - "Ecall", [expr; exprlist; type_]; - "Ebuiltin", [external_function; typelist; exprlist; type_]; - "Eloc", [block; int; type_]; - "Eparen", [expr; type_; type_]; -]) -and exprlist = Sum("exprlist", [ - "Enil", []; - "Econs", [expr; exprlist]; -]) - -let label = ident - -let rec statement = Sum("statement", [ - "Sskip", []; - "Sdo", [expr]; - "Ssequence", [statement; statement]; - "Sifthenelse", [expr; statement; statement]; - "Swhile", [expr; statement]; - "Sdowhile", [expr; statement]; - "Sfor", [statement; expr; statement; statement]; - "Sbreak", []; - "Scontinue", []; - "Sreturn", [option expr]; - "Sswitch", [expr; labeled_statements]; - "Slabel", [label; statement]; - "Sgoto", [label]; -]) -and labeled_statements = Sum("labeled_statements", [ - "LSnil", []; - "LScons", [option _Z; statement; labeled_statements]; -]) - -let function_ = Record("function", [ - "fn_return", type_; - "fn_callconv", calling_convention_d; - "fn_params", list (pair ident type_); - "fn_vars", list (pair ident type_); - "fn_body", statement; -]) - -let fundef = Sum("fundef", [ - "Internal", [function_]; - "External", [external_function; typelist; type_; calling_convention_d]; -]) - -let repr_program = Record("program", [ - "prog_defs", list (pair ident (globdef fundef type_)); - "prog_public", list ident; - "prog_main", ident; - "prog_types", list composite_definition; - "prog_comp_env", composite_env -]) - -type program2 = Program of - (AST.ident * (Csyntax.fundef, Ctypes.coq_type) AST.globdef) list - * AST.ident list - * AST.ident - * Ctypes.composite_definition list - -let program2 = Sum("program2", [ - "mkprogram", [list (pair ident (globdef fundef type_)); - list ident; - ident; - list composite_definition] -]) - -let program2_of_program p = - Csyntax.(Program(p.prog_defs, p.prog_public, p.prog_main, p.prog_types)) -let program_of_program2 (Program(d,p,m,t)) = - Csyntax.( - match Ctypes.build_composite_env t with - | Errors.Error _ -> assert false - | Errors.OK e -> {prog_defs = d; prog_public = p; prog_main = m; - prog_types = t; prog_comp_env = e}) - -let program = As(program2, { - conv_name = "program"; - conv_check = check repr_program; - conv_out = program2_of_program; - conv_in = program_of_program2 -}) - -- cgit From af5758ac9414541a62bf08ae44373b441b8653ec Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 24 Oct 2016 14:27:35 +0200 Subject: driver/Interp: update Cherry-pick commit d1311e6 from trunk. Simplify convert_external_arg so that it works both in 32 and 64 bits. --- driver/Interp.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index c197d004..1e328a70 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -304,7 +304,7 @@ let format_value m flags length conv arg = format_int64 (flags ^ conv) (camlint64_of_coqint i) | ('d'|'i'|'u'|'o'|'x'|'X'), ("ll"|"j"), _ -> " + | ('f'|'e'|'E'|'g'|'G'|'a'), (""|"l"), Vfloat f -> format_float (flags ^ conv) (camlfloat_of_coqfloat f) | ('f'|'e'|'E'|'g'|'G'|'a'), "", _ -> ">=) opt f = match opt with None -> None | Some arg -> f arg (* Like eventval_of_val, but accepts static globals as well *) let convert_external_arg ge v t = - match v, t with - | Vint i, AST.Tint -> Some (EVint i) - | Vfloat f, AST.Tfloat -> Some (EVfloat f) - | Vsingle f, AST.Tsingle -> Some (EVsingle f) - | Vlong n, AST.Tlong -> Some (EVlong n) - | Vptr(b, ofs), AST.Tint -> + match v with + | Vint i -> Some (EVint i) + | Vfloat f -> Some (EVfloat f) + | Vsingle f -> Some (EVsingle f) + | Vlong n -> Some (EVlong n) + | Vptr(b, ofs) -> Senv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) - | _, _ -> None + | _ -> None let rec convert_external_args ge vl tl = match vl, tl with -- cgit From 883341719d7d6868f8165541e7e13ac45192a358 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 27 Oct 2016 11:06:09 +0200 Subject: 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). --- driver/Driver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 4bd08a88..3cc1bcad 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -536,7 +536,7 @@ let _ = | "arm" -> if Configuration.is_big_endian then Machine.arm_bigendian else Machine.arm_littleendian - | "ia32" -> if Configuration.model = "64" then + | "x86" -> if Configuration.model = "64" then Machine.x86_64 else if Configuration.abi = "macosx" -- cgit