From ae7067eea7869563a3e596eeb88b2e63b14673c7 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 14 Nov 2022 11:18:24 +0100
Subject: [PATCH] Check for function formal argument with frama_c_init_obj
attribute.
- Extend checking to more than just left-values.
- Add function in Cil to check only for frama_c_init_obj attribute (as formals
should not be annotated with frama_c_mutable one).
---
src/kernel_internals/typing/cabs2cil.ml | 11 +++++-
src/kernel_services/ast_queries/cil.ml | 35 +++++++++++++------
src/kernel_services/ast_queries/cil.mli | 4 +++
tests/syntax/const-assignments.c | 19 +++++++++-
.../oracle/const-assignments.0.res.oracle | 22 ++++++++++--
.../oracle/const-assignments.7.res.oracle | 22 ++++++++++--
.../oracle/const-assignments.8.res.oracle | 22 ++++++++++--
.../oracle/const-assignments.9.res.oracle | 4 ++-
8 files changed, 120 insertions(+), 19 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 13006c85942..33c49076663 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6877,8 +6877,17 @@ and doExp local_env
(Cil.isPointerType texpected && Ast_info.is_null_expr a') ||
areCompatibleTypes ~context:ContravariantToplevel att texpected
in
+ let ok2 =
+ (* accept pointer to const type as long as the respective
+ argument (formal) is annotated with __fc_initialized_object
+ attribute. *)
+ let arg_is_initialized = Cil.is_initialized a' in
+ arg_is_initialized
+ && Cil.isPointerType texpected
+ && areCompatibleTypes ~context:CovariantToplevel att texpected
+ in
let ok =
- if ok1 then true
+ if ok1 || ok2 then true
(* special warning for void* -> any* conversions;
this is equivalent to option '-Wc++-compat' in GCC *)
else if Cil.isVoidPtrType att && Cil.isPointerType texpected
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 0ca631c1f05..82e08770fa7 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6239,23 +6239,38 @@ and is_complete_agg_member ~allowZeroSizeArrays ?last_field t =
let isCompleteType ?allowZeroSizeArrays t =
isCompleteType ?allowZeroSizeArrays t
-let is_mutable_or_initialized (host, offset) =
+let is_mutable (lhost, offset) =
let rec aux can_mutate typ off =
let can_mutate = can_mutate && not (isConstType typ) in
match unrollType typ, off with
| _, NoOffset -> can_mutate
| _, Field (fi, off) ->
- aux
- (can_mutate || hasAttribute frama_c_mutable fi.fattr)
- fi.ftype off
+ let can_mutate = can_mutate || hasAttribute frama_c_mutable fi.fattr in
+ aux can_mutate fi.ftype off
| TArray(typ, _, _), Index(_, off) -> aux can_mutate typ off
- | _, Index _ -> Kernel.fatal "Index on a non-array type"
+ | typ, Index _ ->
+ Kernel.fatal "Index on a non-array type '%a'" Cil_datatype.Typ.pretty typ
in
- match host with
- | Mem({ enode = Lval (Var vi, NoOffset) })
- when hasAttribute frama_c_init_obj vi.vattr -> true
- | _ ->
- aux false (typeOfLhost host) offset
+ aux false (typeOfLhost lhost) offset
+
+let rec is_initialized_aux on_same_obj e =
+ match e.enode with
+ | Lval (lh, _) | AddrOf (lh, _) | StartOf (lh, _) ->
+ is_initialized_lhost on_same_obj lh
+ | BinOp ((PlusPI|MinusPI), e, _, _) | CastE (_, e) ->
+ is_initialized_aux on_same_obj e
+ | _ -> false
+
+and is_initialized_lhost on_same_obj lhost =
+ match lhost with
+ | Var vi -> hasAttribute frama_c_init_obj vi.vattr
+ | Mem e -> on_same_obj && is_initialized_aux false e
+
+let is_initialized e =
+ is_initialized_aux true e
+
+let is_mutable_or_initialized lval =
+ is_mutable lval || is_initialized_lhost true (fst lval)
let is_modifiable_lval lv =
let t = typeOfLval lv in
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 005bc7a0634..9a2b27a1f4f 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1254,6 +1254,10 @@ val frama_c_mutable: string
*)
val frama_c_inlined: string
+(** [true] if the underlying left-value of the given expression is allowed to be
+ assigned to thanks to a [frama_c_init_obj] attribute. *)
+val is_initialized: exp -> bool
+
(** [true] if the given lval is allowed to be assigned to thanks to
a [frama_c_init_obj] or a [frama_c_mutable] attribute.
*)
diff --git a/tests/syntax/const-assignments.c b/tests/syntax/const-assignments.c
index 745a67aa56a..caa00564dc0 100644
--- a/tests/syntax/const-assignments.c
+++ b/tests/syntax/const-assignments.c
@@ -73,9 +73,10 @@ void h(const int* x) {
g(y);
}
-typedef struct {
+typedef struct S {
__attribute__((__fc_mutable)) int x;
const int y;
+ struct S* z[3];
} S;
void build_S(
@@ -91,6 +92,22 @@ void mutable_test(const S* s) {
s->x += 2;
}
+extern void k1(S*);
+extern void k2(int*);
+
+void mutable_test_call(__attribute__((__fc_initialized_object)) const S* s) {
+ /* Although these calls would make losing the const qualifier, this is OK due
+ to the __fc_initialized_object attribute on s. */
+ k1(s);
+ k1(s->z[0]);
+ int a = 1;
+ k1(a + (s + 2));
+ k2(&(s + 2)->y);
+ /* KO: although s has the __fc_initialized_object attribute, z[0] has not (and
+ cannot) and y is const. */
+ k2(&s->z[0]->y);
+}
+
#ifdef T8
typedef struct {
diff --git a/tests/syntax/oracle/const-assignments.0.res.oracle b/tests/syntax/oracle/const-assignments.0.res.oracle
index 2e6713963fd..8e1f025840a 100644
--- a/tests/syntax/oracle/const-assignments.0.res.oracle
+++ b/tests/syntax/oracle/const-assignments.0.res.oracle
@@ -1,10 +1,13 @@
[kernel] Parsing const-assignments.c (with preprocessing)
+[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
/* Generated by Frama-C */
-struct __anonstruct_S_1 {
+struct S {
int x ;
int const y ;
+ struct S *z[3] ;
};
-typedef struct __anonstruct_S_1 S;
+typedef struct S S;
int const x = 1;
extern void g(int *p);
@@ -31,4 +34,19 @@ void mutable_test(S const *s)
return;
}
+extern void k1(S *);
+
+extern void k2(int *);
+
+void mutable_test_call(S const *s)
+{
+ k1((S *)s);
+ k1(s->z[0]);
+ int a = 1;
+ k1((S *)((s + 2) + a));
+ k2((int *)(& (s + 2)->y));
+ k2((int *)(& (s->z[0])->y));
+ return;
+}
+
diff --git a/tests/syntax/oracle/const-assignments.7.res.oracle b/tests/syntax/oracle/const-assignments.7.res.oracle
index 91a4f1b2285..28fb4fda519 100644
--- a/tests/syntax/oracle/const-assignments.7.res.oracle
+++ b/tests/syntax/oracle/const-assignments.7.res.oracle
@@ -1,12 +1,15 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel:typing:incompatible-types-call] const-assignments.c:60: Warning:
expected 'int *' but got argument of type 'int const *': & x
+[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
/* Generated by Frama-C */
-struct __anonstruct_S_1 {
+struct S {
int x ;
int const y ;
+ struct S *z[3] ;
};
-typedef struct __anonstruct_S_1 S;
+typedef struct S S;
int const x = 1;
extern void g(int *p);
@@ -39,4 +42,19 @@ void mutable_test(S const *s)
return;
}
+extern void k1(S *);
+
+extern void k2(int *);
+
+void mutable_test_call(S const *s)
+{
+ k1((S *)s);
+ k1(s->z[0]);
+ int a = 1;
+ k1((S *)((s + 2) + a));
+ k2((int *)(& (s + 2)->y));
+ k2((int *)(& (s->z[0])->y));
+ return;
+}
+
diff --git a/tests/syntax/oracle/const-assignments.8.res.oracle b/tests/syntax/oracle/const-assignments.8.res.oracle
index 97f911954ff..ee37293dbcb 100644
--- a/tests/syntax/oracle/const-assignments.8.res.oracle
+++ b/tests/syntax/oracle/const-assignments.8.res.oracle
@@ -1,12 +1,15 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel:typing:incompatible-types-call] const-assignments.c:66: Warning:
expected 'int *' but got argument of type 'int const *': x_0
+[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
/* Generated by Frama-C */
-struct __anonstruct_S_1 {
+struct S {
int x ;
int const y ;
+ struct S *z[3] ;
};
-typedef struct __anonstruct_S_1 S;
+typedef struct S S;
int const x = 1;
extern void g(int *p);
@@ -39,4 +42,19 @@ void mutable_test(S const *s)
return;
}
+extern void k1(S *);
+
+extern void k2(int *);
+
+void mutable_test_call(S const *s)
+{
+ k1((S *)s);
+ k1(s->z[0]);
+ int a = 1;
+ k1((S *)((s + 2) + a));
+ k2((int *)(& (s + 2)->y));
+ k2((int *)(& (s->z[0])->y));
+ return;
+}
+
diff --git a/tests/syntax/oracle/const-assignments.9.res.oracle b/tests/syntax/oracle/const-assignments.9.res.oracle
index ae9db5d4373..ec0fc31a923 100644
--- a/tests/syntax/oracle/const-assignments.9.res.oracle
+++ b/tests/syntax/oracle/const-assignments.9.res.oracle
@@ -1,5 +1,7 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:101: User Error:
+[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
+[kernel] const-assignments.c:118: User Error:
Cannot assign to non-modifiable lval t->s.y
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
--
GitLab