Dataflow: Address review comments.

This commit is contained in:
Anders Schack-Mulligen
2024-05-24 11:30:14 +02:00
parent 8085460e4a
commit 4ff37cc7b6
3 changed files with 17 additions and 10 deletions

View File

@@ -1369,6 +1369,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
CcCall ccSomeCall();
/*
* The following `instanceof` predicates are necessary for proper
* caching, since we're able to cache predicates, but not the underlying
* types.
*/
predicate instanceofCc(Cc cc);
predicate instanceofCcCall(CcCall cc);

View File

@@ -502,7 +502,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
)
}
private module CallSetsInput implements MkSetsInp {
private module CallSetsInput implements MkSetsInputSig {
class Key = TCallEdge;
class Value = DataFlowCall;
@@ -523,7 +523,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
private class CallSet = CallSetOption::Option;
private module DispatchSetsInput implements MkSetsInp {
private module DispatchSetsInput implements MkSetsInputSig {
class Key = TCallEdge;
class Value = TCallEdge;
@@ -585,10 +585,11 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
*
* There are four cases:
* - `TAnyCallContext()` : No restrictions on method flow.
* - `TSpecificCall(DataFlowCall call)` : Flow entered through the
* given `call`. This call improves the set of viable
* dispatch targets for at least one method call in the current callable
* or helps prune unreachable nodes in the current callable.
* - `TSpecificCall(CallSet calls, DispatchSet tgts, UnreachableSetOption unreachable)` :
* Flow entered through a specific call that improves the set of viable
* dispatch targets for all of `calls` to the set of dispatch targets in
* `tgts`, and/or the specific call prunes unreachable nodes in the
* current callable as given by `unreachable`.
* - `TSomeCall()` : Flow entered through a parameter. The
* originating call does not improve the set of dispatch targets for any
* method call in the current callable and was therefore not recorded.
@@ -1498,7 +1499,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
cached
int callOrder(DataFlowCall call) { result = call.totalorder() }
private module UnreachableSetsInput implements MkSetsInp {
private module UnreachableSetsInput implements MkSetsInputSig {
class Key = TCallEdge;
class Value = NodeRegion;

View File

@@ -5,7 +5,7 @@
*/
/** The input signature for `MakeSets`. */
signature module MkSetsInp {
signature module MkSetsInputSig {
class Key;
class Value;
@@ -31,7 +31,7 @@ signature module MkSetsInp {
* reasonable fallback where `getValueSet(k).contains(v)` remains equivalent to
* `v = getAValue(k)`.
*/
module MakeSets<MkSetsInp Inp> {
module MakeSets<MkSetsInputSig Inp> {
private import Inp
private int totalorderExt(Value v) {
@@ -53,7 +53,7 @@ module MakeSets<MkSetsInp Inp> {
private newtype TValList =
TValListNil() or
TValListCons(Value head, int r, TValList tail) { hasValListCons(_, head, r, tail) } or
TValListUnordered(Key k) { exists(getAValue(k)) and unordered(k) }
TValListUnordered(Key k) { unordered(k) }
private predicate hasValListCons(Key k, Value head, int r, TValList tail) {
rankedValue(k, head, r) and