Compare result of abstract interpretation with run of program

karelklic / canal

Abstract interpreter for real-world application programs

https://github.com/karelklic/canal/wiki

Other

32 stars 3 forks source link

Compare result of abstract interpretation with run of program #47

Open xbrukner opened 11 years ago

xbrukner commented 11 years ago

It would be nice to calculate fixpoint on some unit test of program, then interpret the program and compare fixpoint with the actual data during the interpretation.

xbrukner commented 11 years ago

Three possible approaches:

use LLVM interpreter to interpret program and check variable values against calculated fixpoint
instrument LLVM bytecode (for example via LLVM Pass) to call our library, which would check given value against value of the same variable in calculated fixpoint
implement "real value" domains - domain representing real integer, real float etc. and "calculate fixpoint" - execute the program and when executing, check the value of real value against calculated fixpoint