gil_parser: add BV literals

GillianCore/GIL_Syntax/Literal.ml

@@ -28,6 +28,7 @@ let rec equal la lb =
   | String sl, String sr | Loc sl, Loc sr -> String.equal sl sr
   | Type tl, Type tr -> Type.equal tl tr
   | LList ll, LList lr -> List.for_all2 equal ll lr
+  | LBitvector (vl, wl), LBitvector (vr, wr) -> Z.equal vl vr && Int.equal wl wr
   | _ -> false
 
 let to_yojson = TypeDef__.literal_to_yojson
@@ -48,7 +49,7 @@ let rec pp fmt x =
   | Loc loc -> Fmt.string fmt loc
   | Type t -> Fmt.string fmt (Type.str t)
   | LList ll -> Fmt.pf fmt "{{ %a }}" (Fmt.list ~sep:Fmt.comma pp) ll
-  | LBitvector (v, w) -> Fmt.pf fmt "%ab%d" Z.pp_print v w
+  | LBitvector (v, w) -> Fmt.pf fmt "0x%sv%d" (Z.format "%x" v) w
 
 (** Typing *)
 let type_of (x : t) : Type.t =

GillianCore/gil_parser/GIL_Lexer.mll

@@ -146,11 +146,13 @@
 }
 
 let digit = ['0'-'9']
+let hexdigit = ['0'-'9''a'-'f''A'-'F']
 let letter = ['a'-'z''A'-'Z']
 let identifier = letter(letter|digit|'_')*
 
 let float = '-'? digit+ ('.' digit*)?
 let int = '-'? digit+ 'i'
+let bv = "0x" hexdigit+ 'v' digit+
 
 let var2 = "_pvar_" (letter|digit|'_')*
 let lvar = '#' (letter|digit|'_'|'$')*
@@ -312,6 +314,11 @@ rule read = parse
                            let s_n = String.sub s 0 ((String.length s) - 1) in
                            let n = Z.of_string s_n in
                            GIL_Parser.INTEGER n }
+  | bv                   { let s = Lexing.lexeme lexbuf in
+                           let l = String.split_on_char 'v' s in
+                           let n = Z.of_string (List.nth l 0) in
+                           let w = int_of_string (List.nth l 1) in
+                           GIL_Parser.BITVECTOR (n, w) }
   | float                { let n = float_of_string (Lexing.lexeme lexbuf) in
                            GIL_Parser.FLOAT n }
   | '"'                  { read_string (Buffer.create 32) lexbuf }

GillianCore/gil_parser/GIL_Parser.mly

@@ -69,6 +69,7 @@ let normalised_lvar_r = Str.regexp "##NORMALISED_LVAR"
 %token FALSE
 %token <float> FLOAT
 %token <Z.t> INTEGER
+%token <Z.t * int> BITVECTOR
 %token NAN
 %token INFINITY
 %token <string> STRING
@@ -1224,6 +1225,7 @@ lit_target:
   | FALSE                     { Literal.Bool false }
   | FLOAT                     { Literal.Num $1 }
   | n = INTEGER               { Literal.Int n }
+  | t = BITVECTOR             { Literal.LBitvector t }
   | NAN                       { Literal.Num nan }
   | INFINITY                  { Literal.Num infinity }
   | STRING                    { Literal.String $1 }