diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 10:19:55 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 10:19:55 +0100 |
| commit | 2ef85f12a76c1d730324001c8cc62b4d8828a109 (patch) | |
| tree | 75c8e82e82d20ab3a94e1fc423152e3cb25e5f5b /mppa_k1c/NeedOp.v | |
| parent | 4d25fa871e9960d6e01dd4b63acdf367fee5431b (diff) | |
| download | compcert-kvx-2ef85f12a76c1d730324001c8cc62b4d8828a109.tar.gz compcert-kvx-2ef85f12a76c1d730324001c8cc62b4d8828a109.zip | |
begin andn orn
Diffstat (limited to 'mppa_k1c/NeedOp.v')
| -rw-r--r-- | mppa_k1c/NeedOp.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v index f7b13cad..12d7a4f7 100644 --- a/mppa_k1c/NeedOp.v +++ b/mppa_k1c/NeedOp.v @@ -57,6 +57,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oxorimm n => op1 (bitwise nv) | Onxor => op2 (bitwise nv) | Onxorimm n => op1 (bitwise nv) + | Onot => op1 (bitwise nv) + | Oandn => op2 (bitwise nv) + | Oandnimm n => op1 (andimm nv n) + | Oorn => op2 (bitwise nv) + | Oornimm n => op1 (orimm nv n) | Oshl | Oshr | Oshru => op2 (default nv) | Oshlimm n => op1 (shlimm nv n) | Oshrimm n => op1 (shrimm nv n) @@ -85,6 +90,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Oxorlimm n => op1 (default nv) | Onxorl => op2 (default nv) | Onxorlimm n => op1 (default nv) + | Onotl => op1 (default nv) + | Oandnl => op2 (default nv) + | Oandnlimm n => op1 (default nv) + | Oornl => op2 (default nv) + | Oornlimm n => op1 (default nv) | Oshll | Oshrl | Oshrlu => op2 (default nv) | Oshllimm n => op1 (default nv) | Oshrlimm n => op1 (default nv) @@ -170,6 +180,11 @@ Proof. - apply xor_sound; auto with na. - apply notint_sound; apply xor_sound; auto. - apply notint_sound; apply xor_sound; auto with na. +- apply notint_sound; auto. +- apply and_sound; try apply notint_sound; auto with na. +- apply andimm_sound; try apply notint_sound; auto with na. +- apply or_sound; try apply notint_sound; auto with na. +- apply orimm_sound; try apply notint_sound; auto with na. - apply shlimm_sound; auto. - apply shrimm_sound; auto. - apply shruimm_sound; auto. |