diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 17:45:44 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-25 17:45:44 +0200 |
commit | beb1cf4f6b56ee739e3a763de93663a875224402 (patch) | |
tree | e5ba1c623394df93e070becc088749306c8dffb4 /mppa_k1c/ValueAOp.v | |
parent | ff1e531a3f2a58b6fbdc4a5a29f2520d5367c01c (diff) | |
download | compcert-kvx-beb1cf4f6b56ee739e3a763de93663a875224402.tar.gz compcert-kvx-beb1cf4f6b56ee739e3a763de93663a875224402.zip |
added code for extfzl/extfsl (not very useful since bitfields are limited to 32 bits)
Diffstat (limited to 'mppa_k1c/ValueAOp.v')
-rw-r--r-- | mppa_k1c/ValueAOp.v | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 23514d21..e9269213 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -101,6 +101,32 @@ Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) := end else Vtop. +Definition eval_static_extfsl (stop : Z) (start : Z) (v : aval) := + if (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int64.zwordsize) + then + let stop' := Z.add stop Z.one in + match v with + | L w => + L (Int64.shr' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + | _ => Vtop + end + else Vtop. + +Definition eval_static_extfzl (stop : Z) (start : Z) (v : aval) := + if (Z.leb start stop) + && (Z.geb start Z.zero) + && (Z.ltb stop Int64.zwordsize) + then + let stop' := Z.add stop Z.one in + match v with + | L w => + L (Int64.shru' (Int64.shl' w (Int.repr (Z.sub Int64.zwordsize stop'))) (Int.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + | _ => Vtop + end + else Vtop. + Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 @@ -231,6 +257,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | (Oselectfs cond), v0::v1::vselect::nil => eval_static_selectfs cond v0 v1 vselect | (Oextfz stop start), v0::nil => eval_static_extfz stop start v0 | (Oextfs stop start), v0::nil => eval_static_extfs stop start v0 + | (Oextfzl stop start), v0::nil => eval_static_extfzl stop start v0 + | (Oextfsl stop start), v0::nil => eval_static_extfsl stop start v0 | _, _ => Vbot end. @@ -368,6 +396,18 @@ Proof. destruct (_ && _ && _). + inv H1; constructor. + constructor. + + (* extfzl *) + - unfold Val.extfzl, eval_static_extfzl. + destruct (_ && _ && _). + + inv H1; constructor. + + constructor. + + (* extfsl *) + - unfold Val.extfsl, eval_static_extfsl. + destruct (_ && _ && _). + + inv H1; constructor. + + constructor. Qed. End SOUNDNESS. |