Commit aa7880dd authored by Bernhard Schommer's avatar Bernhard Schommer
Browse files

Merge branch 'master' into json_export

parents b51cc596 ff625877
...@@ -289,7 +289,7 @@ let string_of_instruction = function ...@@ -289,7 +289,7 @@ let string_of_instruction = function
| Pstwu (i0, c1, i2) -> "Pstwu(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pstwu (i0, c1, i2) -> "Pstwu(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Pstwx (i0, i1, i2) -> "Pstwx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pstwx (i0, i1, i2) -> "Pstwx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Pstwx_a (i0, i1, i2) -> "Pstwx_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pstwx_a (i0, i1, i2) -> "Pstwx_a(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Pstwxu (i0, i1, i2) -> "Pstwxu(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pstwux (i0, i1, i2) -> "Pstwux(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Pstwbrx (i0, i1, i2) -> "Pstwbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pstwbrx (i0, i1, i2) -> "Pstwbrx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Pstwcx_ (i0, i1, i2) -> "Pstwcx_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pstwcx_ (i0, i1, i2) -> "Pstwcx_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
| Psubfc (i0, i1, i2) -> "Psubfc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Psubfc (i0, i1, i2) -> "Psubfc(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")"
......
...@@ -2130,7 +2130,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> ...@@ -2130,7 +2130,7 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
>>= recur_simpl >>= recur_simpl
| _ -> error | _ -> error
end end
| Pstwxu(rd, r1, r2) -> | Pstwux(rd, r1, r2) ->
begin match ecode with begin match ecode with
| STWUX(rS, rA, rB) :: es -> | STWUX(rS, rA, rB) :: es ->
OK(fw) OK(fw)
......
...@@ -260,7 +260,7 @@ Inductive instruction : Type := ...@@ -260,7 +260,7 @@ Inductive instruction : Type :=
| Pstw: ireg -> constant -> ireg -> instruction (**r store 32-bit int *) | Pstw: ireg -> constant -> ireg -> instruction (**r store 32-bit int *)
| Pstwu: ireg -> constant -> ireg -> instruction (**r store 32-bit int with update *) | Pstwu: ireg -> constant -> ireg -> instruction (**r store 32-bit int with update *)
| Pstwx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Pstwx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *)
| Pstwxu: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs and update *) | Pstwux: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs and update *)
| Pstw_a: ireg -> constant -> ireg -> instruction (**r store 32-bit quantity from int reg *) | Pstw_a: ireg -> constant -> ireg -> instruction (**r store 32-bit quantity from int reg *)
| Pstwx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Pstwx_a: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *)
| Pstwbrx: ireg -> ireg -> ireg -> instruction (**r store 32-bit int with reverse endianness *) | Pstwbrx: ireg -> ireg -> ireg -> instruction (**r store 32-bit int with reverse endianness *)
...@@ -878,7 +878,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out ...@@ -878,7 +878,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pstfdu _ _ _ | Pstfdu _ _ _
| Psthbrx _ _ _ | Psthbrx _ _ _
| Pstwu _ _ _ | Pstwu _ _ _
| Pstwxu _ _ _ | Pstwux _ _ _
| Psubfze _ _ | Psubfze _ _
| Psync | Psync
| Ptrap | Ptrap
......
...@@ -457,7 +457,7 @@ let expand_instruction instr = ...@@ -457,7 +457,7 @@ let expand_instruction instr =
emit (Pstwu(GPR1, Cint(coqint_of_camlint adj), GPR1)) emit (Pstwu(GPR1, Cint(coqint_of_camlint adj), GPR1))
else begin else begin
emit_loadimm GPR0 (coqint_of_camlint adj); emit_loadimm GPR0 (coqint_of_camlint adj);
emit (Pstwxu(GPR1, GPR1, GPR0)) emit (Pstwux(GPR1, GPR1, GPR0))
end; end;
emit (Pcfi_adjust (coqint_of_camlint sz)); emit (Pcfi_adjust (coqint_of_camlint sz));
if variadic then begin if variadic then begin
......
...@@ -620,8 +620,8 @@ module Target (System : SYSTEM):TARGET = ...@@ -620,8 +620,8 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " stwu %a, %a(%a)\n" ireg r1 constant c ireg r2 fprintf oc " stwu %a, %a(%a)\n" ireg r1 constant c ireg r2
| Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) -> | Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) ->
fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Pstwxu(r1, r2, r3) -> | Pstwux(r1, r2, r3) ->
fprintf oc " stwxu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 fprintf oc " stwux %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Pstwbrx(r1, r2, r3) -> | Pstwbrx(r1, r2, r3) ->
fprintf oc " stwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 fprintf oc " stwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Pstwcx_(r1, r2, r3) -> | Pstwcx_(r1, r2, r3) ->
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment