Commit fc261f5d authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

ce-display: improve displaying of float counterexamples for CVC4

parent 2d9584fd
......@@ -36,61 +36,110 @@ type float_type =
| Float_value of string * string * string
| Float_hexa of string * float
type repr = BinRepr | HexaRepr
let interp_float ?(interp=true) b eb sb =
try
(* We don't interpret when this is disable *)
if not interp then
raise Exit;
let is_neg = match b with
| "#b0" -> false
| "#b1" -> true
| _ -> raise Exit
in
if String.length eb = 13 && String.sub eb 0 2 = "#b" &&
String.length sb = 15 && String.sub sb 0 2 = "#x" then
(* binary 64 *)
let exp_base2 = String.sub eb 2 11 in
let mant_base16 = String.sub sb 2 13 in
let exp = int_of_string ("0b" ^ exp_base2) in
if exp = 0 then (* subnormals *)
let s = (if is_neg then "-" else "")^
"0x0."^mant_base16^"p-1023"
in Float_hexa(s,float_of_string s)
else if exp = 2047 then (* infinities and NaN *)
if mant_base16="0000000000000" then
if is_neg then Minus_infinity else Plus_infinity
else Not_a_number
else
let exp = exp - 1023 in
let s = (if is_neg then "-" else "")^
"0x1."^mant_base16^"p"^(string_of_int exp)
in Float_hexa(s,float_of_string s)
else
if String.length eb = 4 && String.sub eb 0 2 = "#x" &&
String.length sb = 25 && String.sub sb 0 2 = "#b" then
(* binary 32 *)
let exp_base16 = String.sub eb 2 2 in
let mant_base2 = String.sub sb 2 23 in
let mant_base16 =
Format.asprintf "%06x" (2*int_of_string ("0b" ^ mant_base2))
in
let exp = int_of_string ("0x" ^ exp_base16) in
if exp = 0 then (* subnormals *)
let s = (if is_neg then "-" else "")^
"0x0."^mant_base16^"p-127"
in Float_hexa(s,float_of_string s)
else if exp = 255 then (* infinities and NaN *)
if mant_base16="0000000" then
if is_neg then Minus_infinity else Plus_infinity
else Not_a_number
else
let exp = exp - 127 in
let s = (if is_neg then "-" else "")^
"0x1."^mant_base16^"p"^(string_of_int exp)
in Float_hexa(s,float_of_string s)
else raise Exit
with Exit -> Float_value (b, eb, sb)
let convert (r: repr) s =
(* Convert number of less than 63 bits TODO *)
match r with
| BinRepr when String.length s <= 62 -> int_of_string ("0b" ^ s)
| HexaRepr when String.length s <= 15 -> int_of_string ("0x" ^ s)
| _ -> (* Too big to fit into an integer *) raise Exit in
let rec pow x n =
assert (n <= 63);
match n with
| p when p <= 0 -> 1
| 1 -> x
| p -> x * pow x (p-1) in
let get_repr s len =
if String.sub s 0 2 = "#b" then
BinRepr, String.sub s 2 (len - 2), (len - 2)
else if String.sub s 0 2 = "#x" then
HexaRepr, String.sub s 2 (len - 2), (len - 2) * 4
else raise Exit in
let pad_with_zeros width s =
let s_len = String.length s in
let filled =
let len = width - s_len in
if len <= 0 then "" else String.make len '0' in
filled ^ s in
let only_zeros s =
(* Check that there is only 0 in the string *)
let b = ref true in
for i = 0 to String.length s - 1 do
b := !b && (s.[i] = '0')
done;
!b in
try
(* We don't interpret when this is disable *)
if not interp then
raise Exit;
let is_neg = match b with
| "#b0" -> false
| "#b1" -> true
| _ -> raise Exit
in
let eb_len = String.length eb in
let sb_len = String.length sb in
if eb_len < 2 || sb_len < 2 then raise Exit;
let eb_repr, eb, eb_size = get_repr eb eb_len in
let sb_repr, sb, sb_size = get_repr sb sb_len in
(* Values for the type of float obtained *)
(* Exponent bias *)
let exp_bias = (pow 2 (eb_size - 1)) - 1 in
(* Maximum exponent value *)
let max_exp = (pow 2 eb_size) - 1 in
(* Length of the hexadecimal representation (after the ".") *)
let length_of_number =
if sb_size mod 4 = 0 then sb_size / 4 else sb_size / 4 + 1 in
(* Compute exponent (int) and mantissa (string of hexa) *)
let exp = convert eb_repr eb in
let mant_base16 =
let c = convert sb_repr sb in
let c =
(* The hex value is used after the decimal point. So we need to adjust
it to the number of binary elements there are.
Example in 32bits: significand is 23 bits, and the hexadecimal
representation will have a multiple of 4 bits (ie 24). So, we need to
multiply by two to account the difference. *)
if sb_repr = BinRepr then
let adjust = 4 - sb_size mod 4 in
(* No adjustment needed *)
if adjust = 4 then
c
else
(pow 2 adjust) * c
else
c in
pad_with_zeros length_of_number (Format.asprintf "%x" c)
in
match exp with
| 0 (* subnormals and zero *) ->
(* Case for zero *)
if only_zeros mant_base16 then
if is_neg then Minus_zero else Plus_zero
else
(* Subnormals *)
let s = (if is_neg then "-" else "")^
"0x0."^mant_base16^"p-"^(string_of_int exp_bias)
in Float_hexa (s, float_of_string s)
| e when e = max_exp (* infinities and NaN *) ->
if only_zeros mant_base16 then
if is_neg then Minus_infinity else Plus_infinity
else Not_a_number
| _ (* Normal floats *) ->
let exp = exp - exp_bias in
let s = (if is_neg then "-" else "")^
"0x1."^mant_base16^"p"^(string_of_int exp)
in Float_hexa(s,float_of_string s)
with Exit -> Float_value (b, eb, sb)
type model_value =
| Integer of string
......@@ -275,7 +324,7 @@ let print_float_human fmt f =
| Not_a_number ->
fprintf fmt "NaN"
| Float_value (b, eb, sb) ->
fprintf fmt "float_bits(%s,%s,%s)" b eb sb
fprintf fmt "float_bits(%s,%s,%s)" b eb sb
| Float_hexa(s,f) -> fprintf fmt "%s (%g)" s f
let rec print_array_human fmt (arr: model_array) =
......
......@@ -61,7 +61,7 @@ module GenericFloat
(** {3 Constructors and Constants} *)
val constant zeroF : t (** +0.0 *)
(* exp_bias = 2^(sb - 1) - 1 *)
(* exp_bias = 2^(eb - 1) - 1 *)
(* max_finite_exp = 2^sb - 2 - exp_bias = exp_bias *)
(* max_significand = (2^eb + 2^eb - 1) * 2^(1-eb) *)
(* max_value = (2^eb + 2^eb - 1) * 2^(1-eb) * 2 ^ max_finite_exp *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment