From 5ed93d579371ebc07eec3c4543a1b8d7b3620018 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 25 Mar 2020 18:30:44 +0100
Subject: [PATCH] [Instantiate] m/c alloc: refuse incomplete types
---
src/plugins/instantiate/stdlib/calloc.ml | 3 +-
src/plugins/instantiate/stdlib/malloc.ml | 3 +-
src/plugins/instantiate/tests/stdlib/calloc.c | 1 +
src/plugins/instantiate/tests/stdlib/free.c | 3 +
src/plugins/instantiate/tests/stdlib/malloc.c | 3 +
.../tests/stdlib/oracle/calloc.res.oracle | 7 +-
.../tests/stdlib/oracle/free.res.oracle | 76 ++++++++++++++++++-
.../tests/stdlib/oracle/malloc.res.oracle | 11 ++-
8 files changed, 97 insertions(+), 10 deletions(-)
diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml
index 1ea994392c6..e1cc1460c39 100644
--- a/src/plugins/instantiate/stdlib/calloc.ml
+++ b/src/plugins/instantiate/stdlib/calloc.ml
@@ -133,7 +133,8 @@ let well_typed_call ret args =
match ret, args with
| Some ret, [ _ ; _ ] ->
let t = Cil.typeOfLval ret in
- Cil.isPointerType t && not (Cil.isVoidPtrType t)
+ Cil.isPointerType t && not (Cil.isVoidPtrType t) &&
+ Cil.isCompleteType (Cil.typeOf_pointed t)
| _ -> false
let key_from_call ret _ =
diff --git a/src/plugins/instantiate/stdlib/malloc.ml b/src/plugins/instantiate/stdlib/malloc.ml
index a6debf251e1..9cc215a7711 100644
--- a/src/plugins/instantiate/stdlib/malloc.ml
+++ b/src/plugins/instantiate/stdlib/malloc.ml
@@ -72,7 +72,8 @@ let well_typed_call ret args =
match ret, args with
| Some ret, [ _ ] ->
let t = Cil.typeOfLval ret in
- Cil.isPointerType t && not (Cil.isVoidPtrType t)
+ Cil.isPointerType t && not (Cil.isVoidPtrType t) &&
+ Cil.isCompleteType (Cil.typeOf_pointed t)
| _ -> false
let key_from_call ret _ =
diff --git a/src/plugins/instantiate/tests/stdlib/calloc.c b/src/plugins/instantiate/tests/stdlib/calloc.c
index 77be4d292f1..87b1f9338cc 100644
--- a/src/plugins/instantiate/tests/stdlib/calloc.c
+++ b/src/plugins/instantiate/tests/stdlib/calloc.c
@@ -19,4 +19,5 @@ int main(void){
int (*pa) [10] = calloc(10, sizeof(int[10])) ;
struct Flex* f = calloc(1, sizeof(struct Flex) + 3 * sizeof(int)) ;
void *v = calloc(10, sizeof(char));
+ struct incomplete* inc = calloc(10, 10);
}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/stdlib/free.c b/src/plugins/instantiate/tests/stdlib/free.c
index 40cab4f547c..e61ed8864c1 100644
--- a/src/plugins/instantiate/tests/stdlib/free.c
+++ b/src/plugins/instantiate/tests/stdlib/free.c
@@ -11,4 +11,7 @@ void baz(int (*x) [10]){
}
void with_void(void * x){
free(x);
+}
+void with_incomplete(struct incomplete* t){
+ free(t);
}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/stdlib/malloc.c b/src/plugins/instantiate/tests/stdlib/malloc.c
index 0d5aa4ea04a..00a07820a9a 100644
--- a/src/plugins/instantiate/tests/stdlib/malloc.c
+++ b/src/plugins/instantiate/tests/stdlib/malloc.c
@@ -11,6 +11,8 @@ struct Flex {
int f[] ;
} ;
+struct incomplete ;
+
int main(void){
int* pi = malloc(sizeof(int) * 10) ;
float* pf = malloc(sizeof(float) * 10) ;
@@ -19,4 +21,5 @@ int main(void){
int (*pa) [10] = malloc(sizeof(int[10]) * 10) ;
struct Flex* f = malloc(sizeof(struct Flex) + 3 * sizeof(int)) ;
void *v = malloc(sizeof(char) * 10);
+ struct incomplete* inc = malloc(10);
}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
index 5fb370ab29a..81cf9b246df 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
[instantiate] tests/stdlib/calloc.c:21: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/calloc.c:22: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -11,6 +12,7 @@ struct Flex {
char c ;
int f[] ;
};
+struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
requires only_one: num ≡ 1;
assigns \result, __fc_heap_status;
@@ -263,6 +265,7 @@ int main(void)
calloc_st_Flex((unsigned int)1,
sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = calloc((unsigned int)10,sizeof(char));
+ struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
__retres = 0;
return __retres;
}
@@ -271,7 +274,7 @@ int main(void)
[kernel] Parsing tests/stdlib/result/calloc.c (with preprocessing)
[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
[kernel] tests/stdlib/calloc.c:14: Warning:
- def'n of func main at tests/stdlib/calloc.c:14 (sum 6403) conflicts with the one at tests/stdlib/result/calloc.c:252 (sum 8177); keeping the one at tests/stdlib/result/calloc.c:252.
+ def'n of func main at tests/stdlib/calloc.c:14 (sum 7290) conflicts with the one at tests/stdlib/result/calloc.c:253 (sum 9064); keeping the one at tests/stdlib/result/calloc.c:253.
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -283,6 +286,7 @@ struct Flex {
char c ;
int f[] ;
};
+struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
requires only_one: num ≡ 1;
assigns \result, __fc_heap_status;
@@ -539,6 +543,7 @@ int main(void)
calloc_st_Flex((unsigned int)1,
sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = calloc((unsigned int)10,sizeof(char));
+ struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
index 1e764fcd7c6..11f5ef65b0e 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
@@ -2,6 +2,7 @@
[instantiate] tests/stdlib/free.c:13: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
+struct incomplete;
/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status, ptr;
@@ -104,19 +105,54 @@ void with_void(void *x)
return;
}
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_st_incomplete(struct incomplete *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+void with_incomplete(struct incomplete *t)
+{
+ free_st_incomplete(t);
+ return;
+}
+
[kernel] Parsing tests/stdlib/result/free.c (with preprocessing)
[kernel] Parsing tests/stdlib/free.c (with preprocessing)
[kernel] tests/stdlib/free.c:3: Warning:
- dropping duplicate def'n of func foo at tests/stdlib/free.c:3 in favor of that at tests/stdlib/result/free.c:29
+ dropping duplicate def'n of func foo at tests/stdlib/free.c:3 in favor of that at tests/stdlib/result/free.c:30
[kernel] tests/stdlib/free.c:6: Warning:
- dropping duplicate def'n of func bar at tests/stdlib/free.c:6 in favor of that at tests/stdlib/result/free.c:61
+ dropping duplicate def'n of func bar at tests/stdlib/free.c:6 in favor of that at tests/stdlib/result/free.c:62
[kernel] tests/stdlib/free.c:9: Warning:
- dropping duplicate def'n of func baz at tests/stdlib/free.c:9 in favor of that at tests/stdlib/result/free.c:93
+ dropping duplicate def'n of func baz at tests/stdlib/free.c:9 in favor of that at tests/stdlib/result/free.c:94
[kernel] tests/stdlib/free.c:12: Warning:
- dropping duplicate def'n of func with_void at tests/stdlib/free.c:12 in favor of that at tests/stdlib/result/free.c:99
+ dropping duplicate def'n of func with_void at tests/stdlib/free.c:12 in favor of that at tests/stdlib/result/free.c:100
+[kernel] tests/stdlib/free.c:15: Warning:
+ dropping duplicate def'n of func with_incomplete at tests/stdlib/free.c:15 in favor of that at tests/stdlib/result/free.c:132
/* Generated by Frama-C */
#include "stdlib.h"
+struct incomplete;
/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
assigns __fc_heap_status;
assigns __fc_heap_status \from __fc_heap_status, ptr;
@@ -219,4 +255,36 @@ void with_void(void *x)
return;
}
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior allocation:
+ assumes ptr ≢ \null;
+ ensures freed: \allocable(\old(ptr));
+ assigns __fc_heap_status;
+ assigns __fc_heap_status \from __fc_heap_status, ptr;
+ frees ptr;
+
+ behavior no_allocation:
+ assumes ptr ≡ \null;
+ assigns \nothing;
+ allocates \nothing;
+
+ complete behaviors no_allocation, allocation;
+ disjoint behaviors no_allocation, allocation;
+ */
+void free_st_incomplete(struct incomplete *ptr)
+{
+ free((void *)ptr);
+ return;
+}
+
+void with_incomplete(struct incomplete *t)
+{
+ free_st_incomplete(t);
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
index feb0c41909d..485abcec7f4 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[instantiate] tests/stdlib/malloc.c:21: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/malloc.c:23: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/malloc.c:24: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -11,6 +12,7 @@ struct Flex {
char c ;
int f[] ;
};
+struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
assigns \result, __fc_heap_status;
assigns \result \from __fc_heap_status, size;
@@ -208,6 +210,7 @@ int main(void)
struct Flex *f =
malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = malloc(sizeof(char) * (unsigned int)10);
+ struct incomplete *inc = malloc((unsigned int)10);
__retres = 0;
return __retres;
}
@@ -215,8 +218,8 @@ int main(void)
[kernel] Parsing tests/stdlib/result/malloc.c (with preprocessing)
[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[kernel] tests/stdlib/malloc.c:14: Warning:
- def'n of func main at tests/stdlib/malloc.c:14 (sum 6403) conflicts with the one at tests/stdlib/result/malloc.c:198 (sum 8177); keeping the one at tests/stdlib/result/malloc.c:198.
+[kernel] tests/stdlib/malloc.c:16: Warning:
+ def'n of func main at tests/stdlib/malloc.c:16 (sum 7290) conflicts with the one at tests/stdlib/result/malloc.c:199 (sum 9064); keeping the one at tests/stdlib/result/malloc.c:199.
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -228,6 +231,7 @@ struct Flex {
char c ;
int f[] ;
};
+struct incomplete;
/*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
assigns \result, __fc_heap_status;
assigns \result \from __fc_heap_status, size;
@@ -425,6 +429,7 @@ int main(void)
struct Flex *f =
malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = malloc(sizeof(char) * (unsigned int)10);
+ struct incomplete *inc = malloc((unsigned int)10);
__retres = 0;
return __retres;
}
--
GitLab