diff --git a/share/prolog/oorules/guess.pl b/share/prolog/oorules/guess.pl index 60781d2c..fd992d3d 100644 --- a/share/prolog/oorules/guess.pl +++ b/share/prolog/oorules/guess.pl @@ -136,7 +136,7 @@ reportFirstSeen('guessVirtualFunctionCall'), minof((Insn, Constructor, OOffset, VFTable, VOffset), (likelyVirtualFunctionCall(Insn, Constructor, OOffset, VFTable, VOffset), - not(factNOTConstructor(Constructor)), + negation_helper(not(factNOTConstructor(Constructor))), doNotGuessHelper( factVirtualFunctionCall(Insn, Constructor, OOffset, VFTable, VOffset), factNOTVirtualFunctionCall(Insn, Constructor, OOffset, VFTable, VOffset)))), @@ -183,7 +183,7 @@ % ordering). osetof(VFTable, (possibleVFTable(VFTable), - not(factNOTVFTable(VFTable)), + negation_helper(not(factNOTVFTable(VFTable))), doNotGuessHelper(factVFTable(VFTable), factNOTVFTable(VFTable))), VFTableSet), @@ -701,13 +701,13 @@ guessClassHasNoDerivedA(Class) :- factConstructor(Constructor), - not(( + negation_helper(not(( factConstructor(OtherConstructor), validMethodCallAtOffset(_Insn, OtherConstructor, Constructor, _AnyOffset) - )), + ))), find(Constructor, Class), - not(factDerivedClass(_DerivedClass, Class, _SomeOffset)), + negation_helper(not(factDerivedClass(_DerivedClass, Class, _SomeOffset))), doNotGuessHelper(factClassHasNoDerived(Class), factClassHasUnknownDerived(Class)). @@ -736,13 +736,13 @@ factConstructor(Constructor), factVFTableWrite(_Insn1, Constructor, 0, VFTable), - not(( + negation_helper(not(( factVFTableWrite(_Insn2, Constructor, _Offset1, OtherVFTable), iso_dif(VFTable, OtherVFTable) - )), + ))), find(Constructor, Class), - not(factDerivedClass(Class, _BaseClass, _Offset2)), + negation_helper(not(factDerivedClass(Class, _BaseClass, _Offset2))), doNotGuessHelper(factClassHasNoBase(Class), factClassHasUnknownBase(Class)). @@ -786,7 +786,8 @@ find(_, Class), % Class does not have any base classes - not(factDerivedClass(Class, _Base, _Offset)), + % -10: Very low priority negation! + negation_helper(not(factDerivedClass(Class, _Base, _Offset)), -10), % XXX: If we're at the end of reasoning and there is an unknown base, is that OK? Should % we leave it as is? Try really hard to make a guess? Or treat it as a failure? @@ -809,7 +810,7 @@ find(_, Class), % Class does not have any derived classes - not(factDerivedClass(_DerivedClass, Class, _Offset)), + negation_helper(not(factDerivedClass(_DerivedClass, Class, _Offset))), % XXX: If we're at the end of reasoning and there is an unknown derived class, is that OK? % Should we leave it as is? Try really hard to make a guess? Or treat it as a failure? @@ -847,7 +848,8 @@ factMethodInVFTable(VFTable, _Offset1, Method), % One of the methods is in a class all by itself right now. - is_singleton(Method), + % XXX: Is this monotonic? + negation_helper(is_singleton(Method)), findVFTable(VFTable, Class), @@ -858,7 +860,7 @@ % If a method is in the vftable of a derived and base class, we should give priority to the % base class. - not(factDerivedClass(Class, _BaseClass, _Offset)). + negation_helper(not(factDerivedClass(Class, _BaseClass, _Offset))). guessLateMergeClasses(Out) :- reportFirstSeen('guessLateMergeClassesF1'), @@ -1111,10 +1113,10 @@ find(CalledMethod, CalledClass), % The called method does NOT install any vftables that are on the base class. - not(( + negation_helper(not(( find(BaseVFTable, BaseClass), factVFTableWrite(_Insn, CalledMethod, Offset, BaseVFTable) - )), + ))), % There does NOT exist a distinct class that also calls the called method. If this % happens, there is ambiguity about which derived class the CalledMethod should be placed % on, so it should probably go on the base. @@ -1267,10 +1269,10 @@ % Also ensure that the two methods not in a class relationship already. Merging them would % ultimately result in merging a class with it's own ancestor. - not(( + negation_helper(not(( reasonClassRelationship(Class1, Class2); reasonClassRelationship(Class2, Class1) - )), + ))), checkMergeClasses(Class1, Class2), @@ -1314,7 +1316,7 @@ setof(Class, Insn2^Offset2^Method2^( factVFTableWrite(Insn2, Method2, Offset2, VFTable), - not(factVFTableOverwrite(Method2, _OtherVFTable, VFTable, Offset2)), + negation_helper(not(factVFTableOverwrite(Method2, _OtherVFTable, VFTable, Offset2))), find(Method2, Class), iso_dif(Class1, Class)), ClassSet), @@ -1365,8 +1367,9 @@ factNOTMergeClasses(Class2, Class1)), % XXX: Check factMergeClasses? % Now relationships between the classes are not allowed either. - not(reasonClassRelationship(Class1, Class2)), - not(reasonClassRelationship(Class2, Class1)). + % XXX: negation_helper? + negation_helper(not(reasonClassRelationship(Class1, Class2))), + negation_helper(not(reasonClassRelationship(Class2, Class1))). tryMergeClasses((Method1, Method2)) :- tryMergeClasses(Method1, Method2). % If we are merging classes that have already been merged, just ignore it. @@ -1564,10 +1567,10 @@ % guessDeletingDestructor requires a call to a real destructor. This rule relaxes that a % bit, by ensuring we don't call any non-real destructors. So calling a real destructor % will trigger this rule, but it is not necessary. - not(( + negation_helper(not(( callTarget(_Insn1, Method, Called), not(factRealDestructor(Called)) - )), + ))), !, Out = tryOrNOTDeletingDestructor(Method). @@ -1632,7 +1635,7 @@ % This indicates that the method met some basic criteria in C++. possibleDestructor(DeletingDestructor), % That's not already certain to NOT be a deleting destructor. - not(factNOTDeletingDestructor(DeletingDestructor)), + negation_helper(not(factNOTDeletingDestructor(DeletingDestructor))), % And the deleting destructor must also call delete (we think), since that's what makes it % deleting. Using this instead of the more complicated rule below led toa very slight % improvement in the fast test suite F=0.43 -> F=0.44. @@ -1661,9 +1664,75 @@ % And while it's premature to require the real destructor to be certain, it shouldn't be % disproven. possibleDestructor(RealDestructor), - not(factNOTRealDestructor(RealDestructor)), + negation_helper(not(factNOTRealDestructor(RealDestructor))), true. +tryDelay((G,P,Commit)) :- + try_retract(delay_queue(G, P, Commit)), + + % Do nothing if we've already committed one way or the other + %% (not(G) -> true; + %% delay_goal(G, _) -> true; + %% delay_fail(G) -> true; + + loginfoln('Guessing ~Q.', delay_goal(G, Commit)), + try_assert(delay_goal(G, Commit)). + +tryNOTDelay((G,P)) :- + loginfoln('tryNOTDelay'), + try_retract(delay_queue(G, P, Commit)), + + % Do nothing if we've already committed one way or the other + %% (not(G) -> true; + %% delay_goal(G, _) -> true; + %% delay_fail(G) -> true; + + loginfoln('Guessing ~Q.', delay_fail(G)), + try_assert(delay_fail(G)). + +tryOrNOTDelay((G, P)) :- + % XXX Optimization for not(G)... + + try_retract(delay_queue(G, P)), + + % Do nothing if we've already committed one way or the other + delay_goal(G, _) -> true; + delay_fail(G) -> true; + + ( + tryDelay(G); + tryNOTDelay(G); + logwarnln('Something is wrong upstream: ~Q.', delay(Method)), + fail + ). + +guessDelay(Out) :- + reportFirstSeen('guessDelay'), + + % Remove each false or already committed to delay + forall(delay_queue(G, P, Commit), + ((not(G); + delay_goal(G, _); + delay_fail(G)) + -> (logdebugln('Removing outdated delay goal ~Q', [G]), + retract(delay_queue(G, P, Commit))) + ; true)), + + !, + + setof(P, delay_queue(_, P, _), Pset), + max_list(Pset, Pmax), + + % Sorting the queue takes a while. We should really use a priority queue... + % but this hack works ok for now. + %member(Pmax, [0, -10, _]), + + setof((G, Pmax, Commit), + delay_queue(G, Pmax, Commit), + Gset), + + Out = tryBinarySearch(tryDelay, tryNOTDelay, Gset). + %% Local Variables: %% mode: prolog %% End: diff --git a/share/prolog/oorules/insanity.pl b/share/prolog/oorules/insanity.pl index b99cef92..a9abdaf9 100644 --- a/share/prolog/oorules/insanity.pl +++ b/share/prolog/oorules/insanity.pl @@ -328,6 +328,18 @@ factEmbeddedObject(A, B, C)) ). +% We committed to a condition being true (or false). Make sure that it stays +% that way. +:- table insanityNegation/1 as incremental. +insanityNegation(Out) :- + delay_goal(G, true), + + not(G), + + Out = ( + logwarnln('Consistency checks failed.~nThe condition "~Q" was committed to, but has become false.~n', [G]) + ). + :- table sanityChecks/1 as incremental. sanityChecks(Out) :- insanityNoBaseConsistency(Out); @@ -346,7 +358,8 @@ insanityInheritanceLoop(Out); insanityContradictoryMerges(Out); insanityContradictoryNOTConstructor(Out); - insanityTwoRealDestructorsOnClass(Out). + insanityTwoRealDestructorsOnClass(Out); + insanityNegation(Out). sanityChecks :- sanityChecks(Out) diff --git a/share/prolog/oorules/rules.pl b/share/prolog/oorules/rules.pl index d3707ea6..065d3569 100644 --- a/share/prolog/oorules/rules.pl +++ b/share/prolog/oorules/rules.pl @@ -758,7 +758,7 @@ % There is some offset for which there is a single vftable write and a thiscall to the same % offset factVFTableWrite(WriteAddr, Method, Offset, VFTable), - not((factVFTableWrite(_, Method, Offset, VFTable2), iso_dif(VFTable, VFTable2))), + negation_helper(not((factVFTableWrite(_, Method, Offset, VFTable2), iso_dif(VFTable, VFTable2)))), methodCallAtOffset(CallAddr, Method, Callee, Offset), % ejs 1/08/21: I believe that Offset can not be negative for a constructor or destructor @@ -996,7 +996,7 @@ % directly instantiated, because the "no other class trying to install this vftable" will % be trivially true, and without this clause, the vftable will simply belong to an % arbitrary method that installs it. - not(factVFTableOverwrite(Method, VFTable, _OverwriteVFTable, Offset)), + negation_helper(not(factVFTableOverwrite(Method, VFTable, _OverwriteVFTable, Offset))), % Constructors may inline embedded constructors. If non-offset % zero, we must make sure that there is an inherited class at this @@ -1029,7 +1029,7 @@ % embedded objects at offset 0, then we must own the vftable. (Offset = 0, (factNOTEmbeddedObject(Class, _AnyClass, 0); % Not ideal... - not(factEmbeddedObject(Class, _AnyClass2, 0))))), + negation_helper(not(factEmbeddedObject(Class, _AnyClass2, 0)))))), % VFTables from a base class can be reused in a derived class. If this happens, we know % that the VFTable does not belong to the derived class. @@ -1059,6 +1059,7 @@ % Alternatively, if we are a destructor, make sure there is no other class trying to % install this vftable % XXX: Should Offset = Offset2? + % Use negation_helper? (forall(factVFTableWrite(_Insn5, Method2, Offset2, VFTable), % It is ok to ignore overwritten vftables (factVFTableOverwrite(Method2, VFTable, _OtherVFTable, Offset2); @@ -1095,7 +1096,7 @@ % directly instantiated, because the "no other class trying to install this vftable" will % be trivially true, and without this clause, the vftable will simply belong to an % arbitrary method that installs it. - not(factVFTableOverwrite(Method, VFTable, _OverwriteVFTable, Offset)), + negation_helper(not(factVFTableOverwrite(Method, VFTable, _OverwriteVFTable, Offset))), % Constructors may inline embedded constructors. If non-offset % zero, we must make sure that there is an inherited class at this @@ -1128,7 +1129,7 @@ % embedded objects at offset 0, then we must own the vftable. (Offset = 0, (factNOTEmbeddedObject(Class, _AnyClass, 0); % Not ideal... - not(factEmbeddedObject(Class, _AnyClass2, 0))))), + negation_helper(not(factEmbeddedObject(Class, _AnyClass2, 0)))))), % VFTables from a base class can be reused in a derived class. If this happens, we know % that the VFTable does not belong to the derived class. @@ -1545,7 +1546,7 @@ % Prevent grand ancestors from being decalred object in object. See commentary below. % It's unclear of this constraint is really required in cases where Offset is non-zero. - not(reasonClassRelationship(OuterClass, InnerClass)), + negation_helper(not(reasonClassRelationship(OuterClass, InnerClass))), % Debugging logtraceln('~@~Q.', [not(factObjectInObject(OuterClass, InnerClass, Offset)), @@ -1576,7 +1577,8 @@ % same class. And there doesn't appear be any downside either since there's already an % ObjectInObject at the appropriate offset, and we can reach the right conclusions through % those later class merges. - not(factObjectInObject(OuterClass, _, Offset)), + % negation: hmm, this rule sounds weird. + negation_helper(not(factObjectInObject(OuterClass, _, Offset))), factConstructor(InnerConstructor), iso_dif(InnerConstructor, OuterConstructor), @@ -1777,11 +1779,11 @@ factVFTableWrite(_Insn1, DerivedConstructor, ObjectOffset, DerivedVFTable), % No one overwrites the vftable - not(factVFTableOverwrite(DerivedConstructor, DerivedVFTable, _OverwrittenDerivedVFTable, ObjectOffset)), + negation_helper(not(factVFTableOverwrite(DerivedConstructor, DerivedVFTable, _OverwrittenDerivedVFTable, ObjectOffset))), ((factVFTableWrite(_Insn2, BaseConstructor, 0, BaseVFTable), % No one overwrites the vftable - not(factVFTableOverwrite(BaseConstructor, BaseVFTable, _OverwrittenBaseVFTable, 0)), + negation_helper(not(factVFTableOverwrite(BaseConstructor, BaseVFTable, _OverwrittenBaseVFTable, 0))), % And the vtables values written were different iso_dif(DerivedVFTable, BaseVFTable)); % Right now we assume that if a class inherits from an imported class, the base class is @@ -1796,7 +1798,7 @@ find(BaseConstructor, BaseClass), % There's not already a relationship. (Prevent grand ancestors) - not(reasonClassRelationship(DerivedClass, BaseClass)), + negation_helper(not(reasonClassRelationship(DerivedClass, BaseClass))), % Debugging logtraceln('~@DEBUG Derived VFTable: ~Q~n Base VFTable: ~Q~n Derived Constructor: ~Q~n Base Constructor: ~Q', @@ -1945,7 +1947,7 @@ factConstructor(DerivedConstructor), % The derived constructor does not write a vftable at offset 0 - not(factVFTableWrite(_Insn, DerivedConstructor, 0, _DVFTable)), + negation_helper(not(factVFTableWrite(_Insn, DerivedConstructor, 0, _DVFTable))), % The base class has a primary vftable find(BaseConstructor, BaseClass), @@ -2251,13 +2253,14 @@ % information about the direction of that relationship. :- table reasonClassRelatedMethod/2 as incremental. :- table reasonClassRelatedMethod_A/2 as incremental. -%:- table reasonClassRelatedMethod_B/2 as incremental. +:- table reasonClassRelatedMethod_B/2 as incremental. :- table reasonClassRelatedMethod_C/2 as incremental. reasonClassRelatedMethod(Class, Method) :- reasonClassRelatedMethod_A(Class, Method); % _B is now a trigger rule - %reasonClassRelatedMethod_B(Class, Method); + % Re-enabled (temporarily) for negation branch + reasonClassRelatedMethod_B(Class, Method); reasonClassRelatedMethod_C(Class, Method). % ClassCallsMethod => ClassRelatedMethod @@ -2268,6 +2271,9 @@ thisPtrUsage(Function, ThisPtr, Method) :- thisPtrUsage(_, Function, ThisPtr, Method). +reasonClassRelatedMethod_B(Class1, Method2) :- + reasonClassRelatedMethod_B(Class1, _, _, Method2). + % Because two methods are called on the same this-pointer in the same function. This rule is % NOT direction safe, because it simply observes two methods being called on the same object % pointer, and does not account for inheritance relationships. @@ -2300,10 +2306,10 @@ % ejs 2/12/21 Adding a more conservative (but possibly unnecessary) check for ANY object at % offset 0 (instead of Class1). - not((find(Function, FunctionClass), factObjectInObject(FunctionClass, _InnerClass1, 0))), + negation_helper(not((find(Function, FunctionClass), factObjectInObject(FunctionClass, _InnerClass1, 0)))), % We also need to verify that Class2 has no object at 0. - not((factObjectInObject(Class2, _InnerClass2, 0))), + negation_helper(not((factObjectInObject(Class2, _InnerClass2, 0)))), % Functions that are methods can call base methods @@ -2511,10 +2517,10 @@ find(VFTable1, Class1), find(VFTable2, Class2), iso_dif(Class1, Class2), - not(( + negation_helper(not(( reasonClassRelationship(Class1, Class2); reasonClassRelationship(Class2, Class1) - )), + ))), logtraceln('~@~Q.', [ not(factReusedImplementation(Method)), @@ -2534,10 +2540,10 @@ %possiblyReused(Method), factMethodInVFTable(VFTable1, _Offset1, Method), factMethodInVFTable(VFTable2, _Offset2, Method), - not(( + negation_helper(not(( reasonClassRelationship(Class1, Class2); reasonClassRelationship(Class2, Class1) - )), + ))), logtraceln('~@~Q.', [ not(factReusedImplementation(Method)), @@ -2647,7 +2653,7 @@ % Which has a Method factMethodInVFTable(BaseVFTable, _Offset, Method), not(purecall(Method)), - not(factReusedImplementation(Method)), + negation_helper(not(factReusedImplementation(Method))), % We don't have to check purecall because factMethodInVFTable does already @@ -2673,14 +2679,14 @@ % If we have no bases, it can't be on a base class. factClassHasNoBase(Class), % And if there's no object (embedded or base?) at offset zero... - not(factObjectInObject(Class, _0InnerClass, 0)), + negation_helper(not(factObjectInObject(Class, _0InnerClass, 0))), find(Method, ExistingClass), iso_dif(Class, ExistingClass), % Confusingly, the method's class must also have no base and no object at offset zero, % because the method being called could actually be the base class method... factClassHasNoBase(ExistingClass), - not(factObjectInObject(ExistingClass, _0InnerClass, 0)), + negation_helper(not(factObjectInObject(ExistingClass, _0InnerClass, 0))), % Debugging logtraceln('~@~Q.', [not(find(Class, ExistingClass)), @@ -2693,6 +2699,7 @@ % inverse rule under reasonNOTMergeClasses. % PAPER: Merging-4 reasonMergeClasses_E(Class1, Class2) :- + fail, factDerivedClass(DerivedClass, Class1, ObjectOffset), factDerivedClass(DerivedClass, Class2, ObjectOffset), iso_dif(Class1, Class2), @@ -2749,7 +2756,7 @@ % need to sum the sizes of the base class vftables, be confident in their layout order, and % no that there aren't any other complexities involving multiple inheritance. In the mean % time, just disable this rule where there's more than one base class. - not((factDerivedClass(DerivedClass, OtherBase, _OtherOffset), iso_dif(OtherBase, BaseClass))), + negation_helper(not((factDerivedClass(DerivedClass, OtherBase, _OtherOffset), iso_dif(OtherBase, BaseClass)))), findVFTable(DerivedVFTable, 0, DerivedClass), findVFTable(BaseVFTable, 0, BaseClass), @@ -2758,7 +2765,7 @@ % There's an entry in the derived vftable that's to big to be in the base vftable. factVFTableEntry(DerivedVFTable, VOffset, Method), not(purecall(Method)), - not(factReusedImplementation(Method)), + negation_helper(not(factReusedImplementation(Method))), VOffset > BaseSize, find(Method, MethodClass), iso_dif(DerivedClass, MethodClass), @@ -2993,8 +3000,8 @@ % But one counter example that we need to protect against is the inlining of base class % VFTable writes. The intention here is very similar to factVFTableOverwrite, but without % the complications of caring which value overwrote which other value. - not((factVFTableWrite(_Insn3, Method1, 0, VFTable2))), - not((factVFTableWrite(_Insn4, Method2, 0, VFTable1))), + negation_helper(not((factVFTableWrite(_Insn3, Method1, 0, VFTable2)))), + negation_helper(not((factVFTableWrite(_Insn4, Method2, 0, VFTable1)))), % Debugging logtraceln('~@~Q.', [not(dynFactNOTMergeClasses(Class1, Class2)), reasonNOTMergeClasses_E(Class1, Class2)]). @@ -3174,6 +3181,7 @@ factMethod(Method), iso_dif(Method, Caller), (factConstructor(Method); + % XXX negation_helper here? (factDeletingDestructor(Method), not(factRealDestructor(Caller))); factRealDestructor(Method)), % Handle symmetry @@ -3445,7 +3453,7 @@ % Ideally we'd want a stronger statement here to ensure there is no embedded object. But % at least make sure we don't currently have one. - not(factObjectInObject(_Derived, Class, 0)), + negation_helper(not(factObjectInObject(_Derived, Class, 0))), Debug=nobaseorderived. diff --git a/share/prolog/oorules/setup.pl b/share/prolog/oorules/setup.pl index d6fdb22a..9484a084 100644 --- a/share/prolog/oorules/setup.pl +++ b/share/prolog/oorules/setup.pl @@ -579,7 +579,10 @@ % class that we have not identified a base class for. guessCommitClassHasNoBase(Out); % Same thing for Derived classes - guessCommitClassHasNoDerived(Out) + guessCommitClassHasNoDerived(Out); + + % Commit to a negation + guessNegation(Out) )), diff --git a/share/prolog/oorules/util.pl b/share/prolog/oorules/util.pl index e77fda83..596043cd 100644 --- a/share/prolog/oorules/util.pl +++ b/share/prolog/oorules/util.pl @@ -5,6 +5,56 @@ :- use_module(library(lists), [append/3, nth1/4, list_to_set/2]). +% Delayed and committed negations. The following code is used to indicate a delayed check, +% which is how it sounds. A delayed check may optionally be committed to, which ensures that +% the check can not become false in the future. + +:- dynamic delay_queue/3. + +:- dynamic delay_fail/1. + +%:- dynamic delay_commit/1 as incremental. + +% delayed_goal(Goal, Commit). Commit=true iff the goal should never become false in the +% future. +:- dynamic delay_goal/2 as incremental. + +%delay_helper(G) :- delay_helper(G, 0, false). + +delay(G) :- delay_helper(G, 0, false). + +delay_and_commit(G) :- delay_and_commit(G, 0). + +delay_and_commit(G, P) :- delay_helper(G, P, true). + +delay_helper(G, _, _) :- + var(G) -> throw_with_backtrace(user_error(delay_helper)). + +% We've already delayed for G +delay_helper(G, _, _) :- + delay_goal(G, _), + logtraceln('Already delayed ~Q', G), + !. + +% G results in a sanity failure +delay_helper(G, _, _) :- + delay_fail(G), !, fail. + +% G isn't true right now. +delay_helper(G, _, _) :- + not(G), !, fail. + +% Queue G and fail. +delay_helper(G, P, Commit) :- + !, + (delay_queue(G, OldP, Commit), P >= OldP) + % There is a better or same priority queued element + -> fail + ; logdebugln('I am queueing delay ~Q', G), + assert(delay_queue(G, P, Commit)), + fail. + + sort_tuple((A,B), (C,D)) :- (A < B -> (C=A, D=B); (C=B, D=A)).