Re: [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 
patch along with some FP intrinsics 
supported here: https://github.com/qrort/klee 
. You have mentioned that you'd be happy 
to discuss the possibilities of this to be merged in mainline KLEE in 
this issue . I am 
willing to take the work that needs to be done. Can we discuss it? :)


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] KLEE floating-point support

[Aleksei Pleshakov]

 I currently have the https://github.com/srg-imperial/klee-float
 patch along with some FP intrinsics
supported here: https://github.com/qrort/klee
. You have mentioned that you'd be happy to
discuss the possibilities of this to be merged in mainline KLEE in this
issue . I am willing
to take the work that needs to be done. Can we discuss it? :)
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev