An important aspect of our remediation instrumentation is performing sound optimizations. An optimization is considered sound, if it preserves the semantics of the original program and does not introduce behaviors that were not possible before. In order to verify that our optimizations are sound we should write experiments with Alive2 or KLEE.
Our current bounds check logic is:
%under_limit = icmp ule i64 %derived, %limit ; derived <= limit
%above_base = icmp uge i64 %derived, %base ; derived >= base
%within_bounds = and i1 %underlimit, %above_base ; derived <= limit && derived >= base
Here is an equivalent bounds check optimization using arithmetic operations and integer compare.
%difDerivedBase = sub i64 %derived, %base
%difLimitBase = sub i64 %limit, %base
%within_bounds = icmp ule i64 %difDerivedBase, %difLimitBase
Below is the Alive2 proof:
----------------------------------------
define i1 @src(i64 noundef %base, i64 noundef %derived, i64 noundef %limit) {
#0:
; Alive2 support preconditions
%valid = icmp ule i64 noundef %base, noundef %limit
assume i1 %valid
%under_limit = icmp ule i64 noundef %derived, noundef %limit
%above_base = icmp uge i64 noundef %derived, noundef %base
%within_bds = and i1 %above_base, %under_limit
ret i1 %within_bds
}
=>
define i1 @tgt(i64 noundef %base, i64 noundef %derived, i64 noundef %limit) {
#0:
; Alive2 supports preconditions
%valid = icmp ule i64 noundef %base, noundef %limit
assume i1 %valid
%differDerivedBase = sub i64 noundef %derived, noundef %base
%differLimitBase = sub i64 noundef %limit, noundef %base
%bounds = icmp ule i64 %differDerivedBase, %differLimitBase
ret i1 %bounds
}
Transformation seems to be correct!The optimization being applied here reduces the number of integer comparisons from two to one. The trade-off is that we introduce more math for the comparison. Arithmetic operations are pretty performant on most architectures (i.e. x86-64, ARM) and because we do not have any way to record performance of our optimizations we will return to this at a later time (include discussion about generated assembly). For future PRs that contain compiler optimizations, make sure to include a proof of correctness from Alive2 or KLEE with detailed reasoning of why the optimization is correct.
An important aspect of our remediation instrumentation is performing sound optimizations. An optimization is considered sound, if it preserves the semantics of the original program and does not introduce behaviors that were not possible before. In order to verify that our optimizations are sound we should write experiments with Alive2 or KLEE.
Our current bounds check logic is:
Here is an equivalent bounds check optimization using arithmetic operations and integer compare.
Below is the Alive2 proof:
The optimization being applied here reduces the number of integer comparisons from two to one. The trade-off is that we introduce more math for the comparison. Arithmetic operations are pretty performant on most architectures (i.e. x86-64, ARM) and because we do not have any way to record performance of our optimizations we will return to this at a later time (include discussion about generated assembly). For future PRs that contain compiler optimizations, make sure to include a proof of correctness from Alive2 or KLEE with detailed reasoning of why the optimization is correct.