diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 15:01:33 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-29 15:01:33 +0100 |
commit | 5f38e0401747a59a821852fdefb7b588a818bdcf (patch) | |
tree | 345f4a16f2d450b05602c0be71fa13a54ce90d4b /mppa_k1c/Asmblock.v | |
parent | e9a05f4ca3157a88a03f71ab31ef59bd96650142 (diff) | |
parent | 7633cb38e0440160acf3f60f7795a19224850eec (diff) | |
download | compcert-kvx-5f38e0401747a59a821852fdefb7b588a818bdcf.tar.gz compcert-kvx-5f38e0401747a59a821852fdefb7b588a818bdcf.zip |
Merge remote-tracking branch 'origin/mppa_postpass' into mppa-jumptable
Conflicts:
mppa_k1c/Asmblock.v
mppa_k1c/Asmblockdeps.v
Diffstat (limited to 'mppa_k1c/Asmblock.v')
-rw-r--r-- | mppa_k1c/Asmblock.v | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index d630e767..b4cf57ae 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -178,7 +178,8 @@ Inductive ex_instruction : Type := | Pbtbl (r: ireg) (tbl: list label) (**r N-way branch through a jump table *) *) | Pbuiltin: external_function -> list (builtin_arg preg) - -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *). + -> builtin_res preg -> ex_instruction (**r built-in function (pseudo) *) +. (** FIXME: comment not up to date ! @@ -842,10 +843,10 @@ Section RELSEM. set and memory state after execution of the instruction at [rs#PC], or [Stuck] if the processor is stuck. *) -Inductive outcome {rgset}: Type := - | Next (rs:rgset) (m:mem) +Inductive outcome: Type := + | Next (rs:regset) (m:mem) | Stuck. -Arguments outcome: clear implicits. +(* Arguments outcome: clear implicits. *) (** ** Arithmetic Expressions (including comparisons) *) @@ -1307,7 +1308,7 @@ Definition store_chunk n := (** * basic instructions *) -Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset := +Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := match bi with | PArith ai => Next (exec_arith_instr ai rs) m @@ -1349,7 +1350,7 @@ Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset : | Pnop => Next rs m end. -Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome regset := +Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := match body with | nil => Next rs m | bi::body' => @@ -1409,7 +1410,7 @@ Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z := | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb' end. -Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome regset := +Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := match label_pos lbl 0 (fn_blocks f) with | None => Stuck | Some pos => @@ -1424,7 +1425,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome Warning: in m PC is assumed to be already pointing on the next instruction ! *) -Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome regset := +Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome := match res with | Some true => goto_label f l rs m | Some false => Next rs m @@ -1448,7 +1449,7 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti we generate cannot use those registers to hold values that must survive the execution of the pseudo-instruction. *) -Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome regset := +Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome := match oc with | Some ic => (** Get/Set system registers *) @@ -1498,7 +1499,7 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) | None => Next rs m end. -Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome regset := +Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome := match exec_body (body b) rs0 m with | Next rs' m' => let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m' |