search

UQ-PAC / BASIL

Apache License 2.0
8 stars 0 forks source link

Remove replace stack maintenence stores/loads with free functionspec #143

Open ailrst opened 10 months ago

ailrst commented 10 months ago

The memory_store64_le() operations for maintaining the stack seem to increase verification time exponentially without being relevant to the verification

For example;

  lmain:

    #4, Gamma_#4 := bvadd64(R31, 18446744073709551568bv64), Gamma_R31;
    stack, Gamma_stack := memory_store64_le(stack, #4, R29), gamma_store64(Gamma_stack, #4, Gamma_R29);

    stack, Gamma_stack := memory_store64_le(stack, bvadd64(#4, 8bv64), R30), gamma_store64(Gamma_stack, bvadd64(#4, 8bv64), Gamma_R30);

    R31, Gamma_R31 := #4, Gamma_#4;
    R29, Gamma_R29 := R31, Gamma_R31;
    stack, Gamma_stack := memory_store64_le(stack, bvadd64(R31, 16bv64), R19), gamma_store64(Gamma_stack, bvadd64(R31, 16bv64), Gamma_R19);

These could be removed and replaced with a free requires/ensures.

l-kent commented 10 months ago

This is something that the memory region analysis should theoretically help with once it's working and it doesn't make too much sense to focus on issues like this until that's ready.

I'm not really sure how you would replace them with a free requires/ensures? Would you pass in R31 and R29 as parameters? The stack as a parameter?

More broadly, any solution to this will have to relate to how we identify the relationship between stacks in different procedures.