Spirv OpUndef #769
Spirv OpUndef #769
Conversation
| public Expression visitOpUndef(SpirvParser.OpUndefContext ctx) { | ||
| String id = ctx.idResult().getText(); | ||
| Type type = builder.getType(ctx.idResultType().getText()); | ||
| Expression expression = builder.makeUndefinedValue(type); |
There was a problem hiding this comment.
From the builder, this is calling program.newConstant(), which creates a single global variable that is shared when the code gets duplicated by say inlining or thread creation. I don't think this is the intention. Indeed, we solved a similar problem in #763
There was a problem hiding this comment.
Yes, for non-det values in initial memory, you can use program.newConstant(), otherwise you should use EventFactory.Svcomp.newNonDetChoice (*) as event since this will ensure a fresh value per instance.
Depending on the idea of UndefValue, it would actually be fine to use the same value for all instance (in LLVM, undef values can be freely chosen by the compiler, and he can choose the same value for all instances!).
(*) We need to move that event into the core language like many other "Svcomp Events".
natgavrilenko
force-pushed
the
spirv-op-undef
branch
from
1def61b to
aa00de2
Compare
hernanponcedeleon
force-pushed
the
spirv-op-undef
branch
from
aa00de2 to
c06176a
Compare
No description provided.