haybale
haybale copied to clipboard
error-handled `loop_bound`
Here is a simple c code
void foo()
{
int a = strlen("123");;
int b = strlen("123");
}
When I test it with loop_bound
=2, haybale will throw a LoopBoundExceeded
error because strlen
was called multiple times.
Thus varmap.active_version
store ("strlen", "%21", BV)
twice.
Debug info:
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %1, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %47, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: mosquitto__calloc, bb %2, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %47, starting at instr 1}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %53, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %77, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %93, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %114, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %123, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %133, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %156, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %161, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %174, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %178, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %249, starting at terminator}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %250, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %253, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %258, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %269, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %304, starting at terminator}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %305, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %313, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %335, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %342, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %1, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %17, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %20, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %20, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %29, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %38, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %43, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: handle__publish, bb %342, starting at instr 6}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %1, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %17, starting at instr 0}
{/home/szx/Documents/Experiments/llvm-pass/HelloWorld/complete.bc: strlen, bb %20, starting at instr 0}
Unless I'm missing something, this is the explicitly documented behavior of the loop_bound
field. (I agree that in many cases we'd want a more complicated semantics for loop_bound
, but that would be harder to implement -- Haybale would have to know when to reset the counter for an inner loop.) If you want to allow more iterations, the easy fix is simply to raise loop_bound
.
Yeah, It's hard to identify loop precisely. From my observations, Haybale will never reset varmap.version_num
whenever return from a function like strlen
above, hence the new_version_num
of local variable (e.g., ("strlen", "%21", num)) will increase each time enter this function. Which lead to LoopBoundExceeded
when calling a single function multiple times.
I try to clear the version_num
when back to the callee, maybe is useful.
pub fn clear_version_num(&mut self, funcname: String) {
let version = self.version_num.clone();
let keys: Vec<(&String, &Name)> = version.keys().collect();
for (key, value) in keys {
if key.to_string() == funcname {
let mut a = self.version_num.get(key, value).unwrap();
let name = value.to_owned();
self.version_num
.entry(funcname.clone(), name)
.and_modify(|v| *v = 0) // increment if it already exists in map
.or_insert(0); // insert a 0 if it didn't exist in map
a = self.version_num.get(key, value).unwrap();
}
}
}
I'm worried that reusing the version_num
s across different calls of the same function, will force the local variables in that function to have the same values during every call. But, maybe instead we could make a separate loop_bound
counter that's separate from version_num
.
That said, I still think the easiest (and maybe best) solution is just to raise loop_bound
to the total number of loop iterations you want to allow across all calls to strlen
.