[TheaPredicate2]

Addresses the first half of #171: SymCC fails to compile code that performs arithmetic on i1 values.

Why it crashed

Symbolizer::visitBinaryOperator has a special path for operands of type i1: it routes the binary operator through the runtime's Boolean handlers (buildBoolAnd, buildBoolOr, buildBoolXor) rather than the bit-vector handlers. The switch only covered And/Or/Xor, so Add, Sub, or Mul on i1 fell through to llvm_unreachable("Unknown Boolean operator").

Fix

Add Add/Sub/Mul cases to the existing switch:

• add i1 and sub i1 are arithmetic mod 2, which is equivalent to XOR → buildBoolXor.
• mul i1 is equivalent to AND → buildBoolAnd.

That's a 9-line change in compiler/Symbolizer.cpp.

Test

test/bool_arithmetic.ll is a hand-written regression test modeled on uadd_sat.ll: it reads two symbolic bytes from stdin, truncates each to i1, performs add i1 / sub i1 / mul i1, and branches on the result so the solver is exercised.

The test is written as .ll on reviewer feedback — a C version compiled with any optimization gets the i1 arithmetic folded into bitwise ops before the Symbolizer sees it, so the .c + -O2 form didn't actually exercise the new switch cases.

Scope

Vector type support (second half of #171) has been split out into a follow-up PR to keep this one small and reviewable. The vector work is preserved on branch save/vector-support and will be opened once this lands.

[aurelf]

Thanks ! It seems that there are really 2 issues in issue #171 (please refer to the issues numbers in the comments so that the issue gets referenced and a back link is easy to find).

Could you have a look at the test failures and split the PR in 2 ? "Arithmetic on Booleans" looks like something that we could just merge almost as is.
There is one issue, the test should use -O0, or better a .ll file containing add/sub/mul i1 directly, like uadd_sat.ll. This is because if compiled with -02 the code isn't actually using "Arithmetic on Booleans" any more and the test actually does not test what it is supposed to test.

[TheaPredicate2]

Thanks for the review! I've addressed the feedback:

• Split the PR. This branch now contains only the "arithmetic on booleans" fix. The vector type support will come in a follow-up PR.
• Test rewritten as .ll. test/bool_arithmetic.c has been replaced by test/bool_arithmetic.ll (hand-written IR with explicit add/sub/mul i1), modeled on uadd_sat.ll so the arithmetic survives to the Symbolizer regardless of optimization level.
• Issue referenced. Commit message now says Refs: eurecom-s3/symcc#171.
• Test failures. The only failing test is file_input.c, which was already broken on master (FileNotFoundError: ...file_input.c.input) — unrelated to this PR. Happy to open a separate issue/PR for that if useful.

PR title and description updated accordingly. I force-pushed the branch to reshape it into a single commit; the old history (bool + vectors) is preserved locally and will come back under a new PR for the vector support.