Constraints on divisor != 0

4 views
Skip to first unread message

Weiqi Wang

unread,
Sep 2, 2021, 11:56:40 AMSep 2
to S2E Developer Forum
Hi,

If a concolic byte is not zero and used as a divisor, s2e emits a constraint that requires the byte to be not zero. Can you suggest me on how to disable this? i.e. not emit constraints when a concolic byte is used as divisor

sample program:

int main(void) {
    unsigned char input[32] = { 0 };

    input[1] = 1;

    s2e_make_symbolic(input, 32, "input");

    double c;
    c = (double) 2/ (double) input[1]; // this line emits constraints input[1] != 0 along with several other complex constraints

    return 0;
}

Best,
Weiqi

Vitaly Chipounov

unread,
Sep 2, 2021, 12:03:06 PMSep 2
to s2e...@googlegroups.com, Weiqi Wang

Hi,

You should see a fork if you divide by an unconstrained symbolic value. One path is the divide by zero path, which triggers a CPU exception. Note that S2E does not fully support floating point operations, instead it emulates them with integer arithmetic. This may add more constraints. Removing them may break execution consistency and cause crashes elsewhere in the system.

What kind of analysis would you like to do? Perhaps there are other ways that would not break execution consistency.

Vitaly

--
--
You received this message because you are a member of the S2E Developer Forum.
To post to this group, send email to s2e...@googlegroups.com
To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/s2e-dev

---
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/607b7a4a-9f03-43d6-be0a-cfe884302d8dn%40googlegroups.com.

Weiqi Wang

unread,
Sep 2, 2021, 12:12:30 PMSep 2
to S2E Developer Forum
Hi Vitaly,

Thanks for your prompt reply. I'd like to execute the program concretely and collect constraints. So when I look at the collected constraints, I could see that the byte used as the divisor is unconstrainted. But currently s2e emits constraints that sets the byte to be != 0 even if it's unconstrainted.

Best,
Weiqi

Vitaly Chipounov

unread,
Sep 2, 2021, 7:06:09 PMSep 2
to s2e...@googlegroups.com, Weiqi Wang

Hi,

The byte automatically becomes constrained after the division operation is executed. If the byte wasn't constrained, it could potentially be 0, which is impossible if execution were to proceed past the division instruction. You would end up with a potentially invalid test case.

Vitaly

Weiqi Wang

unread,
Sep 2, 2021, 8:35:42 PMSep 2
to S2E Developer Forum
Hi Vitaly,

Thanks for your reply. I only use s2e for collecting constraints. Testcase generation is handled by another script I wrote.

Since s2e runs concolicly. I assume there are 2 steps: 
1. the non-zero divisor would help execution proceed past the division 
2. s2e generates constraints divisor != 0. <-- This is the part I don't need
What I'm looking for is not collecting constraints on symbolic divisor as it's a regular execution instead of a check. In other words, I'd like the collected constraints to reflect the fact that the binary doesn't check divisor != 0 before running division, so it may have divide by zero bug. 

You mentioned "The byte automatically becomes constrained after the division operation is executed.". I guess s2e needs to know it's a division operation in order to add constraints. Could you refer me to the code that checks whether it's a division operation? Disabling the fork or addConstraints there might help.

Best,
Weiqi

Vitaly Chipounov

unread,
Sep 3, 2021, 4:41:37 PMSep 3
to s2e...@googlegroups.com, Weiqi Wang

Hi Weiqi,

If the binary doesn't check the divisor, it should fork in the helper_divx_XX functions in QEMU [1]. You will have one path where the program crashes with a division by zero exception and another path where the program terminates normally. You can use S2E to detect the crash and record the corresponding test case / path constraints, and discard the other paths that don't crash. If the binary does check the divisor, there won't be a fork in [1] and the program will not crash.

Vitaly

[1]  https://github.com/S2E/s2e/blob/master/libcpu/src/target-i386/op_helper.c#L1918

Reply all
Reply to author
Forward
0 new messages