Proposal: Domain Restriction Semantics

[ohamel-softwaresecure]

This issue should be considered an RFC, so please do propose alternatives if you have any.

We should have an official policy regarding the behaviour of souffle as to what happens when a computation produces a value that cannot be stored in its declared type. The initial motivating example is 2^31 in the test suite, however the same idea extends to other examples, see below and the issue list. I begin with a description and examples of the issue, and then propose some possible policies.

All examples assume RAM_DOMAIN_SIZE == 32.

Current Behaviour:
Any type of overflow is UB. This will likely result in surprising behavior if this computation is not a literal expression. e.g. arguments in a recursive expression. e.g.

// strawman example
.decl recursive_mul(x: number)
.output recursive_mul
recursive_mul(3).
recursive_mul(2 * x) :- recursive_mul(x).

---------------
recursive_mul
x
===============
-2147483648
-1073741824
0
3
6
12
24
....
805306368
1610612736
===============

This behaviour also extends conversions between numeric types. e.g.

.decl a(x: float)
.decl b(x: number)
.output a, b
b(ftoi(x)) :- a(x).
a(3.5).
a(1000000000000000.0).
a(x * x * x) :- a(x).

---------------
a
x
===============
3.5
42.875
78815.6
4.89595e+14
1e+15
inf
===============
---------------
b
x
===============
-2147483648   // surprising; we don't have negative numbers in `a`!
3                      // do we truncate/round/etc? do we fail a rule if the float is not an integer?
42
78815
===============

Complicating this is the fact that there are users currently (ab)using the fact that 2^31 is INT_MIN. Prior to the addition of Java-style bit-shift operators this was somewhat excusable as a way to avoid having to tattoo that awful constant somwhere on your body to keep it handy.

Possible General Policies:

1. Do nothing. UB is UB. Remember that your souffle program is being projected to C++ and hope that the C++ compiler isn't clever enough to notice any UB and exploit it in exciting ways.
2. Map to nearest point in storage domain: Pretend ops are carried out with infinite precision/range and truncate/round/saturated to storage domain. They might have perf repercussions but this could be mitigated using compiler intrinsics. ( e.g. https://clang.llvm.org/docs/LanguageExtensions.html#checked-arithmetic-builtins )
3. Mix and match above. Arithmetic is UB-ish. Other ops (e.g. ^) aren't.

Deprecating 2^31
This can now be replaced by the well defined expression 2 bshl 31. Any changes to 2^31's behaviour will likely have to wait for Souffle 2's release. Until then, the expression 2^31 could be special-cased for back-compat.

In the future we may also wish to provide pre-proc defs for {UN}SIGNED_{MAX, MIN}.

[yanniss]

I'd personally argue for #1: Do nothing, UB is UB. Using 32-bit ints in a logic program is like using assembly. One should know what to expect and the language is a thin veneer of convenience over the raw machine.

This answer is orthogonal to the possible addition of more disciplined (but clearly designated) numeric types. If a different, more disciplined, type were offered, I'd expect the conversions to work differently. But with "number" being "int", I'd find any "clever" semantics (e.g., saturating) surprising and the current semantics unsurprising.

[ohamel-softwaresecure]

Ram{32,64} Portability:
Another point to consider is whether we care about portability between RAM_DOMAIN 32 and 64. The transition to AMD64 from x86 showed that many programs implicitly depended on int being 32 bits. Without explicitly stating the storage size in the type, I'd assume many souffle programs have the same problem.

UB Sanitizers:
I personally have a grudge against 2^31 appearing in our test suites because it keeps tripping ubsan whenever I run it locally. If we're keeping this behaviour we should probably extend the test suite to suppress the sanitiser for that test case. (negative_numbers.dl)

UB in C++ code-gen:
In interpreter mode signed overflow isn't as deadly because the provoking values don't appear until run-time, reducing the likelihood the compiler can deduce something surprising. When generating C++, it becomes visible to the compiler:
Datalog:

.decl a(x: number)
.output a
a((2 bshl 31) - 1).

Synthesis (simplified snippet, bit-casts omitted when not needed):

SignalHandler::instance()->setMsg(R"_(a(((2bshl31)-1)).
in file /home/olivier/projects/souffle/TOY/ub-tester-2.dl [3:1-3:20])_");
/* BEGIN visitQuery @Synthesiser.cpp:273 */
[&]() {
    CREATE_OP_CONTEXT(rel_1_a_op_ctxt, rel_1_a->createContext());
    Tuple<RamDomain, 1> tuple{{
        // VISIBLE UB!
        ramBitCast<RamSigned>(RamUnsigned(2) << (RamSigned(31) & RAM_BIT_SHIFT_MASK)) - 1
    }};
    rel_1_a->insert(tuple, READ_OP_CONTEXT(rel_1_a_op_ctxt));
}(); /* END visitQuery @Synthesiser.cpp:359 */

At which point the compiler is allowed to get rather creative.

[mmcgr]

Note that the overflow behaviour already varies. On some ARM64 platforms. -2^31 gives -2147483647.

One reason there hasn't been much interest about this before is that it's not usually of concern - either the range used is well within the non-UB range, such as counting from 0/1 up, or arithmetic just isn't used as you're dealing with constants. -2^31 or 2^31 - 1 are of interest as constants, not because we want to calculate those numbers. (There's also an argument that if you care about that -2147483648/2147483647 you should just give the number.)

A version of (3) would be that only RamDomains have UB, RamSpecificTypes do not. If you need clearly defined behaviour, then use a clearly defined type.

[aeflores]

I would argue for 1 or maybe some version of 3 like @mmcgr suggests. For integers and RamDomains having UB is the least surprising behavior.

[ohamel-softwaresecure]

Yet another proposal: compile using -fwrapv -fno-strict-float-cast-overflow.

-fwrapv: Signed arith now uses 2's complement for +, -, *.
-fno-strict-float-cast-overflow (clang only?): float -> integral cast uses platform specific behaviour instead of UB.

[mmcgr]

-fwrapv isn't quite the same as using 2's complement, it just asks the compiler to assume it's used. Behaviour is better defined in some respects, but the computer it's run on can still surprise us with UB. I do think we should do this, especially as we already assume 2's complements, but it doesn't completely solve the problem.

There's also -ftrapv which deals with overflow with traps. This would be preferable in some cases, although it's also slower. Since it's compile-time this may only be an option for use with synthesised souffle.

A comparison of the effect of the flags is shown here: https://godbolt.org/z/_dzEQJ