From ff1e531a3f2a58b6fbdc4a5a29f2520d5367c01c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 25 Apr 2019 16:24:10 +0200 Subject: start of extfzl/extfsl --- common/Values.v | 27 +++++++++++++++++++++++++++ mppa_k1c/Asm.v | 5 +++++ mppa_k1c/Asmblockdeps.v | 2 ++ mppa_k1c/Asmvliw.v | 4 ++++ mppa_k1c/PostpassSchedulingOracle.ml | 8 ++++---- mppa_k1c/TargetPrinter.ml | 4 ++-- test/monniaux/bitfields/bitfields.c | 6 ++++++ 7 files changed, 50 insertions(+), 6 deletions(-) diff --git a/common/Values.v b/common/Values.v index 059a72d9..45774913 100644 --- a/common/Values.v +++ b/common/Values.v @@ -794,6 +794,33 @@ Definition extfs stop start v := end else Vundef. +Definition extfzl stop start v := + 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 + | Vlong w => + Vlong (Int64.shru (Int64.shl w (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + | _ => Vundef + end + else Vundef. + + +Definition extfsl stop start v := + 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 + | Vlong w => + Vlong (Int64.shr (Int64.shl w (Int64.repr (Z.sub Int64.zwordsize stop'))) (Int64.repr (Z.sub Int64.zwordsize (Z.sub stop' start)))) + | _ => Vundef + end + else Vundef. + (** Comparisons *) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 1e1f6e36..ec67d703 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -133,6 +133,9 @@ Inductive instruction : Type := | Pextfz (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *) | Pextfs (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields signed *) + | Pextfzl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *) + | Pextfsl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields signed *) + | Pfabsd (rd rs: ireg) (**r float absolute double *) | Pfabsw (rd rs: ireg) (**r float absolute word *) | Pfnegd (rd rs: ireg) (**r float negate double *) @@ -286,6 +289,8 @@ Definition basic_to_instruction (b: basic) := | PArithRR Asmvliw.Pzxwd rd rs => Pzxwd rd rs | PArithRR (Asmvliw.Pextfz stop start) rd rs => Pextfz rd rs stop start | PArithRR (Asmvliw.Pextfs stop start) rd rs => Pextfs rd rs stop start + | PArithRR (Asmvliw.Pextfzl stop start) rd rs => Pextfzl rd rs stop start + | PArithRR (Asmvliw.Pextfsl stop start) rd rs => Pextfsl rd rs stop start | PArithRR Asmvliw.Pfabsd rd rs => Pfabsd rd rs | PArithRR Asmvliw.Pfabsw rd rs => Pfabsw rd rs | PArithRR Asmvliw.Pfnegd rd rs => Pfnegd rd rs diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index b3a72517..a1a11701 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1215,6 +1215,8 @@ Definition string_of_name_rr (n: arith_name_rr): pstring := | Pzxwd => "Pzxwd" | Pextfz _ _ => "Pextfz" | Pextfs _ _ => "Pextfs" + | Pextfzl _ _ => "Pextfzl" + | Pextfsl _ _ => "Pextfsl" | Pfabsd => "Pfabsd" | Pfabsw => "Pfabsw" | Pfnegd => "Pfnegd" diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 13ff5422..3c308960 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -309,6 +309,8 @@ Inductive arith_name_rr : Type := (* | Pextfs (stop : int) (start : int) (**r extract bit field, signed *) *) | Pextfz (stop : Z) (start : Z) (**r extract bit field, unsigned *) | Pextfs (stop : Z) (start : Z) (**r extract bit field, signed *) + | Pextfzl (stop : Z) (start : Z) (**r extract bit field, unsigned *) + | Pextfsl (stop : Z) (start : Z) (**r extract bit field, signed *) | Pfabsd (**r float absolute double *) | Pfabsw (**r float absolute word *) @@ -883,6 +885,8 @@ Definition arith_eval_rr n v := | Pzxwd => Val.longofintu v | Pextfz stop start => Val.extfz stop start v | Pextfs stop start => Val.extfs stop start v + | Pextfzl stop start => Val.extfzl stop start v + | Pextfsl stop start => Val.extfsl stop start v | Pfnegd => Val.negf v | Pfnegw => Val.negfs v | Pfabsd => Val.absf v diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 87f34ee6..b9344116 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -36,6 +36,8 @@ let arith_rr_str = function | Pzxwd -> "Pzxwd" | Pextfz(_,_) -> "Pextfz" | Pextfs(_,_) -> "Pextfs" + | Pextfzl(_,_) -> "Pextfzl" + | Pextfsl(_,_) -> "Pextfsl" | Pfabsw -> "Pfabsw" | Pfabsd -> "Pfabsd" | Pfnegw -> "Pfnegw" @@ -476,10 +478,8 @@ let ab_inst_to_real = function | "Pmaddl" -> Maddd | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make | "Pnop" | "Pcvtw2l" -> Nop - | "Psxwd" -> Extfs - | "Pzxwd" -> Extfz - | "Pextfz" -> Extfz - | "Pextfs" -> Extfs + | "Pextfz" | "Pextfzl" | "Pzxwd" -> Extfz + | "Pextfs" | "Pextfsl" | "Psxwd" -> Extfs | "Pfnarrowdw" -> Fnarrowdw | "Pfwidenlwd" -> Fwidenlwd | "Pfloatwrnsz" -> Floatwz diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 8826e6a2..f986db39 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -377,9 +377,9 @@ module Target (*: TARGET*) = fprintf oc " sxwd %a = %a\n" ireg rd ireg rs | Pzxwd(rd, rs) -> fprintf oc " zxwd %a = %a\n" ireg rd ireg rs - | Pextfz(rd, rs, stop, start) -> + | Pextfz(rd, rs, stop, start) | Pextfzl(rd, rs, stop, start) -> fprintf oc " extfz %a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start) - | Pextfs(rd, rs, stop, start) -> + | Pextfs(rd, rs, stop, start) | Pextfsl(rd, rs, stop, start) -> fprintf oc " extfs %a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start) | Pfabsd(rd, rs) -> fprintf oc " fabsd %a = %a\n" ireg rd ireg rs diff --git a/test/monniaux/bitfields/bitfields.c b/test/monniaux/bitfields/bitfields.c index 868d7483..f9e84399 100644 --- a/test/monniaux/bitfields/bitfields.c +++ b/test/monniaux/bitfields/bitfields.c @@ -14,7 +14,13 @@ int get_f2(struct fields x) { return x.f2; } +void set_f1(struct fields *x, unsigned v) { + x->f1 = v; +} + int main() { struct fields x = {1, 2, -1}; printf("%d %d\n", get_f1(x), get_f2(x)); + set_f1(&x, 4); + printf("%d %d\n", get_f1(x), get_f2(x)); } -- cgit