diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 12:27:15 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-05-30 12:27:15 +0000 |
| commit | f4b41226d60ca57c5981b0a46e0a495152b5301f (patch) | |
| tree | fb3ea7a1cabfc5e4c56ecc1b60eeacd2883a8293 /caml | |
| parent | f77e0ade09d8fd17add98c3bc4317627078f3aa8 (diff) | |
| download | compcert-f4b41226d60ca57c5981b0a46e0a495152b5301f.tar.gz compcert-f4b41226d60ca57c5981b0a46e0a495152b5301f.zip | |
Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore utilisee dans le front-end C.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml')
| -rw-r--r-- | caml/CMlexer.mll | 1 | ||||
| -rw-r--r-- | caml/CMparser.mly | 4 | ||||
| -rw-r--r-- | caml/CMtypecheck.ml | 2 | ||||
| -rw-r--r-- | caml/Floataux.ml | 3 | ||||
| -rw-r--r-- | caml/PrintPPC.ml | 22 |
5 files changed, 31 insertions, 1 deletions
diff --git a/caml/CMlexer.mll b/caml/CMlexer.mll index ba67a699..9854117c 100644 --- a/caml/CMlexer.mll +++ b/caml/CMlexer.mll @@ -77,6 +77,7 @@ rule token = parse | "int8s" { INT8S } | "int8u" { INT8U } | "intoffloat" { INTOFFLOAT } + | "intuoffloat" { INTUOFFLOAT } | "{" { LBRACE } | "{{" { LBRACELBRACE } | "[" { LBRACKET } diff --git a/caml/CMparser.mly b/caml/CMparser.mly index e7c656d6..0b3eafd8 100644 --- a/caml/CMparser.mly +++ b/caml/CMparser.mly @@ -252,6 +252,7 @@ let mkmatch expr cases = %token INT8U %token <int32> INTLIT %token INTOFFLOAT +%token INTUOFFLOAT %token LBRACE %token LBRACELBRACE %token LBRACKET @@ -308,7 +309,7 @@ let mkmatch expr cases = %left LESSLESS GREATERGREATER GREATERGREATERU %left PLUS PLUSF MINUS MINUSF %left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU -%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC +%nonassoc BANG TILDE p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 ALLOC %left LPAREN /* Entry point */ @@ -459,6 +460,7 @@ expr: | MINUSF expr %prec p_uminus { Runop(Onegf, $2) } | ABSF expr { Runop(Oabsf, $2) } | INTOFFLOAT expr { Runop(Ointoffloat, $2) } + | INTUOFFLOAT expr { Runop(Ointuoffloat, $2) } | FLOATOFINT expr { Runop(Ofloatofint, $2) } | FLOATOFINTU expr { Runop(Ofloatofintu, $2) } | TILDE expr { Runop(Onotint, $2) } diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml index 625c36fc..dccaadcf 100644 --- a/caml/CMtypecheck.ml +++ b/caml/CMtypecheck.ml @@ -99,6 +99,7 @@ let type_unary_operation = function | Oabsf -> tfloat, tfloat | Osingleoffloat -> tfloat, tfloat | Ointoffloat -> tfloat, tint + | Ointuoffloat -> tfloat, tint | Ofloatofint -> tint, tfloat | Ofloatofintu -> tint, tfloat @@ -142,6 +143,7 @@ let name_of_unary_operation = function | Oabsf -> "absf" | Osingleoffloat -> "singleoffloat" | Ointoffloat -> "intoffloat" + | Ointuoffloat -> "intuoffloat" | Ofloatofint -> "floatofint" | Ofloatofintu -> "floatofintu" diff --git a/caml/Floataux.ml b/caml/Floataux.ml index 0226de27..6b3b825f 100644 --- a/caml/Floataux.ml +++ b/caml/Floataux.ml @@ -19,6 +19,9 @@ let singleoffloat f = let intoffloat f = coqint_of_camlint (Int32.of_float f) +let intuoffloat f = + coqint_of_camlint (Int64.to_int32 (Int64.of_float f)) + let floatofint i = Int32.to_float (camlint_of_coqint i) diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index 1d2e32ca..030dcc67 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -185,6 +185,28 @@ let print_instruction oc labels = function fprintf oc " fctiwz f13, %a\n" freg r2; fprintf oc " stfd f13, -8(r1)\n"; fprintf oc " lwz %a, -4(r1)\n" ireg r1 + | Pfctiu(r1, r2) -> + let lbl1 = new_label() in + let lbl2 = new_label() in + let lbl3 = new_label() in + fprintf oc " addis r2, 0, ha16(L%d)\n" lbl1; + fprintf oc " lfd f13, lo16(L%d)(r2)\n" lbl1; + fprintf oc " fcmpu cr7, %a, f13\n" freg r2; + fprintf oc " cror 30, 29, 30\n"; + fprintf oc " beq cr7, L%d\n" lbl2; + fprintf oc " fctiwz f13, %a\n" freg r2; + fprintf oc " stfdu f13, -8(r1)\n"; + fprintf oc " lwz %a, 4(r1)\n" ireg r1; + fprintf oc " b L%d\n" lbl3; + fprintf oc "L%d: fsub f13, %a, f13\n" lbl2 freg r2; + fprintf oc " fctiwz f13, f13\n"; + fprintf oc " stfdu f13, -8(r1)\n"; + fprintf oc " lwz %a, 4(r1)\n" ireg r1; + fprintf oc " addis %a, %a, 0x8000\n" ireg r1 ireg r1; + fprintf oc "L%d: addi r1, r1, 8\n" lbl3; + fprintf oc " .const_data\n"; + fprintf oc "L%d: .long 0x41e00000, 0x00000000\n" lbl1; + fprintf oc " .text\n" | Pfdiv(r1, r2, r3) -> fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfmadd(r1, r2, r3, r4) -> |