Skip to content

Commit 6026339

Browse files
mtzguidomtzguido
authored
Merge pull request #4189 from mtzguido/ints
PrintML: nicer integer literals
2 parents 981fc15 + ab49715 commit 6026339

14 files changed

Lines changed: 164 additions & 99 deletions

‎pulse/test/Defer.ml.expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
open Prims
22
let rec without_defer (x : Prims.bool) : unit=
33
let _return = Pulse_Lib_Reference.alloc () false in
4-
let v = Pulse_Lib_Vec.alloc 1 (Stdint.Uint64.of_int (10)) in
4+
let v = Pulse_Lib_Vec.alloc 1 (Stdint.Uint64.of_int 10) in
55
if x
66
then (Pulse_Lib_Vec.free v (); Pulse_Lib_Reference.write _return true)
77
else ();
88
(let _return1 = Pulse_Lib_Reference.read _return () () in
99
if _return1 then () else Pulse_Lib_Vec.free v ())
1010
let rec with_defer (x : Prims.bool) : unit=
1111
let _return = Pulse_Lib_Reference.alloc () false in
12-
let v = Pulse_Lib_Vec.alloc 1 (Stdint.Uint64.of_int (10)) in
12+
let v = Pulse_Lib_Vec.alloc 1 (Stdint.Uint64.of_int 10) in
1313
if x then Pulse_Lib_Reference.write _return true else ();
1414
Pulse_Lib_Vec.free v ()

‎pulse/test/ExtractionTest.ml.expected‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,13 @@ let rec test_read_write (x : FStar_UInt32.t Pulse_Lib_Reference.ref)
88
Pulse_Lib_Reference.write x (FStar_UInt32.add n Stdint.Uint32.zero)
99
let rec test_write_10 (x : FStar_UInt32.t Pulse_Lib_Reference.ref)
1010
(_'n : unit) : unit=
11-
Pulse_Lib_Reference.write x (Stdint.Uint32.of_int (2));
11+
Pulse_Lib_Reference.write x (Stdint.Uint32.of_int 2);
1212
test_read_write x ();
1313
Pulse_Lib_Reference.write x Stdint.Uint32.zero
1414
let rec test_inner_ghost_fun (uu___ : unit) : unit= ()
1515
let rec write10 (x : FStar_UInt32.t Pulse_Lib_Reference.ref) (_'n : unit) :
1616
unit=
17-
let ctr = Pulse_Lib_Reference.alloc () (Stdint.Uint32.of_int (10)) in
17+
let ctr = Pulse_Lib_Reference.alloc () (Stdint.Uint32.of_int 10) in
1818
Pulse_Lib_Dv.while_
1919
(fun while_cond ->
2020
let __anf0 = Pulse_Lib_Reference.read ctr () () in
@@ -40,7 +40,7 @@ let rec fill_array (x : FStar_UInt32.t Pulse_Lib_Array_Core.array)
4040
let rec sub_array (x : FStar_UInt32.t Pulse_Lib_Array_Core.array) : unit=
4141
let __anf0 = Pulse_Lib_Array_Core.sub x () () Stdint.Uint64.one () () in
4242
Pulse_Lib_Array_Core.mask_write __anf0 Stdint.Uint64.zero
43-
(Stdint.Uint32.of_int (42)) () ()
43+
(Stdint.Uint32.of_int 42) () ()
4444
let test0 (x : FStar_SizeT.t) (y : FStar_SizeT.t) : FStar_SizeT.t=
4545
FStar_SizeT.rem x y
4646
type 'a opt =
@@ -53,11 +53,9 @@ let uu___is_Some (projectee : 'a opt) : Prims.bool=
5353
let __proj__Some__item__v (projectee : 'a opt) : 'a=
5454
match projectee with | Some v -> v
5555
let my_safe_add (x : FStar_SizeT.t) (y : FStar_SizeT.t) : FStar_SizeT.t opt=
56-
if FStar_SizeT.lte x (Stdint.Uint64.of_string "0xffff")
56+
if FStar_SizeT.lte x (Stdint.Uint64.of_int 0xffff)
5757
then
58-
(if
59-
FStar_SizeT.lte y
60-
(FStar_SizeT.sub (Stdint.Uint64.of_string "0xffff") x)
58+
(if FStar_SizeT.lte y (FStar_SizeT.sub (Stdint.Uint64.of_int 0xffff) x)
6159
then Some (FStar_SizeT.add x y)
6260
else None)
6361
else None
@@ -72,7 +70,7 @@ let rec fib (x : Prims.nat) : Prims.nat=
7270
then Prims.int_one
7371
else
7472
(let x1 = fib (x - Prims.int_one) in
75-
let x2 = fib (x - (Prims.of_int (2))) in x1 + x2)
73+
let x2 = fib (x - (Prims.of_int 2)) in x1 + x2)
7674
let rec fib2 (x : Prims.nat) : Prims.nat=
7775
let n = fib x in let m = fib (x + Prims.int_one) in m + n
7876
type ('a, 'b) data =

‎pulse/test/InlineArrayLen.ml.expected‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,31 @@
11
open Prims
22
let rec basic (uu___ : unit) : FStar_Int32.t=
33
let arr =
4-
Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int (123))
5-
(Stdint.Uint64.of_int (2)) in
4+
Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int 123)
5+
(Stdint.Uint64.of_int 2) in
66
Pulse_Lib_Array_Core.mask_read arr Stdint.Uint64.zero () () ()
77
let rec use (uu___ : unit) : FStar_Int32.t=
88
let arr =
9-
Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int (123))
10-
(Stdint.Uint64.of_int (2)) in
9+
Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int 123)
10+
(Stdint.Uint64.of_int 2) in
1111
Pulse_Lib_Array_Core.mask_read arr Stdint.Uint64.zero () () ()
1212
let rec use_gen_init (uu___ : unit) : FStar_Int32.t=
1313
let arr =
14-
Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int (123))
15-
(Stdint.Uint64.of_int (2)) in
14+
Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int 123)
15+
(Stdint.Uint64.of_int 2) in
1616
Pulse_Lib_Array_Core.mask_read arr Stdint.Uint64.zero () () ()
1717
let rec use_gen_init_st (uu___ : unit) : FStar_Int32.t=
18-
let init uu___1 uu___2 = (Stdint.Int32.of_int (123)) in
18+
let init uu___1 uu___2 = Stdint.Int32.of_int 123 in
1919
let __anf0 = init () () in
20-
let arr = Pulse_Lib_Array_PtsTo.alloc () __anf0 (Stdint.Uint64.of_int (2)) in
20+
let arr = Pulse_Lib_Array_PtsTo.alloc () __anf0 (Stdint.Uint64.of_int 2) in
2121
Pulse_Lib_Array_Core.mask_read arr Stdint.Uint64.zero () () ()
2222
let rec use_gen_len (uu___ : unit) : FStar_Int32.t=
2323
let arr =
24-
Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int (123))
25-
(Stdint.Uint64.of_int (2)) in
24+
Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int 123)
25+
(Stdint.Uint64.of_int 2) in
2626
Pulse_Lib_Array_Core.mask_read arr Stdint.Uint64.zero () () ()
2727
let rec use_gen_len_st (uu___ : unit) : FStar_Int32.t=
28-
let len uu___1 uu___2 = (Stdint.Uint64.of_int (42)) in
28+
let len uu___1 uu___2 = Stdint.Uint64.of_int 42 in
2929
let __anf0 = len () () in
30-
let arr = Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int (123)) __anf0 in
30+
let arr = Pulse_Lib_Array_PtsTo.alloc () (Stdint.Int32.of_int 123) __anf0 in
3131
Pulse_Lib_Array_Core.mask_read arr Stdint.Uint64.zero () () ()

‎src/ml/FStarC_Extraction_ML_PrintML.ml‎

Lines changed: 50 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -97,22 +97,21 @@ let try_with_idents : Longident.t Asttypes.loc list = [
9797
]
9898
let is_try_with_ident x = List.exists (fun tw -> x = tw) try_with_idents
9999

100-
(* For integer constants (not 0/1) in this range we will use Prims.of_int
101-
* Outside this range we will use string parsing to allow arbitrary sized
102-
* integers.
103-
* Using int_zero/int_one removes int processing to create the int
104-
* Using of_int removes string processing to create the int
105-
*)
106-
let max_of_int_const = Z.of_int 65535
107-
let min_of_int_const = Z.of_int (-65536)
100+
(* For integer constants outside of this range we will use Prims.parse_int,
101+
* to allow for arbitrary sized integers.
102+
* For small integers, we prefer using of_int to avoid string parsing.
103+
* OCaml guarantees a minimum width of 31 ( *not* 32), so we can generate
104+
* literals safely for anything in [-2^30, 2^30 - 1]. *)
105+
let min_of_int_const = Z.neg (Z.pow (Z.of_int 2) 30)
106+
let max_of_int_const = Z.sub (Z.pow (Z.of_int 2) 30) Z.one
108107

109108
let maybe_guts (s:string) : string =
110109
if FStarC_Options.codegen () = Some FStarC_Options.Plugin
111110
then "Fstarcompiler." ^ s
112111
else s
113112

114113
(* mapping functions from F* ML AST to Parsetree *)
115-
let build_constant (c: mlconstant): constant =
114+
let build_constant_expr (c: mlconstant) : expression =
116115
let stdint_module (s:FStarC_Const.signedness) (w:FStarC_Const.width) : string =
117116
let sign = match s with
118117
| FStarC_Const.Signed -> "Int"
@@ -123,53 +122,60 @@ let build_constant (c: mlconstant): constant =
123122
| FStarC_Const.Int16 -> with_w "16"
124123
| FStarC_Const.Int32 -> with_w "32"
125124
| FStarC_Const.Int64 -> with_w "64"
126-
| FStarC_Const.Sizet -> with_w "64" in
127-
match c with
128-
| MLC_Int (v, None) ->
129-
let s = match Z.of_string v with
130-
| x when x = Z.zero ->
131-
maybe_guts "Prims.int_zero"
132-
| x when x = Z.one ->
133-
maybe_guts "Prims.int_one"
134-
| x when (min_of_int_const < x) && (x < max_of_int_const) ->
135-
BatString.concat v ["(Prims.of_int ("; "))"]
136-
| x ->
137-
BatString.concat v ["(Prims.parse_int \""; "\")"] in
138-
Pconst_integer (s, None)
139-
(* Special case for UInt8, as it's realized as OCaml built-in int type *)
140-
| MLC_Int (v, Some (FStarC_Const.Unsigned, FStarC_Const.Int8)) ->
141-
Pconst_integer (v, None)
142-
| MLC_Int (v, Some (s, w)) ->
143-
let s = match Z.of_string v with
144-
| x when x = Z.zero ->
145-
BatString.concat "" [stdint_module s w; ".zero"]
146-
| x when x = Z.one ->
147-
BatString.concat "" [stdint_module s w; ".one"]
148-
| x when (min_of_int_const < x) && (x < max_of_int_const) ->
149-
BatString.concat "" ["("; stdint_module s w; ".of_int ("; v; "))"]
150-
| x ->
151-
BatString.concat "" ["("; stdint_module s w; ".of_string \""; v; "\")"] in
152-
Pconst_integer (s, None)
153-
| MLC_Float v -> Pconst_float (string_of_float v, None)
154-
| MLC_Char v -> Pconst_integer (string_of_int v, None)
155-
| MLC_String v -> Pconst_string (v, no_location, None)
156-
| _ -> failwith "Case not handled"
157-
158-
let build_constant_expr (c: mlconstant): expression =
125+
| FStarC_Const.Sizet -> with_w "64"
126+
in
159127
match c with
160128
| MLC_Unit -> pexp_construct ~loc (mk_lident "()") None
161129
| MLC_Bool b ->
162130
let id = if b then "true" else "false" in
163131
pexp_construct ~loc (mk_lident id) None
164-
| _ -> pexp_constant ~loc (build_constant c)
132+
(* Special case for UInt8, as it's realized as OCaml built-in int type *)
133+
| MLC_Int (v, Some (FStarC_Const.Unsigned, FStarC_Const.Int8)) ->
134+
pexp_constant ~loc @@ Pconst_integer (v, None)
135+
| MLC_Int (v, None) -> (
136+
(* Prims integers *)
137+
match Z.of_string v with
138+
| x when x = Z.zero -> pexp_ident ~loc (mk_lident "Prims.int_zero")
139+
| x when x = Z.one -> pexp_ident ~loc (mk_lident "Prims.int_one")
140+
| x when min_of_int_const <= x && x <= max_of_int_const ->
141+
let r = pexp_ident ~loc (mk_lident "Prims.of_int") in
142+
let n = pexp_constant ~loc (Pconst_integer (v, None)) in
143+
pexp_apply ~loc r [(Nolabel, n)]
144+
| x ->
145+
let r = pexp_ident ~loc (mk_lident "Prims.parse_int") in
146+
let n = pexp_constant ~loc (Pconst_string (v, no_location, None)) in
147+
pexp_apply ~loc r [(Nolabel, n)]
148+
)
149+
| MLC_Int (v, Some (s, w)) -> (
150+
(* Machine integers. *)
151+
match Z.of_string v with
152+
| x when x = Z.zero -> pexp_ident ~loc @@ mk_lident (stdint_module s w ^ ".zero")
153+
| x when x = Z.one -> pexp_ident ~loc @@ mk_lident (stdint_module s w ^ ".one")
154+
| x when min_of_int_const <= x && x <= max_of_int_const ->
155+
let r = pexp_ident ~loc @@ mk_lident (stdint_module s w ^ ".of_int") in
156+
let n = pexp_constant ~loc (Pconst_integer (v, None)) in
157+
pexp_apply ~loc r [(Nolabel, n)]
158+
| x ->
159+
let r = pexp_ident ~loc @@ mk_lident (stdint_module s w ^ ".of_string") in
160+
let n = pexp_constant ~loc (Pconst_string (v, no_location, None)) in
161+
pexp_apply ~loc r [(Nolabel, n)]
162+
)
163+
| MLC_Float v -> pexp_constant ~loc @@ Pconst_float (string_of_float v, None)
164+
| MLC_Char v -> pexp_constant ~loc @@ Pconst_integer (string_of_int v, None)
165+
| MLC_String v -> pexp_constant ~loc @@ Pconst_string (v, no_location, None)
166+
| _ -> failwith "Case not handled"
165167

166168
let build_constant_pat (c: mlconstant): pattern =
167169
match c with
168170
| MLC_Unit -> ppat_construct ~loc (mk_lident "()") None
169171
| MLC_Bool b ->
170172
let id = if b then "true" else "false" in
171173
ppat_construct ~loc (mk_lident id) None
172-
| _ -> ppat_constant ~loc (build_constant c)
174+
| MLC_Float v -> ppat_constant ~loc @@ Pconst_float (string_of_float v, None)
175+
| MLC_Char v -> ppat_constant ~loc @@ Pconst_integer (string_of_int v, None)
176+
| MLC_String v -> ppat_constant ~loc @@ Pconst_string (v, no_location, None)
177+
| MLC_Int _ ->
178+
failwith "PrintML: unexpected integer pattern, should have become a pattern guard"
173179

174180
let rec build_pattern (p: mlpattern): pattern =
175181
match p with

‎tests/bug-reports/closed/Bug2699.ml.expected‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
open Prims
22
let broken_length_f32 : (FStar_UInt32.t * FStar_UInt32.t)=
3-
((FStar_UInt32.uint_to_t (Prims.of_int (24))),
4-
(FStar_UInt32.uint_to_t (Prims.of_int (28))))
3+
((FStar_UInt32.uint_to_t (Prims.of_int 24)),
4+
(FStar_UInt32.uint_to_t (Prims.of_int 28)))
55
let works_length_f32 : (FStar_UInt32.t * FStar_UInt32.t)=
6-
((FStar_UInt32.uint_to_t (Prims.of_int (24))),
7-
(FStar_UInt32.uint_to_t (Prims.of_int (28))))
6+
((FStar_UInt32.uint_to_t (Prims.of_int 24)),
7+
(FStar_UInt32.uint_to_t (Prims.of_int 28)))

‎tests/bug-reports/closed/Bug310.ml.expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
open Prims
22
type ('a, 'a1) capture = ('a1 * 'a)
33
let struct1 : Prims.int= Prims.int_one
4-
let struct11 : Prims.int= (Prims.of_int (2))
4+
let struct11 : Prims.int= Prims.of_int 2
55
let test : (Prims.int * Prims.int)=
6-
let x = Prims.int_zero in let x1 = (Prims.of_int (2)) in (x, x1)
6+
let x = Prims.int_zero in let x1 = Prims.of_int 2 in (x, x1)
77
let r (uu___ : unit) (uu___1 : unit) (uu___2 : Obj.t -> Obj.t) : Prims.int=
88
Prims.int_zero
99
let g (uu___ : Prims.int) (uu___1 : Prims.int) : Prims.int= Prims.int_zero

‎tests/bug-reports/closed/Bug3865.ml.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,6 @@ let intpak : pak=
1111
f = (fun x -> let x = Obj.magic x in Obj.magic (x + Prims.int_one))
1212
}
1313
let use : unit=
14-
let x = intpak.f (Obj.magic (Prims.of_int (123))) in
14+
let x = intpak.f (Obj.magic (Prims.of_int 123)) in
1515
FStar_IO.print_string
1616
(Prims.strcat (Prims.string_of_int (Obj.magic x)) "\n")

‎tests/extraction/ExtractAs.ml.expected‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
open Prims
22
let fail_unless (b : Prims.bool) : Prims.string=
33
if b then "ok" else Prims.magic ()
4-
let rec frob (x : Prims.nat) : Prims.int= x + (Prims.of_int (10))
4+
let rec frob (x : Prims.nat) : Prims.int= x + (Prims.of_int 10)
55
let uu___0 : Prims.string=
6-
fail_unless ((frob Prims.int_one) = (Prims.of_int (11)))
7-
let bar (z : Prims.int) : Prims.int= z + (Prims.of_int (10))
6+
fail_unless ((frob Prims.int_one) = (Prims.of_int 11))
7+
let bar (z : Prims.int) : Prims.int= z + (Prims.of_int 10)
88
let uu___1 : Prims.string=
9-
fail_unless ((bar Prims.int_one) = (Prims.of_int (11)))
9+
fail_unless ((bar Prims.int_one) = (Prims.of_int 11))
1010
let rec loopid (x : Prims.nat) : Prims.nat= x
11-
let two : Prims.nat= loopid (Prims.of_int (2))
11+
let two : Prims.nat= loopid (Prims.of_int 2)

‎tests/extraction/Ints.fst‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
module Ints
2+
3+
module U32 = FStar.UInt32
4+
module I16 = FStar.Int16
5+
6+
let test1 (x : int) : int =
7+
match x with
8+
| 0 -> -1
9+
| 123 -> 321
10+
| 999999 -> 888888
11+
| x -> x-1
12+
13+
let test2 (x : U32.t) : U32.t =
14+
match x with
15+
| 0ul -> 1ul
16+
| 123ul -> 321ul
17+
| 999999ul -> 888888ul
18+
| x -> U32.sub x 1ul
19+
20+
let test3 (x : I16.t) : I16.t =
21+
match x with
22+
| 0s -> -1s
23+
| 123s -> 321s
24+
| 999s -> 888s
25+
| x -> x
26+
27+
(* Literals OK *)
28+
let _ = -1073741824 (* 2^30 *)
29+
let _ = -1073741823 (* 2^30 - 1*)
30+
let _ = 1073741823 (* 2^30 - 1*)
31+
32+
(* Should be strings. *)
33+
let _ = -1073741825 (* 2^30 + 1*)
34+
let _ = 1073741824 (* 2^30 *)
35+
let _ = 1073741825 (* 2^30 + 1*)

‎tests/extraction/Ints.ml.expected‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
open Prims
2+
let test1 (x : Prims.int) : Prims.int=
3+
match x with
4+
| uu___ when uu___ = Prims.int_zero -> Prims.of_int (-1)
5+
| uu___ when uu___ = (Prims.of_int 123) -> Prims.of_int 321
6+
| uu___ when uu___ = (Prims.of_int 999999) -> Prims.of_int 888888
7+
| x1 -> x1 - Prims.int_one
8+
let test2 (x : FStar_UInt32.t) : FStar_UInt32.t=
9+
match x with
10+
| uu___ when uu___ = Stdint.Uint32.zero -> Stdint.Uint32.one
11+
| uu___ when uu___ = (Stdint.Uint32.of_int 123) -> Stdint.Uint32.of_int 321
12+
| uu___ when uu___ = (Stdint.Uint32.of_int 999999) ->
13+
Stdint.Uint32.of_int 888888
14+
| x1 -> FStar_UInt32.sub x1 Stdint.Uint32.one
15+
let test3 (x : FStar_Int16.t) : FStar_Int16.t=
16+
match x with
17+
| uu___ when uu___ = Stdint.Int16.zero -> Stdint.Int16.of_int (-1)
18+
| uu___ when uu___ = (Stdint.Int16.of_int 123) -> Stdint.Int16.of_int 321
19+
| uu___ when uu___ = (Stdint.Int16.of_int 999) -> Stdint.Int16.of_int 888
20+
| x1 -> x1
21+
let uu___0 : Prims.int= Prims.of_int (-1073741824)
22+
let uu___1 : Prims.int= Prims.of_int (-1073741823)
23+
let uu___2 : Prims.int= Prims.of_int 1073741823
24+
let uu___3 : Prims.int= Prims.parse_int "-1073741825"
25+
let uu___4 : Prims.int= Prims.parse_int "1073741824"
26+
let uu___5 : Prims.int= Prims.parse_int "1073741825"

0 commit comments

Comments
 (0)