Added instrumentation of vector TCG operations #38

damienmaier · 2024-02-04T21:49:56Z

This is the code I added for the support of vector TCG instructions in SymQEMU.

I have documented the functions in the source files. There is also some information about the work done in chapter 6 of my bachelor thesis.

damienmaier · 2024-02-04T21:54:48Z

This PR is built on top of my port to QEMU 8 (#37). It also depends on this PR in SymCC that adds support for creating large symbolic constants.

sebastianpoeplau · 2024-02-06T16:51:42Z

I'll wait until we've merged #37 before reviewing this one - the diff should look much nicer after the merge.

aurelf · 2024-02-06T22:26:04Z

@damienmaier could you rebase this branch on the current master?

damienmaier · 2024-02-07T06:23:29Z

Sure !

damienmaier · 2024-02-07T06:35:08Z

Just some infos about how files are organized in this PR :

The original sym helper functions are in accel/tcg/tcg-runtime-sym.c.

I put the vector sym helper functions in a new file accel/tcg/tcg-runtime-sym-vec.c. I also created accel/tcg/tcg-runtime-sym-common.c where I moved some code from tcg-runtime-sym.c that is used both for vector and non-vector sym helper functions.

It seemed better to me to have a separate file for vector helper functions, but if your prefer to have everything in accel/tcg/tcg-runtime-sym.c instead, I can change that.

Other that that I modified tcg/tcg-op-vec.c to inject instrumentation TCG ops. I also added support for helper functions with a larger number of arguments as I needed it.

aurelf

I added a few comments. It would be nice to clarify those points, if they don't need a change, maybe add a comment on what is needed to to activate those features?

tcg/tcg-op-vec.c

aurelf · 2024-02-07T09:24:31Z

tcg/tcg-op-vec.c

@@ -393,9 +550,9 @@ void tcg_gen_not_vec(unsigned vece, TCGv_vec r, TCGv_vec a)
 {
    const TCGOpcode *hold_list = tcg_swap_vecop_list(NULL);

-    if (!TCG_TARGET_HAS_not_vec || !do_op2(vece, r, a, INDEX_op_not_vec)) {
+    /*if (!TCG_TARGET_HAS_not_vec || !do_op2(vece, r, a, INDEX_op_not_vec)) {*/


Same comment as above

tcg/tcg-op-vec.c

aurelf · 2024-02-07T09:34:19Z

Also it would be nice to merge a PR with your testsuite, before we merge this PR (and you could add the tests that are specific to the vec operations to this PR?)

damienmaier · 2024-02-08T06:33:14Z

Regarding the commented code, the only motivation was to save implementation time. By making those instructions being systematically replaced by equivalent, already instrumented instructions, I avoided the work of instrumenting them.

For my defense, this trick was already used for several instructions in the original SymQEMU :) Here is an example https://github.com/eurecom-s3/symqemu/blob/master/tcg/tcg-op.c#L1059

I left the original code (but commented) to be consistent, because this is how it was done for other non vec instructions, like in example above.

damienmaier · 2024-02-08T06:35:06Z

All right, I will make a PR with the tests. I am working on creating a Dockerfile to compile SymQEMU and run the tests

aurelf · 2024-02-08T08:36:47Z

Regarding the commented code, the only motivation was to save implementation time. By making those instructions being systematically replaced by equivalent, already instrumented instructions, I avoided the work of instrumenting them.

Ah, OK. There will be a performance impact I imagine ? The target code could be more efficient if it would be implemented with one instruction ?

For my defense, this trick was already used for several instructions in the original SymQEMU :) Here is an example https://github.com/eurecom-s3/symqemu/blob/master/tcg/tcg-op.c#L1059

Fair :)

I left the original code (but commented) to be consistent, because this is how it was done for other non vec instructions, like in example above.

OK, if my understanding above is correct: could you add a comment, at least on the first such occurrence. I.e., to explain the instruction instrumentation isn't implemented, the alternative works, implementing the instrumentation may give some performance gains (as some likely more effective instructions will be generated)?

sebastianpoeplau

Looks really good, thank you! I've only added two minor comments related to the discussion that we had in your thesis presentation.

One more minor thing: The README currently says in the "Documentation" section that a large part of the implementation is in tcg-runtime-sym.{c,h} - would you mind adding the vector equivalents there? And do you know whether the test mentioned in the same section still works now that some functions have moved and/or changed signatures?

sebastianpoeplau · 2024-02-08T09:03:51Z

accel/tcg/tcg-runtime-sym-vec.c

+ * For each element, the concrete result is used to determine if the comparison was true or false,
+ * and path constraints are pushed accordingly.


Would you mind also mentioning the alternative of computing a symbolic result vector? It's just an intuition, but I think this will make it easier for the solver to come up with good solutions because path constraints have the problem that changing them often requires multiple iterations.

sebastianpoeplau · 2024-02-08T09:04:49Z

accel/tcg/tcg-runtime-sym-vec.c

+ * For each element, the concrete result is used to determine if the ternary condition was true or false,
+ * and path constraints are pushed accordingly.


Same here, let's add the exploration of a symbolic result instead of path constraints as a TODO comment.

damienmaier · 2024-02-11T11:08:33Z

Ah, OK. There will be a performance impact I imagine ? The target code could be more efficient if it would be implemented with one instruction ?

Yes I think that this has a performance impact.

OK, if my understanding above is correct: could you add a comment, at least on the first such occurrence. I.e., to explain the instruction instrumentation isn't implemented, the alternative works, implementing the instrumentation may give some performance gains (as some likely more effective instructions will be generated)?

I added TODO comments to clarify the the situation

aurelf · 2024-02-11T11:29:21Z

Thanks for the updates !

damienmaier · 2024-02-11T13:05:08Z

@sebastianpoeplau I added the todos regarding returning expressions instead of pushing path constrains, and I edited the README.

And do you know whether the test mentioned in the same section still works now that some functions have moved and/or changed signatures

I realize now that the way QEMU tests are run has changed between QEMU 4 and QEMU 8, because QEMU now uses meson. I didn't think about those SymQEMU unit tests when I did the port to QEMU 8, so currently the file tests/check-sym-runtime.c is there but I don't know how to run it.

… tests fail

…instrumented instructions

…instructions

This target program resulted on incorrect results before vector instructions were instrumented

aurelf · 2024-02-17T20:40:43Z

Hi, I rebased this on top of the current main. made a few minor changes, the tests pass.
I think it's good to merge.
It would be nice @damienmaier & @sebastianpoeplau if you could have a look and confirm if it is OK for you?

damienmaier · 2024-02-19T06:11:38Z

It is ok for me !

sebastianpoeplau · 2024-02-22T13:09:25Z

Good for me too!

Minor typos

…com-s3#43)

* Moved check-sym-runtime.c to unit tests and updated to work with QEMU8 * Build and run check-sym-runtime test with meson.build * Improve Dockerfile * Added documentation about test suites

"helper_sym_store_host_i64" and "helper_sym_store_host_i32" were replaced by helper_sym_store_host, adjusting the unit tests accordingly

aurelf · 2024-02-22T15:28:17Z

I had to update also the unit tests, which I just re-enabled.
I'll merge now, after the test passes.
Thanks to both of you!

damienmaier mentioned this pull request Feb 4, 2024

Add a backend function for creating symbolic values representing large integers eurecom-s3/symcc#155

Merged

damienmaier force-pushed the pr-vec-instrumentation branch from 22c49dc to 88e18a3 Compare February 7, 2024 06:11

aurelf reviewed Feb 7, 2024

View reviewed changes

sebastianpoeplau reviewed Feb 8, 2024

View reviewed changes

aurelf mentioned this pull request Feb 11, 2024

SymQEMU tests and Dockefile #39

Closed

damienmaier force-pushed the pr-vec-instrumentation branch from 3b961e7 to 01229b9 Compare February 16, 2024 17:56

damienmaier marked this pull request as draft February 16, 2024 18:07

damienmaier marked this pull request as ready for review February 16, 2024 18:19

damienmaier and others added 10 commits February 17, 2024 20:41

make SymQEMU Dockerfile rely on SymCC Dockerfile

1a9d04e

Add some documentation, fix typos in doc, and wrap to 80 columns

18fc98c

remove unncessary line in Dockerfile

c434dfd

write a wrong test expected output to demonstrate that this makes the…

a9cbdff

… tests fail

revert previous commit

40ffbc2

add util function for vec expr

6f6df2f

instrument tcg_gen_mov_vec

0e5af2e

instumented tcg_gen_ld_vec

3989992

add tcgv_vec_expr util function

af8fa7b

simplify sym_store_host helper

0165c3f

damienmaier and others added 18 commits February 17, 2024 20:44

fix extract symbol logic

89cc562

fix endianess issue in apply_op_and_merge function

82a6792

instrumented saturating signed/unsigned sub/add vec instructions

d3b0386

make sure cmpsel and bitsel instructions are generated using already …

ff7406b

…instrumented instructions

remove forgotten concretization

065eee4

instrumented tcg_gen_dup_i64_vec,tcg_gen_dup_i32_vec functions

f7d0447

instrumented min max functions

6f5b312

instrumented tcg_gen_dup_mem_vec

c5419d0

fix wront assert in sym_load_and_duplicate_into_vec

01b0b10

refactor : put vec helpers in separate file

37491b2

documentation and refactoring

877692f

refactor

d9796f9

fix rotate functions for PR

b29f504

added todo comments to clarify situation for indirectly instrumented …

0529b3b

…instructions

add todo for returning expressions instad of pushing path constraints

1ea43b5

mention files related to vec instructions in README

569f996

Add asprintf test program

3c35a2e

This target program resulted on incorrect results before vector instructions were instrumented

typo fixes in README.md

854d82d

aurelf force-pushed the pr-vec-instrumentation branch from 5808af3 to 854d82d Compare February 17, 2024 19:58

Minor formatting fixes

51bbf36

aurelf added 5 commits February 22, 2024 15:59

Update tcg-runtime-sym-vec.c

5945bd7

Minor typos

Adding QEMU own checks to Dockerfile (CI) and improve README.md (eure…

772c202

…com-s3#43)

Adding SymQEMU unit test suite to CI (eurecom-s3#44)

393104f

* Moved check-sym-runtime.c to unit tests and updated to work with QEMU8 * Build and run check-sym-runtime test with meson.build * Improve Dockerfile * Added documentation about test suites

Update SymQEMU unit tests (check-sym-runtime.c)

087b98d

"helper_sym_store_host_i64" and "helper_sym_store_host_i32" were replaced by helper_sym_store_host, adjusting the unit tests accordingly

Merge branch 'master' into pr-vec-instrumentation

c9a79af

aurelf merged commit 5c00e64 into eurecom-s3:master Feb 22, 2024
1 check passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Added instrumentation of vector TCG operations #38

Added instrumentation of vector TCG operations #38

damienmaier commented Feb 4, 2024

damienmaier commented Feb 4, 2024

sebastianpoeplau commented Feb 6, 2024

aurelf commented Feb 6, 2024

damienmaier commented Feb 7, 2024

damienmaier commented Feb 7, 2024

aurelf left a comment

aurelf Feb 7, 2024

aurelf commented Feb 7, 2024

damienmaier commented Feb 8, 2024

damienmaier commented Feb 8, 2024

aurelf commented Feb 8, 2024

sebastianpoeplau left a comment

sebastianpoeplau Feb 8, 2024

sebastianpoeplau Feb 8, 2024

damienmaier commented Feb 11, 2024

aurelf commented Feb 11, 2024

damienmaier commented Feb 11, 2024

aurelf commented Feb 17, 2024

damienmaier commented Feb 19, 2024

sebastianpoeplau commented Feb 22, 2024

aurelf commented Feb 22, 2024

		* For each element, the concrete result is used to determine if the comparison was true or false,
		* and path constraints are pushed accordingly.

Added instrumentation of vector TCG operations #38

Added instrumentation of vector TCG operations #38

Conversation

damienmaier commented Feb 4, 2024

damienmaier commented Feb 4, 2024

sebastianpoeplau commented Feb 6, 2024

aurelf commented Feb 6, 2024

damienmaier commented Feb 7, 2024

damienmaier commented Feb 7, 2024

aurelf left a comment

Choose a reason for hiding this comment

aurelf Feb 7, 2024

Choose a reason for hiding this comment

aurelf commented Feb 7, 2024

damienmaier commented Feb 8, 2024

damienmaier commented Feb 8, 2024

aurelf commented Feb 8, 2024

sebastianpoeplau left a comment

Choose a reason for hiding this comment

sebastianpoeplau Feb 8, 2024

Choose a reason for hiding this comment

sebastianpoeplau Feb 8, 2024

Choose a reason for hiding this comment

damienmaier commented Feb 11, 2024

aurelf commented Feb 11, 2024

damienmaier commented Feb 11, 2024

aurelf commented Feb 17, 2024

damienmaier commented Feb 19, 2024

sebastianpoeplau commented Feb 22, 2024

aurelf commented Feb 22, 2024