search

StanfordPL / stoke-release

329 stars 19 forks source link

Question regarding instruction implementation #15

Closed rknath closed 9 years ago

rknath commented 9 years ago

Do you have any implemented instruction that has the following kind of flavors ? PSLLW (xmm, xmm, xmm/m128) ... all 128 bit operand .. 3 arity

PSLLW (xmm, imm8) ... one 128 bit and one 8 bit operand .. 2 arity

I am trying to figure out where is the best place to implement it so that

bchurchill commented 9 years ago

We haven't implemented anything like this yet, although it would be very useful to do so. I think an extension to the packed handler that allows for a third constant operand would work best. This would be akin to the different type signatures that can be used for a handler in simple_handler. With some extensions to packed_handler.cc it should be possible to implement these circuits as a one-liner in packed_handler.h. It should end up looking something like "return b << c;" with appropriate parameters for the width of each shift. Shift is provided by SymBitvector (see the shift_handler) so this shouldn't be hard to do. Does that make sense?

On 02/03/2015 05:19 PM, Rajib Nath wrote:

Do you have any implemented instruction that has the following kind of flavors ? PSLLW (xmm, xmm, xmm/m128) ... all 128 bit operand .. 3 arity

PSLLW (xmm, imm8) ... one 128 bit and one 8 bit operand .. 2 arity

I am trying to figure out where is the best place to implement it so that

  • it is consistent with stokes current implementation style.
  • the code size is minimized as suggested in Stoke

Reply to this email directly or view it on GitHub: https://github.com/eschkufz/stoke-release/issues/15

rknath commented 9 years ago

Thanks a lot. Yes its looks like packed_handler is the right place .. I was thinking about something similar to simple_handler arity case. I don't want to modify too much in the original code.

Is there any interface that gives me the SymBitVector size()? Not sure if there is. Sometimes I felt like needing one ... may be there are some valid reason behind it.

bchurchill commented 9 years ago

There isn't a clean interface for size, although you're right it may be helpful. You can invoke the SymTypecheckVisitor which either returns the size if it's well-typed or 0 if not. The only caveat is that it's expensive to do so, as it requires fully traversing the AST. You can see it in use in z3solver.cc for example.

STOKE is young enough that it still needs changes to the code to broaden its scope of applicability. I can talk to the other stoke developers about giving you access to our more dynamic codebase that we actively work on -- but it's less stable than the release. Let me know if I should do so.

On 02/03/2015 05:52 PM, Rajib Nath wrote:

Thanks a lot. Yes its looks like packed_handler is the right place .. I was thinking about something similar to simple_handler arity case. I don't want to modify too much in the original code.

Is there any interface that gives me the SymBitVector size()? Not sure if there is. Sometimes I felt like needing one ... may be there are some valid reason behind it.

Reply to this email directly or view it on GitHub: https://github.com/eschkufz/stoke-release/issues/15#issuecomment-72775813

rknath commented 9 years ago

That will be really useful for me.

Is there any estimate on when stoke will provide full support for

bchurchill commented 9 years ago

Memory is a planned goal, but we don't have a timeline for it. We're considering trying out the theory of arrays to see if that gives us a good implementation or not. Rahul also has some ideas about how to do this well.

For control flow, excluding loops, in validation, we don't have plans but this shouldn't be hard to do if you wanted. Already the control flags are modeled correctly, so it's just a matter of adding support for conditional jumps I believe.

Loops are somewhat supported in search (not validation) of course. To the extent that they aren't, it's a research problem moreso than implementation.

On 02/03/2015 06:45 PM, Rajib Nath wrote:

That will be really useful for me.

Is there any estimate on when stoke will provide full support for

  • memory ( store related validation )
  • control flow ( in validation )
  • loops

Reply to this email directly or view it on GitHub: https://github.com/eschkufz/stoke-release/issues/15#issuecomment-72780628

bchurchill commented 9 years ago

We're working on giving you access to our other repository, and will be in touch once this is possible.