-
Notifications
You must be signed in to change notification settings - Fork 62
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Heapster] Simplify translation of exists x.eq(y)
perms
#1422
Conversation
@m-yac: it looks like some of the CI fails; specifically, it looks like |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Once the CI passes, this all looks good!
@@ -39,11 +39,11 @@ heapster_define_perm env "boolean" " " "llvmptr 1" "exists x:bv 1.eq(llvmword(x) | |||
// memcpy i64 | |||
// heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(X:perm(llvmptr 64), Y:perm(llvmptr 64)).arg0:(exists x:bv 1.X), arg1:(exists x:bv 1.Y), arg2:true, arg3:true -o arg0:(exists x:bv 1.Y), arg1:(exists x:bv 1.Y)" "\\ (X:sort 0) (Y:sort 0) (_:SigBV1 X) (y:SigBV1 Y) -> returnM (SigBV1 Y * (SigBV1 Y * #())) (y, (y, ()))"; | |||
|
|||
// heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(len:bv 64).arg0:byte_array<W,len>, arg1:byte_array<W,len>, arg2:eq(llvmword(len)), arg3:true -o arg0:byte_array<W,len>, arg1:byte_array<W,len>" "\\ (len:Vec 64 Bool) (x y:BVVec 64 len BV8) -> returnM (BVVec 64 len BV8 * (BVVec 64 len BV8 * #())) (y, (y, ()))"; | |||
// heapster_assume_fun env "llvm.memcpy.p0i8.p0i8.i64" "(len:bv 64).arg0:byte_array<W,len>, arg1:byte_array<W,len>, arg2:eq(llvmword(len)), arg3:true -o arg0:byte_array<W,len>, arg1:byte_array<W,len>" "\\ (len:Vec 64 Bool) (x y:BVVec 64 len (Vec 8 Bool)) -> returnM (BVVec 64 len (Vec 8 Bool) * (BVVec 64 len (Vec 8 Bool) * #())) (y, (y, ()))"; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Instead of changing these lines, maybe it would make more sense to change the definition of BV8
to be the new bitvector type without the dependent pair?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, I see, you just got rid of BV8
and friends. That makes sense too; you can ignore my comment if you like.
In this PR, the translation of a permission of the form
exists x.eq(y)
is now just the translation ofx
, instead of a sigma type whose first projection is the translation ofx
and whose second projection isunit
. All the SAW scripts and Coq proof scripts in theheapster-saw/examples
directory have been updated accordingly.NB: This PR adds back
arrays_proofs.v
to the_CoqProject
even though the proof ofno_errors_sum_2d
is still broken - see #1421.