Consistency checks failed in ooprolog.

[kristof-mattei]

reasonForwardAsManyTimesAsPossible complete.
Entering stage 'Initial reasoning complete'.
Consistency checks failed.
Class 0x7ed10c inherits from 0x7e528c at offsets 0 and 0x58
Initial sanity check failed, indicating the OO rules are incorrect.
Please report this failure to the Pharos developers!
  [29] prolog_stack:get_prolog_backtrace(100,[frame(29,clause(<clause>(0x5653afe10bf0),6),_264821938)|_264821926],[goal_term_depth(100)]) at /usr/local/lib/swipl/library/prolog_stack.pl:137
  [28] throw_with_backtrace(error(system_error(initialSanityChecks))) at /usr/local/share/pharos/prolog/oorules/util.pl:185
  [26] solve_internal at /usr/local/share/pharos/prolog/oorules/setup.pl:679
  [25] catch(user:solve_internal,_264822162,user:((_264822230=error(resource_error(private_table_space),_264822244)->complain_table_space(ooscript);_264822294=error(resource_error(stack),_264822308)->complain_stack_size(ooscript);true),throw(_264822340))) at /usr/local/lib/swipl/boot/init.pl:562
  [24] solve(ooscript) at /usr/local/share/pharos/prolog/oorules/setup.pl:617
  [23] psolve_no_halt('<garbage_collected>') at /usr/local/share/pharos/prolog/oorules/report.pl:23
  [22] catch(user:psolve_no_halt(stream(<stream>(0x5653afe3c3c0))),_264822514,user:(print_message(error,_264822580),(globalHalt->halt(1);true))) at /usr/local/lib/swipl/boot/init.pl:562
  [21] catch_with_backtrace('<garbage_collected>','<garbage_collected>','<garbage_collected>') at /usr/local/lib/swipl/boot/init.pl:629
  [20] run_with_backtrace('<garbage_collected>') at /usr/local/bin/ooprolog:177
  [19] <meta call>
  [18] with_output_to(<stream>(0x5653affa7490),run_with_backtrace(psolve_no_halt(stream(<stream>(0x5653afe3c3c0))))) <foreign>
  [17] setup_call_catcher_cleanup(user:(var('/to_analyze/gamemd-results.pl')->open_null_stream(<stream>(0x5653affa7490));open('/to_analyze/gamemd-results.pl',write,<stream>(0x5653affa7490))),user:with_output_to(<stream>(0x5653affa7490),run_with_backtrace(psolve_no_halt(stream(<stream>(0x5653afe3c3c0))))),_264822932,user:close(<stream>(0x5653affa7490))) at /usr/local/lib/swipl/boot/init.pl:663
  [15] setup_call_catcher_cleanup(user:open('/to_analyze/gamemd-facts.pl',read,<stream>(0x5653afe3c3c0)),user:setup_call_cleanup((var('/to_analyze/gamemd-results.pl')->open_null_stream(<stream>(0x5653affa7490));open('/to_analyze/gamemd-results.pl',write,<stream>(0x5653affa7490))),with_output_to(<stream>(0x5653affa7490),run_with_backtrace(psolve_no_halt(stream(<stream>(0x5653afe3c3c0))))),close(<stream>(0x5653affa7490))),_264823142,user:close(<stream>(0x5653afe3c3c0))) at /usr/local/lib/swipl/boot/init.pl:663
  [12] run([script('/usr/local/bin/ooprolog'),json(_264823420),ground(_264823440),rtti(true),guess(true),config(_264823500),stacklimit(200000000000),tablespace(200000000000),oorulespath(_264823560),halt(true),load_only(false),help(_264823620),facts('/to_analyze/gamemd-facts.pl'),results('/to_analyze/gamemd-results.pl'),loglevel(6)]) at /usr/local/bin/ooprolog:235
   [9] catch(user:main(['/usr/local/bin/ooprolog','--facts','/to_analyze/gamemd-facts.pl','--results','/to_analyze/gamemd-results.pl','--log-level=6']),_264823744,user:(print_message(error,_264823874),halt(1))) at /usr/local/lib/swipl/boot/init.pl:562
   [7] catch(user:main,_264823948,'$toplevel':true) at /usr/local/lib/swipl/boot/init.pl:562
   [6] catch_with_backtrace('<garbage_collected>','<garbage_collected>','<garbage_collected>') at /usr/local/lib/swipl/boot/init.pl:629

Note: some frames are missing due to last-call optimization.
Re-run your program in debug mode (:- debug.) to get more detail.
ERROR: /to_analyze/gamemd-facts.pl:496955:
ERROR:    Unknown message: error(system_error(initialSanityChecks))

Commands:

$ partition --serialize=/to_analyze/gamemd.ser --maximum-memory=19000 --no-semantics /to_analyze/gamemd.exe
$ ooanalyzer --serialize=/to_analyze/gamemd.ser --maximum-memory=19000 --no-semantics --prolog-facts=/to_analyze/gamemd-facts.pl --per-function-timeout=60 --delete-method=0x7C8B3D --new-method=0x7c8e17 /to_analyze/gamemd.exe
$ ooprolog --facts /to_analyze/gamemd-facts.pl --results /to_analyze/gamemd-results.pl --log-level=6 > /to_analyze/output.log

Let me know what I can execute to help to get more info!

[sei-eschwartz]

Could you provide the gamemd-facts.pl file? It's hard to do much without this.

It would also be helpful to have gamemd.exe

[kristof-mattei]

gamemd.exe.gz gamemd-facts.pl.gz

[sei-eschwartz]

Thank you. Do you know approximately how long it took to reach the problem?

[sei-eschwartz]

Nevermind, I was able to reproduce it!

[sei-eschwartz]

Contradictory information about constructor: factConstructor(0x4770e0) but reasonNOTConstructor(0x4770e0)

reasonConstructor_D(0x4770e0).
reasonNOTConstructor_I(0x4770e0).

% Because we see that a base class constructor is called before a vftable is installed.
reasonConstructor(Method) :-
    certainConstructorOrDestructorInheritanceSpecialCase(Method, constructor),
    logtraceln('~@~Q.', [not(factConstructor(Method)), reasonConstructor_D(Method)]).

% Because we see a base class destructor is called after a vftable is installed.
reasonNOTConstructor_I(Method) :-
    certainConstructorOrDestructorInheritanceSpecialCase(Method, destructor),
    logtraceln('~@~Q.', [not(factNOTConstructor(Method)),
                         reasonNOTConstructor_I(Method)]).

So... that's weird. certainConstructorOrDestructorInheritanceSpecialCase is supposed to distinguish between constructors and destructors, not trigger for both!

[sei-eschwartz]

This is the thisptr of that method:

funcParameter(0x4770e0, ecx, sv_2291049953129467751).

The problem is that there are multiple method calls:

callParameter(0x4773cb, 0x4770e0, ecx, sv_2291049953129467751).
callParameter(0x477413, 0x4770e0, ecx, sv_2291049953129467751).

The VFTable write is at 0x4773d9, which falls in between. In reality, only 0x4773d9 and 0x4773cb are in the same block. This suggests that the call is first, and so this is a constructor.

Anyway, the solution is to make sure there are not multiple method calls. I have a branch here that I am testing: https://github.com/sei-eschwartz/pharos/tree/issue240

[sei-eschwartz]

Another problem.

Consistency checks failed.
Contradictory information about merging classes: Method1=0x7ef7f0 Method2=0x7e5c24

      1 reasonMergeClasses_K(0x7e5c24, 0x7ef7f0, 0x628df0).
      1 reasonNOTMergeClasses_I(0x81f240, 0x836478, 0x7e5c24, 0x7ef7f0).

% If two methods are present on the same object, and we know neither method's class has a base
% class, the methods must be on the same object.
reasonMergeClasses_K(Class1, Class2) :-

% Because RTTI tells us that they're different classes.
% XXX PAPER: RTTI
reasonNOTMergeClasses_I(Class1, Class2) :-

[sei-eschwartz]

rTTINoBaseName(0x81f240, '.?AV?$VectorClass@PAD@@')
rTTINoBaseName(0x836478, '.?AV?$VectorClass@VHSVClass@@@@').

.?AV?$VectorClass@VHSVClass@@@@
.?AV?$VectorClass@VHSVClass@@@@ class VectorClass<class HSVClass>
.?AV?$VectorClass@PAD@@   
.?AV?$VectorClass@PAD@@ class VectorClass<near char *>

So there are two template instantiations. I haven't looked yet, but I bet 0x628df0 is a method on the class that doesn't depend on the template arguments.

[sei-eschwartz]

The problem seems to be in function 0x626c60. It appears to call new on two different objects. For some reason, we don't assign a symbolic value to the return of new. You can see this here in the facts:

insnCallsNew(0x626c70, 0x626c60, invalid).
insnCallsNew(0x626c8c, 0x626c60, invalid).
insnCallsNew(0x626cc8, 0x626c60, invalid).
insnCallsNew(0x626cfa, 0x626c60, invalid).
insnCallsNew(0x626d1e, 0x626c60, invalid).

Here are some other facts that imply we're doing stuff to the same object, but actually these are for separate heap allocations:

callParameter(0x626ca0, 0x626c60, ecx, sv_6655002938392236482).
callParameter(0x626cdc, 0x626c60, ecx, sv_6655002938392236482).

So this is a fact problem. This is where I usually reach out to @sei-ccohen for help. I'm not sure why this would happen. Is it possible that you hit a memory or time limit on function 0x626c60?

[kristof-mattei]

Let me re-run with more time! Memory is harder, but I can fire up a VM in the cloud.

[sei-eschwartz]

I just wanted to say we're still looking into this. It doesn't seem to be a resource issue. But rather, functions are not being analyzed in the order that we expected.

[kristof-mattei]

@sei-eschwartz I really appreciate it. Let me know if I need to rerun stuff.

[edmcman]

@sei-mwd made some progress. For some reason, Pharos thinks that there are out going function calls from memcpy, when there does not appear to be. This results in a cycle, which we break in an inconvenient way and causes the problem you are encountering. The next question is why are we getting these (invalid) out going function calls?

[edmcman]

Specifically, Pharos thinks that memcpy (0x7ca090) calls function 0x44acf0.

[sei-eschwartz]

This problem appears to be present in stock ROSE too.
gamemd.pdf

Note the edge from 0x7ca252 to 0x498d00 which looks pretty suspicious to me. I don't even think 0x498d00 is an aligned instruction.

[sei-eschwartz]

0x7ca252 appears to use a jump table, but it's a little bit odd because the index is negated. IDA actually gets confused and says there is only one switch case. ROSE does better, but unfortunately fails to detect the end (the lowest address) of the table, which is at 0x007CA304. Instead, it looks at 0x7ca300. which contains 00 8D 49 00. According to IDA, the first 00 byte is part of the instruction:

007CA2FA jmp ds:jpt_7CA274[edx*4] ; switch 4 cases

I am not sure what the other three bytes are for. IDA says they are alignment. But if that is so, why wouldn't they be null?

[sei-eschwartz]

8D 49 00 disassembles to lea ecx, [ecx], which is a noop. It doesn't make much sense because immediately following the noop is a code pointer, not code. But maybe it's some anti disassembly attempt?

From Ghidra:

                             switchD_007ca2fa::switchD
        007ca2fa ff 24 95        JMP        dword ptr [EDX*0x4 + ->switchD_007ca274::caseD_0]                    = 007ca380
                 70 a3 7c 00
                                                      $U2080:4 = INT_MULT EDX, 4:4
                                                      $U2180:4 = INT_ADD 0x7ca370:4, $U2080:4
                                                      $U7a00:4 = LOAD ram($U2180:4)
                                                      BRANCHIND $U7a00:4
        007ca301 8d 49 00        LEA        ECX,[ECX]
                                                      ECX = COPY ECX
        007ca304 24 a3 7c 00     addr       LAB_007ca324
        007ca308 2c a3 7c 00     addr       LAB_007ca32c
        007ca30c 34 a3 7c 00     addr       LAB_007ca334
        007ca310 3c a3 7c 00     addr       LAB_007ca33c
        007ca314 44 a3 7c 00     addr       LAB_007ca344
        007ca318 4c a3 7c 00     addr       LAB_007ca34c
        007ca31c 54 a3 7c 00     addr       LAB_007ca354

[sei-eschwartz]

The ROSE maintainer says that he has fixed this internally, and will be pushing the fix out soon.

[kristof-mattei]

Awesome. I'll wait for the fix and re-try.

[sei-eschwartz]

It looks like this finally went live https://github.com/rose-compiler/rose/commit/06d18de547b51acb623d771c4732ab3eaf8ee30d

[sei-mwd]

Yes, the necessary change made it into ROSE, but we can't test it yet because some other API changes are needed before Pharos can be compiled against the ROSE tip again. (Specifically, Engine needs its constructors to be protected rather than private.) The ROSE devs know this, but it hasn't made it to Github yet.

[kristof-mattei]

@sei-eschwartz thanks for the update @sei-mwd thanks! Looking for the updated release!