diff options
author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-15 11:55:15 +0200 |
---|---|---|
committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-15 11:55:15 +0200 |
commit | 6d8dce834bf5c1eebdca8d6b874378cea9fc1199 (patch) | |
tree | aad1307aba2dbe82d833c031e6a3b8bf9c392c9b | |
parent | a297e5ff34ff9729ec56838543ef8d044a49f683 (diff) | |
parent | c6d61b7c46e459e7a2891801e2adac94e164dd19 (diff) | |
download | compcert-kvx-6d8dce834bf5c1eebdca8d6b874378cea9fc1199.tar.gz compcert-kvx-6d8dce834bf5c1eebdca8d6b874378cea9fc1199.zip |
Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx-work
-rw-r--r-- | aarch64/PeepholeOracle.ml | 2 | ||||
-rw-r--r-- | riscV/OpWeights.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml index 2b214df4..1d890f2c 100644 --- a/aarch64/PeepholeOracle.ml +++ b/aarch64/PeepholeOracle.ml @@ -468,6 +468,7 @@ let pair_rep_inv insta = (trans_sti sti, rd1, r, chunk_store sti, c, ADimm (b, n1)))); Hashtbl.replace symb_mem st_t pot_rep (* Any other inst *)) + else reset_str_symb_mem () | i -> ( (* Clear list of candidates if there is a non supported store *) match i with PStore _ -> reset_str_symb_mem () | _ -> ()) @@ -598,6 +599,7 @@ let pair_rep insta = PStore (Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n)))); Hashtbl.replace symb_mem st_t pot_rep) + else reset_str_symb_mem () (* Any other inst *) | i, _ -> ( (* Clear list of candidates if there is a non supported store *) diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml index 32cb4c9f..226f8b20 100644 --- a/riscV/OpWeights.ml +++ b/riscV/OpWeights.ml @@ -102,14 +102,12 @@ module FU74 = struct let non_pipelined_resources_of_op (op : operation) (nargs : int) = match op with - | Odiv | Odivu | Omod | Omodu | Odivl | Odivlu | Omodl | Omodlu | Odivf - | Odivfs -> - [| 68 |] + | Odiv | Odivu | Odivl | Odivlu | Odivf | Odivfs -> [| 68 |] | _ -> [| -1 |] let resources_of_cond (cond : condition) (nargs : int) = match cond with - | Ccompf _ |Cnotcompf _|Ccompfs _|Cnotcompfs _ -> [| 1; 0; 1; 1; 0 |] + | Ccompf _ | Cnotcompf _ | Ccompfs _ | Cnotcompfs _ -> [| 1; 0; 1; 1; 0 |] | _ -> [| 1; 0; 1; 0; 0 |] let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3 |