Skip to content

Commit

Permalink
Re-enable CIL inlines merging to work around its bug
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Feb 28, 2022
1 parent e75edab commit 62d7591
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/util/cilfacade.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@ let init () =
initCIL ();
lowerConstants := true;
Mergecil.ignore_merge_conflicts := true;
Mergecil.merge_inlines := true; (* work around https://github.com/goblint/analyzer/pull/603#issuecomment-1054204635 *)
(* lineDirectiveStyle := None; *)
Rmtmps.keepUnused := true;
print_CIL_Input := true
Expand Down

8 comments on commit 62d7591

@michael-schwarz
Copy link
Member

@michael-schwarz michael-schwarz commented on 62d7591 Feb 28, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should be careful with this, if we do this, our incremental approach stops working for zstd. CC @stilscher

@sim642
Copy link
Member Author

@sim642 sim642 commented on 62d7591 Feb 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Define "stops working". With optimizations and fortification disabled during preprocessing, what other inlines were there?

Considering goblint/cil#84, which screws up our internal notion of functions, I'd say that would potentially invalidate benchmarking results as well and more likely even cause incremental comparison/update to silently do something wrong. So I'm not sure how well that would work either.

@michael-schwarz
Copy link
Member

@michael-schwarz michael-schwarz commented on 62d7591 Feb 28, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Define "stops working".

Throws an exception during List.iter2 on CFG comparison.
Edit: Actually, might have been during AST comparison already @stilscher?

@sim642
Copy link
Member Author

@sim642 sim642 commented on 62d7591 Feb 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess that's just #574, which should be fixed anyway instead of hiding it behind inline merging.

@stilscher
Copy link
Member

@stilscher stilscher commented on 62d7591 Feb 28, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think the problem with merging inlines has anything to do with the CFG comparison. I just tried it again, the analysis on zstd runs through even with merge_inlines turned on, but with several warnings such as "The name MEM_32bits is used for two distinct globals". Having two distinct globals with the same name can be problematic because it possibly breaks the general CIL file comparison (used for CFG and AST comparison) which assumes that globals can be uniquely identified by their category (GVar, GVarDecl, GFun) and their name.

I opened the PR #615 to insert a check for duplicate global identifiers to hopefully make the reason for a failure more obvious than the delayed exception in List.iter2 of UpdateCil.ml that often appeared when different function globals share the same name.

@sim642
Copy link
Member Author

@sim642 sim642 commented on 62d7591 Feb 28, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually I suspect goblint/cil#84 isn't just limited to merging of inlines, but also some other functions because there's a bunch of different cases for function merging, but regardless the names are merged unconditionally first.
I therefore suspect that a similar problem leads to this "is used for two distinct globals" if Mergecil eagerly merges the names (makes fundecs share a single varinfo), but then doesn't actually merge the functions, leaving two fundecs around.

@stilscher
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Have we come to a conclusion on what to do here? So far I ran the benchmarks without this change (that is merge_inlines turned off) because with merge_inline set to true, the incremental runs on zstd do not pass this check from #615. And I think it is not justifiable to incrementally analyze files with duplicate globals when we know that the comparison can not handle this.

@sim642
Copy link
Member Author

@sim642 sim642 commented on 62d7591 Mar 15, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Well yeah, either way this causes issues for incremental compare/update (although for different reasons), so there's no easy way out.

Do you know the source for these "is used for two distinct globals" warnings?
I'm not sure if this is it, but I happened to look into the compiledb database for ztd and it contains some anomalies: files like debug.c are listed twice with vastly different arguments. For example, the first entry doesn't even have the -DZSTD_NO_INTRINSICS that we want to force it to have. Maybe it's another case of #628 where compiledb leaves some semi-duplicate broken entries?

EDIT: Bear doesn't leave multiple entries for debug.c at least.

Please sign in to comment.