From 8efcd09eb4fe97338500e52153372f01f871a6f8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Apr 2022 14:49:45 +0300 Subject: [PATCH 1/5] Use var_eq unknown invalidate fix from #618 --- src/analyses/varEq.ml | 11 ++--------- .../06-symbeq/32-var_eq-unknown-invalidate.c | 2 +- 2 files changed, 3 insertions(+), 10 deletions(-) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 4eb8d2186a..7512c52822 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -491,15 +491,8 @@ struct match reachables (Analyses.ask_of_ctx ctx) es with | None -> D.top () | Some rs -> - let remove_reachable1 es st = - let remove_reachable2 e st = - if reachable_from rs e && not (isConstant e) then remove_exp (Analyses.ask_of_ctx ctx) e st else st - in - D.B.fold remove_reachable2 es st - in - (* TODO: do something like this instead to be sound? *) - (* List.fold_left (fun st e -> remove_exp (Analyses.ask_of_ctx ctx) e st) ctx.local (Queries.LS.fold (fun lval acc -> mkAddrOf (Lval.CilLval.to_lval lval) :: acc) rs []) *) - D.fold remove_reachable1 ctx.local ctx.local + (* TODO: avoid intermediate list *) + List.fold_left (fun st e -> remove_exp (Analyses.ask_of_ctx ctx) e st) ctx.local (Queries.LS.fold (fun lval acc -> mkAddrOf (Lval.CilLval.to_lval lval) :: acc) rs []) let unknown_fn ctx lval f args = let args = diff --git a/tests/regression/06-symbeq/32-var_eq-unknown-invalidate.c b/tests/regression/06-symbeq/32-var_eq-unknown-invalidate.c index e7ac5d46cc..540cd1013d 100644 --- a/tests/regression/06-symbeq/32-var_eq-unknown-invalidate.c +++ b/tests/regression/06-symbeq/32-var_eq-unknown-invalidate.c @@ -19,7 +19,7 @@ int main() { if (res == (struct resource *)0) assert(1); // reachable else - assert(1); // TODO reachable + assert(1); // reachable return 0; } \ No newline at end of file From a829e55d5e3e615f91a97d9b5ea2c9bccafc1eeb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Apr 2022 14:50:28 +0300 Subject: [PATCH 2/5] Fix VarEq.may_change TypeOfError on alloc variables --- src/analyses/varEq.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 7512c52822..ae94638fe3 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -193,6 +193,7 @@ struct let bt = match unrollTypeDeep (Cilfacade.typeOf b) with | TPtr (t,_) -> t + | exception Cilfacade.TypeOfError _ | _ -> voidType in (* type of thing that changed: typeof( *b ) *) let rec type_may_change_apt a = From 68c9a277a24d1e48b1277186a20b99e48463c38e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Apr 2022 14:51:09 +0300 Subject: [PATCH 3/5] Fix base eval_lv crash on "unknown" offset from own query results --- src/analyses/base.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index a39b0a5945..5bd3e909ac 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -809,6 +809,8 @@ struct match ofs with | NoOffset -> `NoOffset | Field (fld, ofs) -> `Field (fld, convert_offset a gs st ofs) + | Index (CastE (TInt(IInt,[]), Const (CStr ("unknown",No_encoding))), ofs) -> (* special offset added by convertToQueryLval *) + `Index (IdxDom.top (), convert_offset a gs st ofs) | Index (exp, ofs) -> let exp_rv = eval_rv a gs st exp in match exp_rv with From 5e5fd267af31d76cb8bd76933570194c7db31176 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Apr 2022 14:57:07 +0300 Subject: [PATCH 4/5] Simplify VarEq.remove_reachable --- src/analyses/varEq.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index ae94638fe3..6551c30079 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -489,11 +489,13 @@ struct | None -> st2 let remove_reachable ctx es = - match reachables (Analyses.ask_of_ctx ctx) es with + let ask = Analyses.ask_of_ctx ctx in + match reachables ask es with | None -> D.top () | Some rs -> - (* TODO: avoid intermediate list *) - List.fold_left (fun st e -> remove_exp (Analyses.ask_of_ctx ctx) e st) ctx.local (Queries.LS.fold (fun lval acc -> mkAddrOf (Lval.CilLval.to_lval lval) :: acc) rs []) + Queries.LS.fold (fun lval st -> + remove ask (Lval.CilLval.to_lval lval) st + ) rs ctx.local let unknown_fn ctx lval f args = let args = From c0765c4b006ca71efe5219b639cf260b3be4c205 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 27 Apr 2022 09:15:27 +0300 Subject: [PATCH 5/5] Remove now-unused VarEq.reachable_from (PR #694) --- src/analyses/varEq.ml | 37 +++---------------------------------- 1 file changed, 3 insertions(+), 34 deletions(-) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 6551c30079..280779bbc2 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -409,40 +409,6 @@ struct in List.fold_right reachable es (Some (Queries.LS.empty ())) - let rec reachable_from (r:Queries.LS.t) e = - if Queries.LS.is_top r then true else - let rec is_prefix x1 x2 = - match x1, x2 with - | _, `NoOffset -> true - | Field (f1,o1), `Field (f2,o2) when CilType.Fieldinfo.equal f1 f2 -> is_prefix o1 o2 - | Index (_,o1), `Index (_,o2) -> is_prefix o1 o2 - | _ -> false - in - let has_reachable_prefix v1 ofs = - let suitable_prefix (v2,ofs2) = - CilType.Varinfo.equal v1 v2 - && is_prefix ofs ofs2 - in - Queries.LS.exists suitable_prefix r - in - match e with - | SizeOf _ - | SizeOfE _ - | SizeOfStr _ - | AlignOf _ - | Const _ - | AlignOfE _ - | UnOp _ - | BinOp _ -> true - | AddrOf (Var v2,ofs) - | StartOf (Var v2,ofs) - | Lval (Var v2,ofs) -> has_reachable_prefix v2 ofs - | AddrOf (Mem e,_) - | StartOf (Mem e,_) - | Lval (Mem e,_) - | CastE (_,e) -> reachable_from r e - | Question _ -> failwith "Logical operations should be compiled away by CIL." - | _ -> failwith "Unmatched pattern." (* Probably ok as is. *) let body ctx f = ctx.local @@ -493,6 +459,9 @@ struct match reachables ask es with | None -> D.top () | Some rs -> + (* Prior to https://github.com/goblint/analyzer/pull/694 checks were done "in the other direction": + each expression in ctx.local was checked for reachability from es/rs using very conservative but also unsound reachable_from. + It is unknown, why that was necessary. *) Queries.LS.fold (fun lval st -> remove ask (Lval.CilLval.to_lval lval) st ) rs ctx.local