[klee-dev] KLEE floating-point support

[Cristian Cadar]

Hi Aleksei,

 From what I understand, you managed to rebase the KLEE-Float extension 
on top of KLEE's mainline.  That's great!

As I mentioned on GitHub, my main concern is that KLEE-Float changes the 
expression representation, which has a significant impact on the core of 
KLEE.  The question is whether it is possible to integrate the changes 
in such a way that the core of KLEE is minimally affected.  This would 
require incremental changes and careful measurements.

I am also considering right now experimenting with supporting FP 
programs via fixed-point arithmetic, see the last project at 
https://klee.github.io/projects/.

My proposal would be to first submit your changes to the KLEE-Float 
project at https://github.com/srg-imperial/klee-float.  There is still 
interest in that extension, but it's starting to show its age, as you 
can see in the open issues.  In fact, even the Docker container is 
difficult to run these days, as Arch Linux changed its packaging format 
in the meantime.

Best,
Cristian

On 22/11/2020 21:08, Aleksei Pleshakov wrote:
> I currently have the https://github.com/srg-imperial/klee-float 
> <https://t.co/iq6VMQHLS7?amp=1>patch along with some FP intrinsics 
> supported here: https://github.com/qrort/klee 
> <https://t.co/EbHLzazVQf?amp=1>. You have mentioned that you'd be happy 
> to discuss the possibilities of this to be merged in mainline KLEE in 
> this issue <https://github.com/srg-imperial/klee-float/issues/3>. I am 
> willing to take the work that needs to be done. Can we discuss it? :)
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>