From 366129663b9c164822a733fd73c2361662ec7247 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 28 Jan 2025 15:55:41 +0100
Subject: [PATCH] [kernel] Fix typing of types in builtins
The builtins `__builtin_types_compatible_p` and `__builtin_va_arg` need
a type as argument. Frama-C converts them to an expression to be able to
type the builtin call.
This commit change the conversion in `cparser.mly` from a sizeof on the
type to a cast with a marker indicating from which builtin the argument
is coming from. This allows `cabs2cil` to type this expression
differently than a regular cast or sizeof.
---
src/kernel_internals/parsing/cparser.mly | 24 ++++++++++++-----
src/kernel_internals/typing/cabs2cil.ml | 26 +++++++++++++++++++
.../ast_printing/cil_printer.ml | 2 +-
3 files changed, 45 insertions(+), 7 deletions(-)
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 653febf25e..16b088b68f 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -313,6 +313,15 @@ let in_ghost_block ?(battrs=[]) l =
get_statementloc (List.hd l),
get_statementloc (Extlib.last l)))
+let type_to_expr_for_builtin ~loc ~builtin specifier decl_type =
+ (* Prefix the builtin name with __fc_ to avoid collisions with real
+ world code. *)
+ let builtin = "__fc_" ^ builtin in
+ (* Build an expression representing the given type with a marker to indicate
+ the builtin for which this translation was made. *)
+ let info = SINGLE_INIT { expr_loc = loc; expr_node = VARIABLE builtin } in
+ { expr_loc = loc; expr_node = CAST ((specifier, decl_type), info) }
+
%}
%token <Filepath.position * string> SPEC
@@ -551,28 +560,31 @@ postfix_expression: /*(* 6.5.2 *)*/
| postfix_expression LPAREN arguments RPAREN ghost_arguments_opt
{ make_expr $sloc (CALL ($1, $3, $5))}
| BUILTIN_VA_ARG LPAREN expression COMMA type_name RPAREN {
+ let builtin = "__builtin_va_arg" in
let b, d = $5 in
let loc = Cil_datatype.Location.of_lexing_loc $loc($5) in
let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in
+ let type_as_expr = type_to_expr_for_builtin ~loc ~builtin b d in
make_expr $sloc
(CALL
({ expr_loc = loc_f;
- expr_node = VARIABLE "__builtin_va_arg"},
- [$3; { expr_loc = loc;
- expr_node = TYPE_SIZEOF (b, d)}],[]))
+ expr_node = VARIABLE builtin},
+ [$3; type_as_expr],[]))
}
| BUILTIN_TYPES_COMPAT LPAREN type_name COMMA type_name RPAREN {
+ let builtin = "__builtin_types_compatible_p" in
let b1,d1 = $3 in
let b2,d2 = $5 in
let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in
let loc1 = Cil_datatype.Location.of_lexing_loc $loc($3) in
let loc2 = Cil_datatype.Location.of_lexing_loc $loc($5) in
+ let type_as_expr1 = type_to_expr_for_builtin ~loc:loc1 ~builtin b1 d1 in
+ let type_as_expr2 = type_to_expr_for_builtin ~loc:loc2 ~builtin b2 d2 in
make_expr $sloc
(CALL
({expr_loc = loc_f;
- expr_node = VARIABLE "__builtin_types_compatible_p"},
- [ { expr_loc = loc1; expr_node = TYPE_SIZEOF(b1,d1)};
- { expr_loc = loc2; expr_node = TYPE_SIZEOF(b2,d2)}],[]))
+ expr_node = VARIABLE builtin},
+ [ type_as_expr1; type_as_expr2],[]))
}
| BUILTIN_OFFSETOF LPAREN type_name COMMA offsetof_member_designator RPAREN {
let loc_f = Cil_datatype.Location.of_lexing_loc $loc($1) in
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 0d523e85c3..8ca38fc507 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -265,6 +265,12 @@ let rec stripParen e =
| { expr_node = Cabs.PAREN e } -> stripParen e
| e -> e
+let is_for_builtin builtin info =
+ match info with
+ | SINGLE_INIT { expr_node = VARIABLE name } ->
+ String.equal ("__fc_" ^ builtin) name
+ | _ -> false
+
let rec is_dangerous_offset = function
NoOffset -> false
| Field (fi, o) ->
@@ -5818,6 +5824,26 @@ and doExp local_env
finishExp [] scope_chunk (new_exp ~loc (AlignOfE(e'')))
(Machine.sizeof_type ())
+ (* In cparser, the types used as arguments of certain builtins are converted
+ to casts so that they can be represented as expressions. The following
+ matches are special cases to type those expressions. They are then
+ converted to `sizeof typ` for CIL. *)
+ | Cabs.CAST ((specs, dt), info)
+ when is_for_builtin "__builtin_types_compatible_p" info ->
+ let typ = doOnlyType loc local_env.is_ghost specs dt in
+ let res = new_exp ~loc (SizeOf typ) in
+ finishExp [] (unspecified_chunk empty) res (Machine.sizeof_type ())
+
+ | Cabs.CAST ((specs, dt), info)
+ when is_for_builtin "__builtin_va_arg" info ->
+ let typ = doOnlyType loc local_env.is_ghost specs dt in
+ if not (Cil.isCompleteType typ) then
+ Kernel.error ~current:true "__builtin_va_arg on incomplete type '%a'"
+ Cil_datatype.Typ.pretty typ;
+ let res = new_exp ~loc (SizeOf typ) in
+ finishExp [] (unspecified_chunk empty) res (Machine.sizeof_type ())
+ (* End of special casts. *)
+
| Cabs.CAST ((specs, dt), ie) ->
let s', dt', ie' = preprocessCast loc local_env.is_ghost specs dt ie in
(* We know now that we can do s' and dt' many times *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index f3bc4b667c..43115b0c53 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -1097,7 +1097,7 @@ class cil_printer () = object (self)
let last = self#getLastNamedArgument () in
self#instr fmt (Call(res,Cil.dummy_exp(Lval(Var vi,NoOffset)),[last],l))
- (* In cparser we have turned the call to
+ (* In cabs2cil we have turned the call to
__builtin_types_compatible_p(t1, t2) into
__builtin_types_compatible_p(sizeof t1, sizeof t2), so that we can
represent the types as expressions.
--
GitLab