From 55fa6bd96bd5413ae181f2da0cba9b670c0613b1 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 28 Feb 2025 10:26:36 +0100 Subject: [PATCH 1/2] Fix refinement in `baseInvariant` for more complicated lvals --- src/analyses/baseInvariant.ml | 18 +++++++++------- tests/regression/03-practical/36-struct-ptr.c | 21 +++++++++++++++++++ 2 files changed, 32 insertions(+), 7 deletions(-) create mode 100644 tests/regression/03-practical/36-struct-ptr.c diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index fd52d099bf..ccc83e7d18 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -112,14 +112,18 @@ struct r ) | Mem (Lval lv), off -> - let lvals = eval_lv ~man st (Mem (Lval lv), off) in - let res = AD.fold (fun a acc -> + (* Underlying lvals (may have offsets themselves), e.g., for struct members NOT including any offset appended to outer Mem *) + let lvals = eval_lv ~man st (Mem (Lval lv), NoOffset) in + (* Additional offset of value being refined in Addr Offset type *) + let original_offset = convert_offset ~man st off in + let res = AD.fold (fun base_a acc -> Option.bind acc (fun acc -> - match a with - | Addr (base, _) as orig -> - let (a:VD.t) = Address (AD.singleton (AD.Addr.of_var base)) in - if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty a; - let st = set' lv a st in + match base_a with + | Addr _ -> + let (lval_a:VD.t) = Address (AD.singleton base_a) in + if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty lval_a; + let st = set' lv lval_a st in + let orig = AD.Addr.add_offset base_a original_offset in let old_val = get ~man st (AD.singleton orig) None in let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *) (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *) diff --git a/tests/regression/03-practical/36-struct-ptr.c b/tests/regression/03-practical/36-struct-ptr.c new file mode 100644 index 0000000000..eb31293cd0 --- /dev/null +++ b/tests/regression/03-practical/36-struct-ptr.c @@ -0,0 +1,21 @@ +#include +struct aws_al { + unsigned long current_size; + }; + + struct aws_pq { + int pred; + struct aws_al container; + }; + + int main() { + struct aws_pq queue = { 0, { 0}}; + struct aws_al *const list = &queue.container; + + if (list->current_size == 0UL) { + if (list->current_size == 0UL) + { + __goblint_check(1); //REACHABLE + } + } + } From b05e305aef7d881b4bd4feba7b9cd80f75875e24 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 3 Mar 2025 10:34:36 +0100 Subject: [PATCH 2/2] 03/36: Fix indentation --- tests/regression/03-practical/36-struct-ptr.c | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/tests/regression/03-practical/36-struct-ptr.c b/tests/regression/03-practical/36-struct-ptr.c index eb31293cd0..e96a7f7966 100644 --- a/tests/regression/03-practical/36-struct-ptr.c +++ b/tests/regression/03-practical/36-struct-ptr.c @@ -1,21 +1,20 @@ #include struct aws_al { unsigned long current_size; - }; +}; - struct aws_pq { - int pred; - struct aws_al container; - }; +struct aws_pq { + int pred; + struct aws_al container; +}; - int main() { +int main() { struct aws_pq queue = { 0, { 0}}; struct aws_al *const list = &queue.container; if (list->current_size == 0UL) { - if (list->current_size == 0UL) - { + if (list->current_size == 0UL) { __goblint_check(1); //REACHABLE } } - } +}