From 5c73e9884f68e86b673879664ecbb5677c0edb1d Mon Sep 17 00:00:00 2001 From: Hanno Becker Date: Fri, 15 Mar 2024 06:53:48 +0000 Subject: [PATCH] Fix performance issue during model generation --- slothy/core/core.py | 70 ++++++++++++++++--------- slothy/targets/arm_v81m/cortex_m85r1.py | 24 +++++---- 2 files changed, 57 insertions(+), 37 deletions(-) diff --git a/slothy/core/core.py b/slothy/core/core.py index 8064571c..caa7c4c3 100644 --- a/slothy/core/core.py +++ b/slothy/core/core.py @@ -2326,7 +2326,7 @@ def _add_constraints_locked_ordering(self): def inst_changes_addr(inst): return inst.increment is not None - def _forbid_reordering(t0,t1): + def should_forbid_reordering(t0,t1): if not t0.inst.is_load_store_instruction(): return False if not t1.inst.is_load_store_instruction(): @@ -2341,27 +2341,36 @@ def _forbid_reordering(t0,t1): return True return False - for t0, t1 in self.get_inst_pairs(): - if not t0.orig_pos < t1.orig_pos: - continue - if not self.config.constraints.allow_reordering or \ - t0.is_locked or \ - t1.is_locked or \ - _forbid_reordering(t0,t1): - - if self.config.sw_pipelining.enabled: - self._AddImplication( t0.post_var, t1.post_var ) - self._AddImplication( t1.pre_var, t0.pre_var ) - self._AddImplication( t0.pre_var, t1.post_var.Not() ) - - if _forbid_reordering(t0,t1): - self.logger.debug("Forbid reordering of (%s,%s) to avoid address fixup issues", - t0, t1) - - self._add_path_constraint( t1, t0, - lambda t0=t0, t1=t1: self._Add(t0.program_start_var < t1.program_start_var) ) - - # Look for source annotations forcing orderings + def force_stays_before(t0, t1): + if self.config.sw_pipelining.enabled: + self._AddImplication( t0.post_var, t1.post_var ) + self._AddImplication( t1.pre_var, t0.pre_var ) + self._AddImplication( t0.pre_var, t1.post_var.Not() ) + if should_forbid_reordering(t0,t1): + self.logger.debug("Forbid reordering of (%s,%s) to avoid address fixup issues", + t0, t1) + self._add_path_constraint( t1, t0, + lambda t0=t0, t1=t1: self._Add(t0.program_start_var < t1.program_start_var) ) + + def comes_before(t0, t1): + return (t0.orig_pos < t1.orig_pos) + + if self.config.constraints.allow_reordering is False: + for t0, t1 in self.get_inst_pairs(cond=comes_before): + force_stays_before(t0, t1) + else: + for t0, t1 in self.get_inst_pairs( + cond_fst=lambda t: t.is_locked, + cond_snd=lambda t: t.is_locked, + cond = comes_before): + force_stays_before(t0, t1) + + for t0, t1 in self.get_inst_pairs( + cond_fst = lambda t: t.inst.is_load_store_instruction(), + cond_snd = lambda t: t.inst.is_load_store_instruction(), + cond = comes_before): + if should_force_stays_before(t0, t1): + force_stays_before(t0, t1) if self.config.sw_pipelining.enabled is True: nodes = self._get_nodes(low=True) @@ -2502,7 +2511,7 @@ def _add_constraints_register_usage(self): def _add_constraints_misc(self): self.target.add_further_constraints(self) - def get_inst_pairs(self, cond=None): + def get_inst_pairs(self, cond_fst=None, cond_snd=None, cond=None): """Yields all instruction pairs satisfying the provided predicate. This can be useful for the specification of additional @@ -2513,9 +2522,18 @@ def get_inst_pairs(self, cond=None): Returns: Generator of all instruction pairs satisfying the predicate.""" - for t0 in self._model.tree.nodes: - for t1 in self._model.tree.nodes: - if cond is None or cond(t0,t1): + if cond_fst is None: + cond_fst = lambda x: True + if cond_snd is None: + cond_snd = lambda x: True + if cond is None: + cond = lambda x, y: True + + fst = list(filter(cond_fst, self._model.tree.nodes)) + snd = list(filter(cond_snd, self._model.tree.nodes)) + for t0 in fst: + for t1 in snd: + if cond(t0,t1): yield (t0,t1) # ================================================================# diff --git a/slothy/targets/arm_v81m/cortex_m85r1.py b/slothy/targets/arm_v81m/cortex_m85r1.py index f598d826..1d246578 100644 --- a/slothy/targets/arm_v81m/cortex_m85r1.py +++ b/slothy/targets/arm_v81m/cortex_m85r1.py @@ -77,17 +77,19 @@ def __repr__(self): # Opaque function called by SLOTHY to add further microarchitecture- # specific constraints which are not encapsulated by the general framework. def add_further_constraints(slothy): - for t0, t1 in slothy.get_inst_pairs(): - for t2, t3 in slothy.get_inst_pairs(): - if (not t0.inst.is_load_store_instruction() and - t1.inst.is_vector_load() and - t2.inst.is_vector_store() and - t3.inst.is_vector_load()): - b = [ slothy._NewBoolVar("") for _ in range(0,3) ] - slothy._AddAtLeastOne(b) - slothy._Add(t1.program_start_var != t0.program_start_var + 1).OnlyEnforceIf(b[0]) - slothy._Add(t2.program_start_var != t1.program_start_var + 1).OnlyEnforceIf(b[1]) - slothy._Add(t3.program_start_var != t2.program_start_var + 1).OnlyEnforceIf(b[2]) + t0_t1 = slothy.get_inst_pairs( + cond_fst=lambda t: not t.inst.is_load_store_instruction(), + cond_snd=lambda t: t.inst.is_vector_load()) + t2_t3 = slothy.get_inst_pairs( + cond_fst=lambda t: t.inst.is_vector_store(), + cond_snd=lambda t: t.inst.is_vector_load()) + for t0, t1 in t0_t1: + for t2, t3 in t2_t3: + b = [ slothy._NewBoolVar("") for _ in range(0,3) ] + slothy._AddAtLeastOne(b) + slothy._Add(t1.program_start_var != t0.program_start_var + 1).OnlyEnforceIf(b[0]) + slothy._Add(t2.program_start_var != t1.program_start_var + 1).OnlyEnforceIf(b[1]) + slothy._Add(t3.program_start_var != t2.program_start_var + 1).OnlyEnforceIf(b[2]) for t0, t1 in slothy.get_inst_pairs():