Thomas Haas
Thomas Haas
**Problem:** Our relation analysis represents the may/must-sets of all relations explicitly, which results in huge (possibly prohibitive) memory consumption on larger benchmarks. Since relations can be quadratic in the unrolled...
We need to improve our support for CAT features to handle the new ARM/ASL model. Having those features is generally useful even outside of ARM/ASL. I want to list the...
Our `GEPToAddition` pass produces wrong offsets that do not respect alignment. The underlying issue is that `size(struct {a, b}) != size(a) + size(b)` due to alignment requirements. This results in...
We have decided to not enforce SSA-form in our IR, however, this can cause worse encodings. Whenever encoding a read access of register `r`, we need to iterate over all...
**Context:** Our program processing frequently produces exceptions due to, e.g., unsupported intrinsics, unsupported control-flow (unnatural loops), or failure of analysis. **Problem:** Sometimes, such errors occur only in dead code, i.e.,...
SImilar to #534, we should have better ways to visualize (and hence understand) our own internal analyses results. By internal analysis results, I mean things like aliasing relationships, call/control-flow graphs,...
Some PR (probably the LLVM rework?) removed the ability to parse a program as integers and instead moved all integer reasoning to the encoder (when `encoding.integers=true`). This does not work...
We should have a (toggable) feature in the Refinement procedure that allows us to collect (dynamic) information about all observed executions and check that against our statically derived information. This...
This issue is a summary of what we discussed in #528 **Context:** PTX requires a partial notion of coherence rather than a total one. We adapted our anarchic semantics to...
Some hardware supports branchless instructions like e.g. CMOV on x86 and CSEL on ARM64. PowerPC and RISC-V seem to have less of those. Such branchless instructions, as their name suggests,...