aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-15 11:55:15 +0200
committerDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-15 11:55:15 +0200
commit6d8dce834bf5c1eebdca8d6b874378cea9fc1199 (patch)
treeaad1307aba2dbe82d833c031e6a3b8bf9c392c9b
parenta297e5ff34ff9729ec56838543ef8d044a49f683 (diff)
parentc6d61b7c46e459e7a2891801e2adac94e164dd19 (diff)
downloadcompcert-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.ml2
-rw-r--r--riscV/OpWeights.ml6
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