Skip to content

Commit e31a36d

Browse files
committed
Fix a bug in parsing 0x<num1>e<num2>
The parser was previously accepting `e` and `E` as an exponent character in hex strings. This results in enormous exponentiation, so we disallow it. Tracked down from the report at https://coq.zulipchat.com/#narrow/stream/247791-fiat-crypto/topic/ECDSA/near/223249990
1 parent c86d501 commit e31a36d

File tree

1 file changed

+21
-9
lines changed

1 file changed

+21
-9
lines changed

src/Util/Strings/ParseArithmetic.v

Lines changed: 21 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,10 @@ Definition parse_oct_prefix : ParserAction _ := "0o".
4646
Definition parse_dec_prefix : ParserAction _ := "".
4747
Definition parse_hex_prefix : ParserAction _ := "0x".
4848

49+
(** Is [E]/[e] a valid digit in the given base? *)
50+
Definition base_accepts_E (base : N) : bool
51+
:= (10 + N_of_ascii "E" - N_of_ascii "A" <? base)%N.
52+
4953
Definition parse_digits_gen_step (base : N) : ParserAction N
5054
:= (parse_strs
5155
(List.flat_map
@@ -81,7 +85,17 @@ Local Coercion Z.of_N : N >-> Z.
8185
Local Coercion inject_Z : Z >-> Q.
8286

8387
Definition parse_num_gen (allow_neg : bool) {P} (base : N) (parse_prefix : ParserAction P) : ParserAction Q
84-
:= (if allow_neg then ((strip_whitespace_around "-")?) else parse_map (fun _ => None) "")
88+
:= let parse_E_exponent
89+
:= (("e" || "E") ;;->{ fun _ v => Qpower 10 v }
90+
(((strip_whitespace_around "-")?)
91+
;;->{ fun n v => if n:option _ then (-v)%Z else v }
92+
(parse_map (digits_to_N base : _ -> Z) ((parse_digits_gen_step base)+) )))%parse in
93+
let parse_P_exponent
94+
:= (("p" || "P") ;;->{ fun _ v => Qpower 2 v }
95+
(((strip_whitespace_around "-")?)
96+
;;->{ fun n v => if n:option _ then (-v)%Z else v }
97+
(parse_map (digits_to_N base : _ -> Z) ((parse_digits_gen_step base)+) )))%parse in
98+
(if allow_neg then ((strip_whitespace_around "-")?) else parse_map (fun _ => None) "")
8599
;;->{ fun n v => if n:option _ then (-v)%Q else v }
86100
parse_prefix ;;->{ fun _ v => v }
87101
((((parse_digits_gen_step base)* )
@@ -92,14 +106,9 @@ Definition parse_num_gen (allow_neg : bool) {P} (base : N) (parse_prefix : Parse
92106
(parse_digits_gen_step base)* )
93107
|| parse_map (digits_to_N base : _ -> Q) ((parse_digits_gen_step base)+))
94108
;;->{ fun n e => match e with Some e => n * e | None => n end%Q }
95-
(((("e" || "E") ;;->{ fun _ v => Qpower 10 v }
96-
(((strip_whitespace_around "-")?)
97-
;;->{ fun n v => if n:option _ then (-v)%Z else v }
98-
(parse_map (digits_to_N base : _ -> Z) ((parse_digits_gen_step base)+) )))
99-
|| (("p" || "P") ;;->{ fun _ v => Qpower 2 v }
100-
(((strip_whitespace_around "-")?)
101-
;;->{ fun n v => if n:option _ then (-v)%Z else v }
102-
(parse_map (digits_to_N base : _ -> Z) ((parse_digits_gen_step base)+) ))))?).
109+
((if base_accepts_E base
110+
then parse_P_exponent (* if [e] is a valid character in the base, then we don't permit [e] as an exponent *)
111+
else (parse_E_exponent || parse_P_exponent))?).
103112

104113
Definition parse_num (allow_neg : bool) : ParserAction Q
105114
:= parse_num_gen allow_neg 2 parse_bin_prefix
@@ -112,6 +121,9 @@ Redirect "log" Check let ls := [("-1234", -(1234):Q); ("0xF", 15:Q); ("10.5", (1
112121
: List.map (fun '(s, v) => ((parse_num true;;->{fun v _ => v} ε)%parse s )) ls
113122
= List.map (fun '(s, v) => [(v, "")]) ls.
114123

124+
(* This was previously stack overflowing due to treating [e] as an exponent *)
125+
Redirect "log" Compute parse_num false "0xffffffff00000000ffffffffffffffffbce6faada7179e84f3b9cac2fc632551".
126+
115127
Inductive Qexpr := Qv (_ : Q) | Qeopp (a : Qexpr) | Qeadd (a b : Qexpr) | Qesub (a b : Qexpr) | Qemul (a b : Qexpr) | Qediv (a b : Qexpr) | Qepow (b e : Qexpr).
116128
Coercion Qv : Q >-> Qexpr.
117129
Delimit Scope Qexpr_scope with Qexpr.

0 commit comments

Comments
 (0)