diff --git a/.gitignore b/.gitignore
index 065769eeba111c28e7250e496aec936c81b7db4f..633a7d72b4f6a96980eec0d1d508467a17ddfa92 100644
--- a/.gitignore
+++ b/.gitignore
@@ -204,3 +204,4 @@ hello-*.tar.gz
/src/plugins/gui/gtk_compat.ml
/src/plugins/gui/GSourceView.ml
/src/plugins/gui/GSourceView.mli
+/tests/crowbar/integer_bb_pretty
diff --git a/src/libraries/stdlib/integer.ml b/src/libraries/stdlib/integer.ml
index 55d36122770094da3949f3540941b9fdc0bdccbd..1a7e593f79aede19b4ecddaf53d51964fa7020ce 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -109,17 +109,85 @@ let popcount = Z.popcount
raises multiple [Failure _] exceptions *)
failwith "Integer.of_string"
-
let max_int64 = of_int64 Int64.max_int
let min_int64 = of_int64 Int64.min_int
-
let to_string = Z.to_string
let to_float = Z.to_float
let of_float z =
try Z.of_float z
with Z.Overflow -> raise Too_big
+ let bdigits = [|
+ "0000" ; (* 0 *)
+ "0001" ; (* 1 *)
+ "0010" ; (* 2 *)
+ "0011" ; (* 3 *)
+ "0100" ; (* 4 *)
+ "0101" ; (* 5 *)
+ "0110" ; (* 6 *)
+ "0111" ; (* 7 *)
+ "1000" ; (* 8 *)
+ "1001" ; (* 9 *)
+ "1010" ; (* 10 *)
+ "1011" ; (* 11 *)
+ "1100" ; (* 12 *)
+ "1101" ; (* 13 *)
+ "1110" ; (* 14 *)
+ "1111" ; (* 15 *)
+ |]
+
+ let pp_bin_pos fmt r = Format.pp_print_string fmt bdigits.(r)
+ let pp_bin_neg fmt r = Format.pp_print_string fmt bdigits.(15-r)
+
+ let pp_hex_pos fmt r = Format.fprintf fmt "%04X" r
+ let pp_hex_neg fmt r = Format.fprintf fmt "%04X" (0xFFFF-r)
+
+ let bmask_bin = Z.of_int 0xF (* 4 bits mask *)
+ let bmask_hex = Z.of_int 0xFFFF (* 64 bits mask *)
+
+ type digits = {
+ nbits : int ; (* max number of bits *)
+ bsize : int ; (* bits in each bloc *)
+ bmask : Z.t ; (* block mask, must be (1 << bsize) - 1 *)
+ sep : string ;
+ pp : Format.formatter -> int -> unit ; (* print one block *)
+ }
+
+ let rec pp_digits d fmt n v =
+ if gt v zero || n < d.nbits then
+ begin
+ let r = Z.to_int (Z.logand v d.bmask) in
+ let k = d.bsize in
+ pp_digits d fmt (n + k) (Z.shift_right_trunc v k) ;
+ if gt v d.bmask || (n + k) < d.nbits
+ then Format.pp_print_string fmt d.sep ;
+ d.pp fmt r ;
+ end
+
+ let pp_bin ?(nbits=1) ?(sep="") fmt v =
+ let nbits = if nbits <= 0 then 1 else nbits in
+ if le zero v then
+ ( Format.pp_print_string fmt "0b" ;
+ pp_digits { nbits ; sep ; bsize=4 ;
+ bmask = bmask_bin ; pp = pp_bin_pos } fmt 0 v )
+ else
+ ( Format.pp_print_string fmt "1b" ;
+ pp_digits { nbits ; sep ; bsize=4 ;
+ bmask = bmask_bin ; pp = pp_bin_neg } fmt 0 (Z.lognot v) )
+
+ let pp_hex ?(nbits=1) ?(sep="") fmt v =
+ let nbits = if nbits <= 0 then 1 else nbits in
+ if le zero v then
+ ( Format.pp_print_string fmt "0x" ;
+ pp_digits { nbits ; sep ; bsize=16 ;
+ bmask = bmask_hex ; pp = pp_hex_pos } fmt 0 v )
+
+ else
+ ( Format.pp_print_string fmt "1x" ;
+ pp_digits { nbits ; sep ; bsize=16 ;
+ bmask = bmask_hex ; pp = pp_hex_neg } fmt 0 (Z.lognot v) )
+
let pretty ?(hexa=false) fmt v =
let rec aux v =
if gt v two_power_60 then
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 4e939382bf131017b673f534505420f04c0df94c..3ed0f1297471b8c393056437955eec4085c79363 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -150,8 +150,23 @@ val popcount: t -> int
val pretty : ?hexa:bool -> t Pretty_utils.formatter
-
+val pp_bin : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
+(** Print binary format. Digits are output by blocs of 4 bits
+ separated by [~sep] with at least [~nbits] total bits. If [nbits] is
+ non positive, it will be ignored.
+
+ Positive values are prefixed with ["0b"] and negative values
+ are printed as their 2-complement ([lnot]) with prefix ["1b"]. *)
+
+val pp_hex : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
+(** Print hexadecimal format. Digits are output by blocs of 16 bits
+ (4 hex digits) separated by [~sep] with at least [~nbits] total bits.
+ If [nbits] is non positive, it will be ignored.
+
+ Positive values are preffixed with ["0x"] and negative values
+ are printed as their 2-complement ([lnot]) with prefix ["1x"]. *)
(*
+
Local Variables:
compile-command: "make -C ../../.."
End:
diff --git a/tests/crowbar/integer_bb_pretty.ml b/tests/crowbar/integer_bb_pretty.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2c6ec812e2968f282f1efb3e3cb19a7c45c9ef0a
--- /dev/null
+++ b/tests/crowbar/integer_bb_pretty.ml
@@ -0,0 +1,59 @@
+open Crowbar
+
+let reparse v s =
+ let failure info =
+ Crowbar.fail
+ ("Pretty-printing '" ^ (Z.to_string v) ^ "' returns '" ^ s ^ "'" ^ info)
+ in
+ if String.length s <= 2 then failure "";
+ let is_neg = s.[0] = '1' in
+ let is_hex = s.[1] = 'x' in
+ let s = String.(concat "" (split_on_char '_' s)) in
+ let v' =
+ if is_neg then begin
+ let chr = if is_hex then 'F' else '1' in
+ let module M = struct exception Found of int end in
+ let check i c = if i > 1 && c <> chr then raise (M.Found i) in
+ try String.iteri check s; Z.minus_one
+ with M.Found idx ->
+ let len, v' =
+ if is_hex then begin
+ let remains = String.sub s idx (String.length s - idx) in
+ let v' = Z.of_string ("0x" ^ remains) in
+ 4 * (String.length remains), v'
+ end else begin
+ let remains = String.sub s idx (String.length s - idx) in
+ let v' = Z.of_string ("0b" ^ remains) in
+ String.length remains, v'
+ end
+ in
+ let m = Z.(one lsl len) in
+ let m = Z.pred m in
+ let v' = Z.logxor m v' in
+ Z.pred (Z.lognot (Z.pred v'))
+ end else
+ Z.of_string s
+ in
+ if not (Z.equal v v') then
+ failure (" reparsed as '" ^ Z.format "%b" v' ^ "' (" ^ Z.to_string v' ^ ")")
+
+let test z is_hex nbits has_sep =
+ guard (nbits >= 0 && nbits <= 1024);
+ let sep = if has_sep then Some "_" else None in
+ let pp z = if is_hex then
+ Integer.pp_hex ~nbits ?sep z
+ else
+ Integer.pp_bin ~nbits ?sep z
+ in
+ let s = Format.asprintf "%a" pp z in
+ reparse z s
+
+let zarith =
+ let open Crowbar in
+ fix (fun zarith ->
+ choose
+ [ map [int64] Z.of_int64;
+ map [zarith; int64] (fun z i -> Z.((z lsl 64) + of_int64 i)) ])
+
+let () = Crowbar.add_test ~name:"pp_bin_hex"
+ [ zarith; Crowbar.bool; Crowbar.int; Crowbar.bool ] test
diff --git a/tests/misc/oracle/pp_bin_hex.res.oracle b/tests/misc/oracle/pp_bin_hex.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4791a522a343769216bd7ce7e105707e34f739e4
--- /dev/null
+++ b/tests/misc/oracle/pp_bin_hex.res.oracle
@@ -0,0 +1,86 @@
+--------------------------------------------------
+Dec. 0
+Hex. 0x0000
+Bin. 0b0000_0000
+--------------------------------------------------
+Dec. 1
+Hex. 0x0001
+Bin. 0b0000_0001
+--------------------------------------------------
+Dec. -1
+Hex. 1xFFFF
+Bin. 1b1111_1111
+--------------------------------------------------
+Dec. 2
+Hex. 0x0002
+Bin. 0b0000_0010
+--------------------------------------------------
+Dec. -2
+Hex. 1xFFFE
+Bin. 1b1111_1110
+--------------------------------------------------
+Dec. 5
+Hex. 0x0005
+Bin. 0b0000_0101
+--------------------------------------------------
+Dec. -5
+Hex. 1xFFFB
+Bin. 1b1111_1011
+--------------------------------------------------
+Dec. 9
+Hex. 0x0009
+Bin. 0b0000_1001
+--------------------------------------------------
+Dec. -9
+Hex. 1xFFF7
+Bin. 1b1111_0111
+--------------------------------------------------
+Dec. 16
+Hex. 0x0010
+Bin. 0b0001_0000
+--------------------------------------------------
+Dec. -16
+Hex. 1xFFF0
+Bin. 1b1111_0000
+--------------------------------------------------
+Dec. 127
+Hex. 0x007F
+Bin. 0b0111_1111
+--------------------------------------------------
+Dec. -127
+Hex. 1xFF81
+Bin. 1b1000_0001
+--------------------------------------------------
+Dec. 128
+Hex. 0x0080
+Bin. 0b1000_0000
+--------------------------------------------------
+Dec. -128
+Hex. 1xFF80
+Bin. 1b1000_0000
+--------------------------------------------------
+Dec. 255
+Hex. 0x00FF
+Bin. 0b1111_1111
+--------------------------------------------------
+Dec. -255
+Hex. 1xFF01
+Bin. 1b0000_0001
+--------------------------------------------------
+Dec. 4279173135
+Hex. 0xFF0F_000F
+Bin. 0b1111_1111_0000_1111_0000_0000_0000_1111
+--------------------------------------------------
+Dec. -4279173135
+Hex. 1x00F0_FFF1
+Bin. 1b0000_0000_1111_0000_1111_1111_1111_0001
+--------------------------------------------------
+Dec. 386334727
+Hex. 0x1707_0007
+Bin. 0b0001_0111_0000_0111_0000_0000_0000_0111
+--------------------------------------------------
+Dec. -386334727
+Hex. 1xE8F8_FFF9
+Bin. 1b1110_1000_1111_1000_1111_1111_1111_1001
+--------------------------------------------------
+[kernel] Parsing tests/misc/pp_bin_hex.i (no preprocessing)
diff --git a/tests/misc/pp_bin_hex.i b/tests/misc/pp_bin_hex.i
new file mode 100644
index 0000000000000000000000000000000000000000..a53499be69922b6d91cd0d4926968829ccf22a93
--- /dev/null
+++ b/tests/misc/pp_bin_hex.i
@@ -0,0 +1,3 @@
+/* run.config
+ OPT: -no-autoload-plugins -load-script tests/misc/pp_bin_hex.ml
+*/
diff --git a/tests/misc/pp_bin_hex.ml b/tests/misc/pp_bin_hex.ml
new file mode 100644
index 0000000000000000000000000000000000000000..41ab2e6ab92ee1beef120983f3e307461ada4811
--- /dev/null
+++ b/tests/misc/pp_bin_hex.ml
@@ -0,0 +1,37 @@
+let pp_dec fmt z = Integer.pretty ~hexa:false fmt z
+let pp_hex fmt z = Integer.pp_hex ~nbits:16 ~sep:"_" fmt z
+let pp_bin fmt z = Integer.pp_bin ~nbits:8 ~sep:"_" fmt z
+
+let hrule () =
+ Format.printf "--------------------------------------------------@."
+
+let testcase z =
+ begin
+ hrule () ;
+ Format.printf "Dec. %a@." pp_dec z ;
+ Format.printf "Hex. %a@." pp_hex z ;
+ Format.printf "Bin. %a@." pp_bin z ;
+ end
+
+let () =
+ begin
+ List.iter
+ (fun z ->
+ testcase z ;
+ if not (Integer.equal z Integer.zero) then
+ testcase (Integer.neg z)
+ ) [
+ Integer.of_string "0" ;
+ Integer.of_string "1" ;
+ Integer.of_string "2" ;
+ Integer.of_string "5" ;
+ Integer.of_string "9" ;
+ Integer.of_string "16" ;
+ Integer.of_string "127" ;
+ Integer.of_string "128" ;
+ Integer.of_string "0xFF" ;
+ Integer.of_string "0xFF0F000F" ;
+ Integer.of_string "0x17070007" ;
+ ] ;
+ hrule () ;
+ end
diff --git a/tests/misc/print_machdep.i b/tests/misc/print_machdep.i
index 80afbbd20f335c72d597dbc6c45cf6e37d304c37..0762669acd646cdbd6257081b52f420d15c7e2b2 100644
--- a/tests/misc/print_machdep.i
+++ b/tests/misc/print_machdep.i
@@ -1,4 +1,3 @@
/* run.config
- CMD: @frama-c@ -no-autoload-plugins
- OPT: -print-machdep
+ OPT: -no-autoload-plugins -print-machdep
*/