Skip to content

Commit

Permalink
Merge pull request #49 from goblint/int128
Browse files Browse the repository at this point in the history
add support for `__int128`, `__int128_t`, `__uint128_t`
  • Loading branch information
vogler authored Oct 12, 2021
2 parents 7a912dd + 5408ee7 commit c16dddf
Show file tree
Hide file tree
Showing 7 changed files with 73 additions and 18 deletions.
33 changes: 28 additions & 5 deletions src/cil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -293,6 +293,8 @@ and ikind =
| ILongLong (** [long long] (or [_int64] on Microsoft Visual C) *)
| IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft
Visual C) *)
| IInt128 (** [__int128] *)
| IUInt128 (** [unsigned __int128] *)

(** Various kinds of floating-point numbers*)
and fkind =
Expand Down Expand Up @@ -1310,13 +1312,15 @@ let isSigned = function
| IUShort
| IUInt
| IULong
| IULongLong ->
| IULongLong
| IUInt128 ->
false
| ISChar
| IShort
| IInt
| ILong
| ILongLong ->
| ILongLong
| IInt128 ->
true
| IChar ->
not !M.theMachine.M.char_is_unsigned
Expand Down Expand Up @@ -1705,6 +1709,8 @@ let d_ikind () = function
| IULongLong ->
if !msvcMode then text "unsigned __int64"
else text "unsigned long long"
| IInt128 -> text "__int128"
| IUInt128 -> text "unsigned __int128"

let d_fkind () = function
FFloat -> text "float"
Expand Down Expand Up @@ -1732,6 +1738,7 @@ let bytesSizeOfInt (ik: ikind): int =
| IShort | IUShort -> !M.theMachine.M.sizeof_short
| ILong | IULong -> !M.theMachine.M.sizeof_long
| ILongLong | IULongLong -> !M.theMachine.M.sizeof_longlong
| IInt128 | IUInt128 -> 16

(* constant *)
let d_const () c =
Expand All @@ -1747,7 +1754,12 @@ let d_const () c =
| IULong -> "UL"
| ILongLong -> if !msvcMode then "L" else "LL"
| IULongLong -> if !msvcMode then "UL" else "ULL"
(* if long long is 128 bit we can use its suffix, otherwise unsupported by GCC, see https://github.com/goblint/cil/issues/41#issuecomment-893291878 *)
| IInt128 when !M.theMachine.M.sizeof_longlong = 16 -> "LL"
| IUInt128 when !M.theMachine.M.sizeof_longlong = 16 -> "ULL"
| _ -> ""
(* TODO warn/fail? *)
(* E.s (E.bug "unknown/unsupported suffix") *)
in
let prefix : string =
if suffix <> "" then ""
Expand Down Expand Up @@ -2005,6 +2017,7 @@ let unsignedVersionOf (ik:ikind): ikind =
| IInt -> IUInt
| ILong -> IULong
| ILongLong -> IULongLong
| IInt128 -> IUInt128
| _ -> ik

let signedVersionOf (ik:ikind): ikind =
Expand All @@ -2014,6 +2027,7 @@ let signedVersionOf (ik:ikind): ikind =
| IUInt -> IInt
| IULong -> ILong
| IULongLong -> ILongLong
| IUInt128 -> IInt128
| _ -> ik

(* Return the integer conversion rank of an integer kind *)
Expand All @@ -2025,6 +2039,7 @@ let intRank (ik:ikind) : int =
| IInt | IUInt -> 3
| ILong | IULong -> 4
| ILongLong | IULongLong -> 5
| IInt128 | IUInt128 -> 6

(* Return the common integer kind of the two integer arguments, as
defined in ISO C 6.3.1.8 ("Usual arithmetic conversions") *)
Expand Down Expand Up @@ -2057,6 +2072,7 @@ let intKindForSize (s:int) (unsigned:bool) : ikind =
else if s = !M.theMachine.M.sizeof_long then IULong
else if s = !M.theMachine.M.sizeof_short then IUShort
else if s = !M.theMachine.M.sizeof_longlong then IULongLong
else if s = 16 then IUInt128
else raise Not_found
else
(* Test the most common sizes first *)
Expand All @@ -2065,6 +2081,7 @@ let intKindForSize (s:int) (unsigned:bool) : ikind =
else if s = !M.theMachine.M.sizeof_long then ILong
else if s = !M.theMachine.M.sizeof_short then IShort
else if s = !M.theMachine.M.sizeof_longlong then ILongLong
else if s = 16 then IInt128
else raise Not_found

let floatKindForSize (s:int) =
Expand Down Expand Up @@ -2142,13 +2159,15 @@ let intKindForValue (i: cilint) (unsigned: bool) =
else if fitsInInt IUShort i then IUShort
else if fitsInInt IUInt i then IUInt
else if fitsInInt IULong i then IULong
else IULongLong
else if fitsInInt IUInt128 i then IUInt128
else IULongLong (* warn, IUInt128? *)
else
if fitsInInt ISChar i then ISChar
else if fitsInInt IShort i then IShort
else if fitsInInt IInt i then IInt
else if fitsInInt ILong i then ILong
else ILongLong
else if fitsInInt IInt128 i then IInt128
else ILongLong (* warn, IInt128? *)

(** If the given expression is an integer constant or a CastE'd
integer constant, return that constant's value as an ikind, int64 pair.
Expand Down Expand Up @@ -2207,6 +2226,7 @@ let rec alignOf_int t =
| TInt((IInt|IUInt), _) -> !M.theMachine.M.alignof_int
| TInt((ILong|IULong), _) -> !M.theMachine.M.alignof_long
| TInt((ILongLong|IULongLong), _) -> !M.theMachine.M.alignof_longlong
| TInt((IInt128|IUInt128), _) -> 16 (* not generated since not all architectures support 128bit ints and the value should be the same for those that do *)
| TEnum(ei, _) -> alignOf_int (TInt(ei.ekind, []))
| TFloat(FFloat, _) -> !M.theMachine.M.alignof_float
| TFloat(FDouble, _) -> !M.theMachine.M.alignof_double
Expand Down Expand Up @@ -2839,7 +2859,7 @@ let parseInt (str: string) : exp =
(* The length of the suffix and a list of possible kinds. See ISO
* 6.4.4.1 *)
let hasSuffix = hasSuffix str in
let suffixlen, kinds =
let suffixlen, kinds = (* 128bit constants are only supported if long long is also 128bit, so we can parse those as long long *)
if hasSuffix "ULL" || hasSuffix "LLU" then
3, [IULongLong]
else if hasSuffix "LL" then
Expand Down Expand Up @@ -7025,6 +7045,8 @@ let initCIL () =
else if name = "unsigned short" then IUShort
else if name = "char" then IChar
else if name = "unsigned char" then IUChar
else if name = "__int128" then IInt128
else if name = "unsigned __int128" then IUInt128
else E.s(E.unimp "initCIL: cannot find the right ikind for type %s\n" name)
in
upointType := TInt(findIkindSz true !M.theMachine.M.sizeof_ptr, []);
Expand Down Expand Up @@ -7248,6 +7270,7 @@ let convertInts (i1:int64) (ik1:ikind) (i2:int64) (ik2:ikind)
| IInt | IUInt -> 3
| ILong | IULong -> 4
| ILongLong | IULongLong -> 5
| IInt128 | IUInt128 -> 6
in
let r1 = rank ik1 in
let r2 = rank ik2 in
Expand Down
2 changes: 2 additions & 0 deletions src/cil.mli
Original file line number Diff line number Diff line change
Expand Up @@ -287,6 +287,8 @@ and ikind =
| ILongLong (** [long long] (or [_int64] on Microsoft Visual C) *)
| IULongLong (** [unsigned long long] (or [unsigned _int64] on Microsoft
Visual C) *)
| IInt128 (** [__int128] *)
| IUInt128 (** [unsigned __int128] *)

(** Various kinds of floating-point numbers*)
and fkind =
Expand Down
5 changes: 5 additions & 0 deletions src/ciltools.ml
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ let ocaml_int_to_cil v n s =
let short_size = bitsSizeOf (TInt(IShort,[]))in
let long_size = bitsSizeOf longType in
let longlong_size = bitsSizeOf (TInt(ILongLong,[])) in
let int128_size = bitsSizeOf (TInt(IInt128,[])) in
let i =
match s with
Signed ->
Expand All @@ -72,6 +73,8 @@ let ocaml_int_to_cil v n s =
ILong
else if (n = longlong_size) then
ILongLong
else if (n = int128_size) then
IInt128
else
raise Weird_bitwidth
| Unsigned ->
Expand All @@ -85,6 +88,8 @@ let ocaml_int_to_cil v n s =
IULong
else if (n = longlong_size) then
IULongLong
else if (n = int128_size) then
IUInt128
else
raise Weird_bitwidth
in
Expand Down
11 changes: 10 additions & 1 deletion src/formatparse.mly
Original file line number Diff line number Diff line change
Expand Up @@ -238,7 +238,7 @@ type maybeInit =
%token EOF
%token CHAR INT DOUBLE FLOAT VOID INT64 INT32
%token ENUM STRUCT TYPEDEF UNION
%token SIGNED UNSIGNED LONG SHORT
%token SIGNED UNSIGNED LONG SHORT INT128
%token VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER

%token <string> ARG_e ARG_eo ARG_E ARG_u ARG_b ARG_t ARG_d ARG_lo ARG_l ARG_i
Expand Down Expand Up @@ -817,6 +817,15 @@ type_spec:
matchIntType IULongLong)
}

| INT128 { ((fun al args -> TInt(IInt128, al)),
matchIntType IInt128)
}
| UNSIGNED INT128 { ((fun al args -> TInt(IUInt128, al)),
matchIntType IUInt128)
}

| FLOAT { ((fun al args -> TFloat(FFloat, al)),
matchFloatType FFloat)
}
Expand Down
32 changes: 21 additions & 11 deletions src/frontc/cabs2cil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@ let interpret_character_constant char_list =
if value <= (Int64.of_int32 Int32.max_int) then
(CInt64(value,IULong,orig_rep)),(TInt(IULong,[]))
else
(CInt64(value,IULongLong,orig_rep)),(TInt(IULongLong,[]))
(CInt64(value,IULongLong,orig_rep)),(TInt(IULongLong,[])) (* 128bit constants are only supported if long long is also 128bit wide *)
end

(*** EXPRESSIONS *************)
Expand Down Expand Up @@ -743,11 +743,11 @@ let lookupTypeNoError (kind: string)
| _ -> raise Not_found

let lookupType (kind: string)
(n: string) : typ * location =
(n: string) : (typ * location) option =
try
lookupTypeNoError kind n
with Not_found ->
E.s (error "Cannot find type %s (kind:%s)" n kind)
Some (lookupTypeNoError kind n)
with Not_found -> None
(* E.s (error "Cannot find type %s (kind:%s)" n kind) *)

(* Create the self ref cell and add it to the map. Return also an indication
* if this is a new one. *)
Expand Down Expand Up @@ -2382,9 +2382,10 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
| A.Tlong -> 5
| A.Tint -> 6
| A.Tint64 -> 7
| A.Tfloat -> 8
| A.Tdouble -> 9
| _ -> 10 (* There should be at most one of the others *)
| A.Tint128 -> 8
| A.Tfloat -> 9
| A.Tdouble -> 10
| _ -> 11 (* There should be at most one of the others *)
in
List.stable_sort (fun ts1 ts2 -> compare (order ts1) (order ts2)) tspecs'
in
Expand Down Expand Up @@ -2451,6 +2452,11 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of

| [A.Tunsigned; A.Tint64] -> TInt(IULongLong, [])

| [A.Tint128]
| [A.Tsigned; A.Tint128] -> TInt(IInt128, [])

| [A.Tunsigned; A.Tint128] -> TInt(IUInt128, [])

| [A.Tfloat] -> TFloat(FFloat, [])
| [A.Tdouble] -> TFloat(FDouble, [])

Expand All @@ -2465,8 +2471,12 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
end else
let t =
match lookupType "type" n with
(TNamed _) as x, _ -> x
| typ -> E.s (error "Named type %s is not mapped correctly" n)
| Some (TNamed _ as x, _) -> x
| _ ->
match n with
| "__int128_t" -> TInt(IInt128, [])
| "__uint128_t" -> TInt(IUInt128, [])
| _ -> E.s (error "Named type %s is not mapped correctly" n)
in
t
end
Expand Down Expand Up @@ -2548,7 +2558,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
else if fitsInInt ILong i then ILong
else if fitsInInt IULong i then IULong
else if fitsInInt ILongLong i then ILongLong
else IULongLong
else IULongLong (* assume there can be not enum constants that don't fit in long long since there can only be 128bit constants if long long is also 128bit *)
in
(* as each name,value pair is determined, this is called *)
let rec processName kname (i: exp) loc rest = begin
Expand Down
3 changes: 3 additions & 0 deletions src/frontc/clexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -279,6 +279,9 @@ let init ~(filename: string) : Lexing.lexbuf =
init_lexicon ();
(* Inititialize the pointer in Errormsg *)
Lexerhack.add_type := add_type;
(* add some built-in types which are handled as Tnamed in cabs2cil *)
add_type "__int128_t"; (* __int128 *)
add_type "__uint128_t"; (* unsigned __int128 *)
Lexerhack.push_context := push_context;
Lexerhack.pop_context := pop_context;
Lexerhack.add_identifier := add_identifier;
Expand Down
5 changes: 4 additions & 1 deletion src/frontc/frontc.ml
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,7 @@ and parse_to_cabs_inner (fname : string) =
try
if !E.verboseFlag then ignore (E.log "Frontc is parsing %s\n" fname);
flush !E.logChannel;
(* if !E.verboseFlag then ignore @@ Parsing.set_trace true; *)
let lexbuf = Clexer.init ~filename:fname in
let cabs = Stats.time "parse" (Cparser.interpret (Whitetrack.wraplexer clexer)) lexbuf in
Whitetrack.setFinalWhite (Clexer.get_white ());
Expand All @@ -202,7 +203,9 @@ and parse_to_cabs_inner (fname : string) =
ignore (E.log "Parsing error");
Clexer.finish ();
close_output ();
raise (ParseError("Parse error"))
(* raise (ParseError("Parse error")) *)
let backtrace = Printexc.get_raw_backtrace () in
Printexc.raise_with_backtrace (ParseError("Parse error")) backtrace (* re-raise with captured inner backtrace *)
end
| e -> begin
ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e));
Expand Down

0 comments on commit c16dddf

Please sign in to comment.