Skip to content

Relational analysis always populates result table even when not dumping #1526

Closed
@michael-schwarz

Description

@michael-schwarz

let sync ctx reason =
(* After the solver is finished, store the results (for later comparison) *)
if !AnalysisState.postsolving then begin
let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in
let keep_global = GobConfig.get_bool "ana.relation.invariant.global" in
(* filter variables *)
let var_filter v = match RV.find_metadata v with
| Some (Global _) -> keep_global
| Some (Local _) -> keep_local
| _ -> false
in
let st = RD.keep_filter ctx.local.rel var_filter in
let old_value = PCU.RH.find_default results ctx.node (RD.bot ()) in
let new_value = RD.join old_value st in
PCU.RH.replace results ctx.node new_value;
end;
WideningTokens.with_local_side_tokens (fun () ->
Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread])
)

Here, the table results is always populated, even whenexp.relation.prec-dump is off, and results is never considered. This is likely not terribly expensive given casting to octagons only happens later, but still completely unnecessary.

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions