s2e crashes in strcmp when I add FunctionModels in configure file

[JodieAllen]

Hi~, when I try to explore all paths in binary (which includes strcmp) with s2e, I meet a crash if I write add_plugin("FunctionModels") in s2e-config.lua and the s2e stops. ( I run s2e in ubuntu14.04 and x86_64.)

my test file as below (c file):

int main(int argc, const char * argv[]) {
    char str1[15];
    char str2[15];
    int ret = 0;
    strcpy(str1,argv[1]);
    strcpy(str2,"ABCDE");
   
    ret = strcmp(str1,str2);
    if(ret > 0 )
    {
        printf("> 0");
    }
    else if(ret < 0){
        printf("< 0");
    }
    else{
        printf("== 0");
    }
    return 0;
       
}

my commands as following, I set the arg[1] to be symbol: s2e new_project -i debian-9.2.1-x86_64 -a="1" ~/my_s2e_test_pro/jodietest/scmp_symargv "xxxx"

then I write add_plugin("FunctionModels") in s2e-config.lua and run ./launch-s2e.sh

the crash as following:

4 [State 0] BaseInstructions: Inserted symbolic data @0x7ffd9f676e9b of size 0x4: arg1='xxxx' pc=0x7fb95c6d6fb6
4 [State 0] BaseInstructions: Testing whether data at 0x7ffd9f676518 and size 8 is symbolic:  false
4 [State 0] BaseInstructions: Testing whether data at 0x7ffd9f676520 and size 8 is symbolic:  false
4 [State 0] FunctionModels: Handling strcpy(0x7ffd9f676550, 0x7ffd9f676e9b)
4 [State 0] FunctionModels: Searching for NULL at 0x7ffd9f676e9b
4 [State 0] FunctionModels: Max length 4
4 [State 0] BaseInstructions: Testing whether data at 0x7ffd9f676520 and size 8 is symbolic:  false
4 [State 0] BaseInstructions: Testing whether data at 0x7ffd9f676518 and size 8 is symbolic:  false
4 [State 0] FunctionModels: Handling strcmp(0x7ffd9f676550, 0x7ffd9f676560)
4 [State 0] FunctionModels: Searching for NULL at 0x7ffd9f676550
4 [State 0] FunctionModels: Max length 4
4 [State 0] FunctionModels: Searching for NULL at 0x7ffd9f676560
4 [State 0] FunctionModels: Max length 5
4 [State 0] FunctionModels: Comparing 5 chars
qemu-system-x86_64: /home/ying/s2e/source/s2e/libs2eplugins/src/s2e/Plugins/Models/BaseFunctionModels.cpp:207: bool s2e::plugins::models::BaseFunctionModels::strcmpHelperCommon(s2e::S2EExecutionState *, const uint64_t *, uint64_t, ref<klee::Expr> &): Assertion `width == Expr::Int32 && "-1 representation becomes wrong"' failed.
./launch-s2e.sh: line 74: 22998 Aborted                 (core dumped) LD_PRELOAD=$LIBS2E $QEMU $DRIVE -k en-us $GRAPHICS -monitor null -m 256M -enable-kvm -serial file:serial.txt -net none -net nic,model=e1000 -loadvm ready $*

I want to know is there something wrong with my commands or my test file ? Or , s2e can not handle strcmp in FunctionModels ? ( I've meet the same crash when I tried to explore libxml2(a library) with s2e , so I write the above test file to test strcmp with s2e.)

Thanks a lot!

[vitalych]

Looks like the plugin doesn't support 64-bit yet.

[JodieAllen]

ok, thank you!

[JodieAllen]

I've tried to build the test file with -m32 and run it on debian-9.2.1-i386. However, if I write add_plugin("FunctionModels") into s2e-config.lua, the screen shows a loop message as following :

[state 0] BaseInstruction: Testing whether data at 0x8048620 and size 1 is symbol: false
[state 0] BaseInstruction: Testing whether data at 0x8048620 and size 1 is symbol: false
[state 0] BaseInstruction: Testing whether data at 0x8048620 and size 1 is symbol: false
[state 0] BaseInstruction: Testing whether data at 0x8048620 and size 1 is symbol: false
[state 1] BaseInstruction: Testing whether data at 0x8048624 and size 1 is symbol: false
[state 1] BaseInstruction: Testing whether data at 0x8048624 and size 1 is symbol: false
[state 1] BaseInstruction: Testing whether data at 0x8048624 and size 1 is symbol: false
[state 1] BaseInstruction: Testing whether data at 0x8048624 and size 1 is symbol: false
[state 0] BaseInstruction: Testing whether data at 0x8048620 and size 1 is symbol: false
[state 0] BaseInstruction: Testing whether data at 0x8048620 and size 1 is symbol: false
[state 0] BaseInstruction: Testing whether data at 0x8048620 and size 1 is symbol: false
[state 0] BaseInstruction: Testing whether data at 0x8048620 and size 1 is symbol: false

And, If I remove the FunctionModels, s2e can give the right concrete of arg[1]. I want to know why s2e gives me the loop message and never stop when FunctionModels is in.

Thank you very much!