Could you tell me why this has only 1 path?

[Rumata888]

from symbolic.args import *

@symbolic(a=0xdeaddeaddeaddead,b=0xbeefbeefbeefbeef)
def expandKey(a,b):
    i=0;
    passkeyn=[a,b]

    expandedkey=[]
    while i<6:
        expandedkey=expandedkey+passkeyn
        i=i+1
        v1=passkeyn[0]
        v2=passkeyn[1]
        v3=(v1>>0x30)|(((v1>>0x20)&0xffff)<<0x10)|(((v1>>0x10)&0xffff)<<0x20)|((v1&0xffff)<<0x30)
        v4=(v2>>0x30)|(((v2>>0x20)&0xffff)<<0x10)|(((v2>>0x10)&0xffff)<<0x20)|((v2&0xffff)<<0x30)
        v5 = ((v4 & 0xFFFFFF8000000000) >> 39) | ((v3 << 25)&0xffffffffffffffff);
        v6 = ((v3 & 0xFFFFFF8000000000) >> 39) | ((v4 << 25)&0xffffffffffffffff);
        v1=(v5>>0x30)|(((v5>>0x20)&0xffff)<<0x10)|(((v5>>0x10)&0xffff)<<0x20)|(((v4 & 0xFFFFFF8000000000) >> 39)<<0x30)
        v2=(v6>>0x30)|(((v6>>32)&0xffff)<<0x10)|(((v6>>0x10)&0xffff)<<0x20)|(((v3 & 0xFFFFFF8000000000) >> 39)<<0x30)
        passkeyn=[v1,v2]
    expandedkey=expandedkey+passkeyn
    if expandedkey==[16045725885737590445, 13758425323549998831, 7044313620519854103485, 8215411798635391606653, 8245388070021240879798, 3384596836810669685695, 9287860625795901259255, 4527376222128629444341, 4093654381503457390331, 4647353382867023162077, 8665057901351565392853, 8816957627389395711965, 6783497306152038280055, 9291067819851303074799]:
        return 1
    return 2

[tballmsft]

Can you tell me why you expect it to have two paths? It's not immediately obvious.

[Rumata888]

the values, which are described in @(symbolic) are the ones that produce this result

[Rumata888]

I checked, it can deal with lists. But it seems to get into a real problem in here. It extends both values to 64 bits, but it still only uses zero values. That seems strange, as the rules can be clearly derived form equations

[tballmsft]

The zero values are the initial default values. I believe that the reason it is not finding the second path is that it limits the search to 64 bits, so it cannot properly solve the bit shifting operations. You could experiment with increasing the bitwidth. Best,

n Tom

From: Innokentiy Sennovskiy [mailto:[email protected]] Sent: Wednesday, May 6, 2015 1:02 AM To: thomasjball/PyExZ3 Cc: Tom Ball (MSR) Subject: Re: [PyExZ3] Could you tell me why this has only 1 path? (#17)

I checked, it can deal with lists. But it seems to get into a real problem in here. It extends both values to 64 bits, but it still only uses zero values. That seems strange, as the rules can be clearly derived form equations

— Reply to this email directly or view it on GitHubhttps://github.com/thomasjball/PyExZ3/issues/17#issuecomment-99365697.