search

UQ-PAC / aslp

Partial evaluator for Arm's Architecture Specification Language (ASL)
Other
6 stars 2 forks source link

symbolic opcodes #52

Open mmcloughlin opened 4 months ago

mmcloughlin commented 4 months ago

I am interested in generating semantics for symbolic opcodes, for example where fields corresponding to immediate values or shift amounts are variable. Symbolic register indexes may be interesting as well.

Is this something you've considered already?

I have a work-in-progress PR that demonstrates feasibility. It would need some cleanup but if you agree with the general approach I'd be happy to work on preparing it for review. Please see the PR description for more details on the changes.

https://github.com/mmcloughlin/aslp/pull/1

Thanks!

ncough commented 4 months ago

Hi, thanks for giving this feature a shot! Funnily enough, this is something we have been playing around with for the last few weeks. We began with an approach much like yours, but ran into issues as things became more symbolic. In particular, the current partial evaluator is dependent on bitvector widths and loop bounds being concrete. It's not clear to me whether you'll also run into these issues in your use case, though I suspect shifts may create some problems.

If so, we have sidestepped the problem through an analysis to identify when these concrete values are necessary and a subsequent transform to partially duplicate the program for each concrete possibility. The branch is here https://github.com/UQ-PAC/aslp/tree/taint, with the relevant stages in libASL/symbolic_lifter.ml and libASL/req_analysis.ml. This branch attempts to treat the opcode as entirely symbolic, to effectively extract a lifter, so it also includes changes to support symbolic register indexes.

Either way, we'd be keen for an interface for mixed symbolic/concrete opcodes as you suggest and an implementation based on your approach is definitely feasible.