<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 16 Aug 2019 at 01:42, Kristóf Umann <<a href="mailto:dkszelethus@gmail.com" target="_blank">dkszelethus@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">We seem to agree on that an even more thought-out dependency system would be good, and that separating checkers into modeling and diagnostics portions would be ideal, so I'll detail my proposal further:<div><br></div><div>I googled it, apparently "modelling" is British, and "modeling" is American, so for this mail I'm just gonna roll with American. :^)</div><div><br></div><div>1. Don't allow dependency checkers (and implicitly regard them as modeling checkers) and modeling checkers to emit diagnostics</div><div>  a.) This implies that if we imagine checkers dependencies as a directed graph where any given checker's parent is the checkers it depends on, any given checker that emits diagnostics is a leaf and has either no parent, or it's parent is a modeling checker, and the path leading to the root of the directed graph contains only modeling checkers. Since Checkers.inc contains every checker that is a dependency, assert()ing whether the ProgramPointTag associated with the report is a dependency checker (given that we have at least one testcase for each checker that emits a report) would enforce that any report is emitted with the correct tag.</div><div>  b.) The problem that this wouldn't solve is modeling subcheckers, Making addTransition take the tag as a mandatory argument would help on this, but wouldn't *enforce* it, and woud result in a significant code duplication. We define subcheckers as checkers that do not have their own checker objects (they are basically glorified checker options), and I don't even have any ideas how we could catch these cases. There are two things that make this a tad bit better: For one, we don't have a checker like that just yet. For another, this would only affect developers when they are inspecting the ExplodedGraph, and with some experience, they may be able to catch and fix this.</div></div></blockquote><div><br></div><div>Realistically, this is such a low level issue, I don't think it's worth wasting development time on.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>  c.) This would pretty much make it so that disabling a checker would mean suppressing it's diagnostics, nothing else.</div><div><br></div><div>2. Making all modeling checkers hidden</div><div>  a.) Hidden checkers are defined as development only checkers. Riding on this excuse, I envision no expectations from end users regarding this. We mentioned that maybe if a dependency checker gets disabled but if later in the invocation a dependent checker is enabled it should reenable the dependency, but I think there is no need to implement this functionality if we enforce this rule along with the first one. Anybody who disables a development-only checker should know what that means, and any non-developer advised to do so is probably doing it to get rid of a crash or similar bad behavior.</div><div>  b.) Modeling checkers really are implementation details, and this move would make sure that whatever the user enables/disables, the analyzer would be responsible for any undesired side effects.</div><div><br></div><div>3. Allow checkers to depend on packages</div><div>Does this need any justification? We should be able to depend on whether the sun is out or not, but definitely on packages.</div><div><br></div><div>4. Create the hidden(!) coreModeling package, separate all the modeling from core to it, leaving core as a set of highly recommended, but no longer mandatory checkers. coreModeling would be a dependency of all pathsensitive checkers.</div><div>  a.) Remember how we need to remember to enable core in all test cases where at least a single pathsensitive checker is enabled? Well, from now on, **not** enabling core would be an even better idea, because we would have all the necessary modeling without the obstruction of core diagnostics. Also, one less thing to keep in mind!</div><div>  b.) "Make an interface easy to use correctly, and hard to use incorrectly" (Scott Meyers): This would be a drastic improvement in that department.</div><div>  c.) Don't allow any checker to directly depend on a coreModeling checker. This would allow us to evaluate whether there are any pathsensitive checkers enabled (which we can only do after we loaded everything else into CheckerManager) and enable coreModeling according to that. This would of course increase the pressure on codeModeling: if an error in this package slips into a release, we're screwed, though this has pretty much been the case ever since, my proposal only formalizes it a little better.</div><div><br class="m_3038164815671080475gmail-m_2572566777548704098gmail-Apple-interchange-newline">5. Regard some operation modifying the ProgramState as modeling operations, and regard checkers doing modeling operations as modeling checkers.</div><div>  a.) This would both make sure that the ExplodedGraph would remain the same aside from the diagnostic reports regardless of what non-developer, non-alpha checkers are enabled. We could come up with other heuristics as well, such as regarding checkers that add regular range constraints to a value to be regarded as modeling checkers.  </div></div></blockquote><div><br></div><div>Oops, meant to delete the second sentence add leave it as a separate point. Should proof read my emails better :)</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>  b.) Regard the creation of sink nodes as modeling operations. I bet we could somehow combine the function to create regular sink nodes and sink error nodes to allow bug reports to be both sink nodes and not be regarded as modeling checkers.</div><div>  c.) Modifications of regular range constraints are also modeling operations.</div><div>  d.) Document this well, make adding new modeling operations simple, and easy to remember for reviewers.</div></div></blockquote><div><br></div><div>Let's actually internalize this point, because know that I think about it, it rather talks about detecting whether a checker should reside in apiModeling, rather then simply categorizing checkers into modeling/diagnostic portions. Like, I plan to split UninitializedObjectChecker into a checker that emits the current default diagnostics, and turn the pointer chasing option into its own subchecker, while the actual logic would be moved to the hidden UninitializedObjectModeling checker. It's clear that the modeling portion wouldn't affect the rest of the analysis at all (hence we can disable it if both diagnostic checkers are also disabled), while a checker like DynamicMemoryModeling creates sinks and affects the analysis even when none of its subcheckers is enabled.<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
</blockquote></div>
</blockquote></div></div>