From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jan 2013 09:10:29 +0000 Subject: Ported to Coq 8.4pl1. Merge of branches/coq-8.4. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Asm_printers.ml | 17 +++-------------- checklink/Check.ml | 11 +++++------ checklink/Frameworks.ml | 4 ++-- checklink/Library.ml | 26 ++++++++++++-------------- 4 files changed, 22 insertions(+), 36 deletions(-) (limited to 'checklink') diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml index 094d51d..aeb4b3f 100644 --- a/checklink/Asm_printers.ml +++ b/checklink/Asm_printers.ml @@ -1,21 +1,10 @@ +open Camlcoq open Asm open AST -open BinInt -open BinPos open Library -let rec int_of_pos = function - | Coq_xH -> 1 - | Coq_xO q -> 2 * int_of_pos q - | Coq_xI q -> 2 * int_of_pos q + 1 - -let string_of_pos p = string_of_int (int_of_pos p) - -let string_of_coq_Z = function - | Z0 -> "0" - | Zpos p -> string_of_pos p - | Zneg p -> "-" ^ string_of_pos p - +let string_of_pos p = Z.to_string (Z.Zpos p) +let string_of_coq_Z = Z.to_string let string_of_ident = string_of_pos let string_of_label = string_of_pos let string_of_iint = string_of_coq_Z diff --git a/checklink/Check.ml b/checklink/Check.ml index a1cc004..9d668fa 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -1,8 +1,7 @@ +open Camlcoq open Asm open Asm_printers open AST -open BinInt -open BinPos open Bitstring_utils open C2C open Camlcoq @@ -204,7 +203,7 @@ let re_variadic_stub: Str.regexp = Str.regexp "\\(.*\\)\\$[if]*$" address, unless the symbol is a stub from CompCert. Otherwise, it filters out all symbols whose virtual address does not match [vaddr]. *) -let idmap_unify (k: positive) (vaddr: int32) (sfw: s_framework) +let idmap_unify (k: P.t) (vaddr: int32) (sfw: s_framework) : s_framework or_err = try ( (* get the list of possible symbols for ident [k] *) @@ -438,13 +437,13 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw -> (* sda should be handled separately in places it occurs *) fatal "Unhandled Csymbol_sda, please report." -let match_z_int32 (cz: coq_Z) (ei: int32) = +let match_z_int32 (cz: Z.t) (ei: int32) = let cz = z_int32 cz in check_eq ( Printf.sprintf "match_z_int32 %s %s" (string_of_int32 cz) (string_of_int32 ei) ) cz ei -let match_z_int (cz: coq_Z) (ei: int) = +let match_z_int (cz: Z.t) (ei: int) = let cz = z_int32 cz in let ei = Safe32.of_int ei in check_eq ( @@ -452,7 +451,7 @@ let match_z_int (cz: coq_Z) (ei: int) = ) cz ei (* [m] is interpreted as a bitmask, and checked against [ei]. *) -let match_mask (m: coq_Z) (ei: int32) = +let match_mask (m: Z.t) (ei: int32) = let m = z_int32_lax m in check_eq ( Printf.sprintf "match_mask %s %s" diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index 074a432..35144dc 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -1,6 +1,6 @@ +open Camlcoq open Asm open AST -open BinPos open ELF_types open Lens open Library @@ -62,7 +62,7 @@ type e_framework = { } module PosOT = struct - type t = positive + type t = P.t let compare = Pervasives.compare end diff --git a/checklink/Library.ml b/checklink/Library.ml index c38c1f1..acea80a 100644 --- a/checklink/Library.ml +++ b/checklink/Library.ml @@ -1,5 +1,3 @@ -open BinInt -open BinPos open Camlcoq type bitstring = Bitstring.bitstring @@ -75,9 +73,9 @@ exception Int32Overflow (* Can only return positive numbers 0 <= res < 2^31 *) let positive_int32 p = let rec positive_int32_unsafe = function - | Coq_xI(p) -> Int32.(add (shift_left (positive_int32_unsafe p) 1) 1l) - | Coq_xO(p) -> Int32.(shift_left (positive_int32_unsafe p) 1) - | Coq_xH -> 1l + | P.Coq_xI(p) -> Int32.(add (shift_left (positive_int32_unsafe p) 1) 1l) + | P.Coq_xO(p) -> Int32.(shift_left (positive_int32_unsafe p) 1) + | P.Coq_xH -> 1l in let res = positive_int32_unsafe p in if res >= 0l @@ -86,27 +84,27 @@ let positive_int32 p = (* This allows for 1 bit of overflow, effectively returning a negative *) let rec positive_int32_lax = function -| Coq_xI(p) -> +| P.Coq_xI(p) -> let acc = positive_int32_lax p in if acc < 0l then raise Int32Overflow else Int32.(add (shift_left acc 1) 1l) -| Coq_xO(p) -> +| P.Coq_xO(p) -> let acc = positive_int32_lax p in if acc < 0l then raise Int32Overflow else Int32.shift_left acc 1 -| Coq_xH -> 1l +| P.Coq_xH -> 1l let z_int32 = function -| Z0 -> 0l -| Zpos(p) -> positive_int32 p -| Zneg(p) -> Int32.neg (positive_int32 p) +| Z.Z0 -> 0l +| Z.Zpos(p) -> positive_int32 p +| Z.Zneg(p) -> Int32.neg (positive_int32 p) let z_int32_lax = function -| Z0 -> 0l -| Zpos(p) -> positive_int32_lax p -| Zneg(_) -> raise Int32Overflow +| Z.Z0 -> 0l +| Z.Zpos(p) -> positive_int32_lax p +| Z.Zneg(_) -> raise Int32Overflow let z_int z = Safe32.to_int (z_int32 z) -- cgit v1.2.3