From effaace3a7d9e3b42baff2e20ef4c5a6df99774e Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 2 Oct 2023 09:58:20 +0200
Subject: [PATCH] Move transformation inside compileCondExp
---
src/kernel_internals/typing/cabs2cil.ml | 36 +++++-----
...emporary_object_issue_1037-1220.res.oracle | 68 ++++++++++++++-----
.../syntax/temporary_object_issue_1037-1220.i | 16 +++--
3 files changed, 76 insertions(+), 44 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 99ff1f644d8..99ff8f404ad 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -7702,7 +7702,7 @@ and doCondExp local_env asconst
in
result
-and compileCondExp ~ghost ce st sf =
+and compileCondExp ?(hide=false) ~ghost ce st sf =
match ce with
| CEAnd (ce1, ce2) ->
let loc = CurrentLoc.get () in
@@ -7713,7 +7713,7 @@ and compileCondExp ~ghost ce st sf =
let lab = newLabelName ghost "_LAND" in
(false, gotoChunk ~ghost lab loc, consLabel ~ghost lab sf loc false)
in
- let st' = compileCondExp ~ghost ce2 st sf1 in
+ let st' = compileCondExp ~hide ~ghost ce2 st sf1 in
if not duplicable && !doAlternateConditional then
let st_fall_through = chunkFallsThrough st' in
(* if st does not fall through, we do not need to add a goto
@@ -7730,11 +7730,11 @@ and compileCondExp ~ghost ce st sf =
else skipChunk
in
let (@@@) s1 s2 = s1 @@@ (s2, ghost) in
- (compileCondExp ~ghost ce1 st' sf')
+ (compileCondExp ~hide ~ghost ce1 st' sf')
@@@ gotostmt @@@ sf2 @@@ labstmt
else
let sf' = sf2 in
- compileCondExp ~ghost ce1 st' sf'
+ compileCondExp ~hide ~ghost ce1 st' sf'
| CEOr (ce1, ce2) ->
let loc = CurrentLoc.get () in
@@ -7747,7 +7747,7 @@ and compileCondExp ~ghost ce st sf =
in
if not duplicable && !doAlternateConditional then
let st' = duplicateChunk st1 in
- let sf' = compileCondExp ~ghost ce2 st1 sf in
+ let sf' = compileCondExp ~hide ~ghost ce2 st1 sf in
let sf_fall_through = chunkFallsThrough sf' in
let lab = newLabelName ghost "_LOR" in
let gotostmt =
@@ -7761,17 +7761,14 @@ and compileCondExp ~ghost ce st sf =
else skipChunk
in
let (@@@) s1 s2 = s1 @@@ (s2, ghost) in
- (compileCondExp ~ghost ce1 st' sf')
+ (compileCondExp ~hide ~ghost ce1 st' sf')
@@@ gotostmt @@@ st2 @@@ labstmt
else
let st' = st1 in
- let sf' = compileCondExp ~ghost ce2 st2 sf in
- (*Format.eprintf
- "result:@\nchunk then:@\n @[%a@]@\nchunk else: @[%a@]@."
- d_chunk st d_chunk sf;*)
- compileCondExp ~ghost ce1 st' sf'
+ let sf' = compileCondExp ~hide ~ghost ce2 st2 sf in
+ compileCondExp ~hide ~ghost ce1 st' sf'
- | CENot ce1 -> compileCondExp ~ghost ce1 sf st
+ | CENot ce1 -> compileCondExp ~hide ~ghost ce1 sf st
| CEExp (se, e) -> begin
match e.enode with
@@ -7783,7 +7780,12 @@ and compileCondExp ~ghost ce st sf =
when (Integer.equal z Integer.zero) && canDrop st ->
full_clean_up_chunk_locals st;
se @@@ (sf, ghost)
- | _ -> (empty @@@ (se, ghost)) @@@ (ifChunk ~ghost e e.eloc st sf, ghost)
+ | _ ->
+ let se', e' =
+ if hide then hide_chunk ~ghost ~loc:e.eloc [] se e (typeOf e)
+ else se, e
+ in
+ (empty @@@ (se', ghost)) @@@ (ifChunk ~ghost e' e'.eloc st sf, ghost)
end
@@ -7822,12 +7824,8 @@ and doCondition ~is_loop local_env asconst
if is_loop then
(* enclose our problematic chunk and the break condition. *)
enclose_chunk ~ghost (compileCondExp ~ghost ce st sf)
- else match ce with
- | CEExp (c, e) ->
- (* Else if it's a IF, hide chunk result. *)
- let c', e' = hide_chunk ~ghost ~loc:e.eloc [] c e (typeOf e) in
- compileCondExp ~ghost (CEExp (c', e')) st sf
- | _ -> assert false
+ else
+ compileCondExp ~hide:true ~ghost ce st sf
end
else compileCondExp ~ghost ce st sf
end
diff --git a/tests/syntax/oracle/temporary_object_issue_1037-1220.res.oracle b/tests/syntax/oracle/temporary_object_issue_1037-1220.res.oracle
index b25ba284ac5..5322119aa8d 100644
--- a/tests/syntax/oracle/temporary_object_issue_1037-1220.res.oracle
+++ b/tests/syntax/oracle/temporary_object_issue_1037-1220.res.oracle
@@ -1,20 +1,20 @@
[kernel] Parsing temporary_object_issue_1037-1220.i (no preprocessing)
/* Generated by Frama-C */
struct X {
- int arr[1] ;
+ int arr[2] ;
};
struct S {
struct X x ;
};
struct X get_x(void)
{
- struct X __constr_expr_0 = {.arr = {42}};
+ struct X __constr_expr_0 = {.arr = {42, 16}};
return __constr_expr_0;
}
struct S get_s(void)
{
- struct S __constr_expr_1 = {.x = {.arr = {42}}};
+ struct S __constr_expr_1 = {.x = {.arr = {42, 16}}};
return __constr_expr_1;
}
@@ -57,9 +57,10 @@ void g2(int *x)
return;
}
-void calls(void)
+int *calls(void)
{
int tmp_0;
+ int *tmp_3;
{
struct X tmp;
tmp = get_x();
@@ -71,15 +72,21 @@ void calls(void)
tmp_1 = get_x();
g2(tmp_1.arr);
}
- return;
+ {
+ struct X tmp_2;
+ tmp_2 = get_x();
+ tmp_3 = tmp_2.arr;
+ }
+ return tmp_3;
}
int *cond(void)
{
int *__retres;
+ int *p;
char *tmp_1;
int tmp_3;
- int *tmp_7;
+ int tmp_7;
{
struct X tmp;
tmp = get_x();
@@ -103,30 +110,55 @@ int *cond(void)
__retres = (int *)2;
goto return_label;
}
+ {
+ struct X tmp_4;
+ tmp_4 = get_x();
+ ;
+ tmp_7 = tmp_4.arr[0];
+ }
+ if (tmp_7) {
+ __retres = (int *)3;
+ goto return_label;
+ }
+ else {
+ int tmp_6;
+ {
+ struct X tmp_5;
+ tmp_5 = get_x();
+ p = tmp_5.arr;
+ tmp_6 = *(p + 1);
+ }
+ if (tmp_6) {
+ __retres = (int *)3;
+ goto return_label;
+ }
+ }
{
int i = 0;
while (1) {
{
- struct X tmp_4;
- tmp_4 = get_x();
- if (! (tmp_4.arr)) break;
+ struct X tmp_8;
+ tmp_8 = get_x();
+ if (! (tmp_8.arr)) break;
}
i ++;
}
}
while (1) {
{
- struct X tmp_5;
- tmp_5 = get_x();
- if (! (tmp_5.arr)) break;
+ struct X tmp_9;
+ tmp_9 = get_x();
+ ;
+ if (tmp_9.arr[0]) {
+ struct X tmp_10;
+ tmp_10 = get_x();
+ ;
+ if (! tmp_10.arr[1]) break;
+ }
+ else break;
}
}
- {
- struct X tmp_6;
- tmp_6 = get_x();
- tmp_7 = tmp_6.arr;
- }
- __retres = tmp_7;
+ __retres = p;
return_label: return __retres;
}
diff --git a/tests/syntax/temporary_object_issue_1037-1220.i b/tests/syntax/temporary_object_issue_1037-1220.i
index cec72a204fc..692f1931ced 100644
--- a/tests/syntax/temporary_object_issue_1037-1220.i
+++ b/tests/syntax/temporary_object_issue_1037-1220.i
@@ -3,7 +3,7 @@
*/
struct X {
- int arr[1];
+ int arr[2];
};
struct S {
@@ -11,9 +11,9 @@ struct S {
};
-struct X get_x(void) { return (struct X){42}; }
+struct X get_x(void) { return (struct X){42,16}; }
-struct S get_s(void) { return (struct S){ (struct X){42} }; }
+struct S get_s(void) { return (struct S){ (struct X){42,16} }; }
int init(void) {
int *p = get_x().arr; // OK
@@ -26,7 +26,7 @@ int g1(int* x) { return *x; }
void g2(int* x) { *x = 1; }
//from issue 1220
-void calls(void) {
+int* calls(void) {
// C99: UB access to a[0] in g1 whose lifetime ended
// at the sequence point at the start of g1
// C11: OK, d is 2.0
@@ -36,20 +36,22 @@ void calls(void) {
// C11: UB attempt to modify a temporary object
g2(get_x().arr); // OK
- return;
+ return get_x().arr; // OK
}
int* cond(void) {
+ int *p;
if(get_x().arr);
if((char*)get_x().arr) return 1; // OK
if(*(get_x().arr + 0)) return 2; // OK
+ if(*(get_x().arr + 0) || (p = get_x().arr, *(p + 1))) return 3; // OK
for (int i = 0; get_x().arr; i++); // OK
- do{} while (get_x().arr); // OK
+ do{} while (*(get_x().arr + 0) && *(get_x().arr + 1)); // OK
- return get_x().arr; // OK
+ return p; // UB
}
int paren_return(void){
--
GitLab