From b5016fc85e7fe1476a2607bd4cbfab90f8d1c0be Mon Sep 17 00:00:00 2001 From: Christian Dietrich Date: Wed, 12 Aug 2015 09:18:36 +0200 Subject: [PATCH] generator/SSE: alternative SSE with APP-FSM The symbolic system execution is now able to enumerate all possible system states with two different approaches. Either we can use the "old" version which uses states with blocks to be executed in the next step, like it is described in LCTES'15 (Dietrich et. al). Or we can use the application finite state machines as basis. These state machines are smaller (lesser nodes) than the application's CFG. They are based on the task's ICFG. Change-Id: I05e050ed3f39bd18ecf86b4d7bb423b4ce0825e0 --- app/bcc1/task1/CMakeLists.txt | 8 +- generator/analysis/ApplicationFSM.py | 146 +++++++- generator/analysis/DynamicPriorityAnalysis.py | 6 +- generator/analysis/PreciseSystemState.py | 119 ++++-- generator/analysis/PrioritySpreadingPass.py | 2 + generator/analysis/Sporadic.py | 11 +- generator/analysis/Subtask.py | 2 + generator/analysis/SymbolicSystemExecution.py | 106 ++++-- generator/analysis/SystemSemantic.py | 342 +++++++++++------- generator/analysis/SystemState.py | 9 +- generator/analysis/SystemStateFlow.py | 22 +- generator/analysis/common.py | 4 +- generator/analysis/types.py | 7 +- generator/main.py | 4 +- generator/tools/__init__.py | 11 + .../transform/FiniteStateMachineBuilder.py | 56 ++- 16 files changed, 622 insertions(+), 233 deletions(-) diff --git a/app/bcc1/task1/CMakeLists.txt b/app/bcc1/task1/CMakeLists.txt index 63696c0..5448827 100644 --- a/app/bcc1/task1/CMakeLists.txt +++ b/app/bcc1/task1/CMakeLists.txt @@ -7,6 +7,11 @@ DOSEK_BINARY( a.cc ) +# This has to be done, since FSM is currently build with the APP-FSM +# method and not the CFG->GCFG method for SSE. +config_valid(VALID --systemcalls normal) +if(VALID) + DOSEK_BINARY( NAME bcc1_task1a_sse SYSTEM_DESC system.oil @@ -15,7 +20,8 @@ DOSEK_BINARY( GENERATOR_ARGS -fgen-asserts -fsse TEST_ISO a.cc -) + ) +endif() DOSEK_BINARY( NAME bcc1_task1b diff --git a/generator/analysis/ApplicationFSM.py b/generator/analysis/ApplicationFSM.py index b746c06..b494e62 100644 --- a/generator/analysis/ApplicationFSM.py +++ b/generator/analysis/ApplicationFSM.py @@ -1,6 +1,6 @@ from .common import * from .Analysis import Analysis -from .AtomicBasicBlock import E, S +from .AtomicBasicBlock import E, S, AtomicBasicBlock from .Function import Function from datastructures.fsm import * from collections import defaultdict @@ -32,7 +32,7 @@ class ApplicationFSM(Analysis, GraphObject): for subtask in self.system_graph.subtasks: wrapper = GraphObjectContainer(str(subtask), color='red') nodes = {} - for trans in subtask.conf.fsm.transitions: + for trans in subtask.fsm.transitions: if not trans.source in nodes: nodes[trans.source] = Node(None, str(trans.source), color='black') if not trans.target in nodes: @@ -54,7 +54,12 @@ class ApplicationFSM(Analysis, GraphObject): def block_functor(in_edge, cur_abb): transitions = [] - # ICFG Entry transition + # Here we do the following. Each Edge becomes a state in our finite state machine. + # So from + # ---[in_edge]--> [in_edge.target] --[out_edge]--> + # we make + # [in_edge] --[in_edge.target == ABB]--> [out_edge] + # Entry and exit nodes are handleded differently if cur_abb == subtask.entry_abb: in_edge = None out_edge = cur_abb.get_outgoing_edges(self.get_edge_filter())[0] @@ -63,6 +68,12 @@ class ApplicationFSM(Analysis, GraphObject): for out_edge in cur_abb.get_outgoing_edges(self.get_edge_filter()): # Every Edge becomes a state, every state becomes an edge transitions.append(Transition(in_edge, out_edge, out_edge.target)) + # Exit nodes are different + if cur_abb == subtask.exit_abb: + out_edge = None + # Every Edge becomes a state, every state becomes an edge + transitions.append(Transition(in_edge, -1, None)) + event = Event(cur_abb, transitions) ret.add_event(event) @@ -76,7 +87,7 @@ class ApplicationFSM(Analysis, GraphObject): ret.initial_state = None return ret - def __epsilon_elimination(self, fsm): + def epsilon_elimination(self, fsm): """The epsilon elimination pass makes every computation event/transition to an epsilon transition. With the standard FSM epslion elimination, we reduce the FSM @@ -91,7 +102,7 @@ class ApplicationFSM(Analysis, GraphObject): # epsilon set is the set of states, that can be reached from # one state by using only epsilon transitions. In our case, # all computation blocks are epsilon transitions. - def is_epsilon_transition(transition): + def is_epsilon_transition(trans): return trans.event.isA(S.computation) changed = True while changed: @@ -138,8 +149,125 @@ class ApplicationFSM(Analysis, GraphObject): app_fsm = self.__to_fsm(subtask) app_fsm.rename(states=True) - app_fsm = self.__epsilon_elimination(app_fsm) + app_fsm = self.epsilon_elimination(app_fsm) + subtask.fsm = app_fsm + subtask.ApplicationFSMIterator = ApplicationFSMIterator.create + + # Rewrite AlarmSubtask + if self.system_graph.AlarmHandlerSubtask: + fsm = self.system_graph.AlarmHandlerSubtask.fsm + for E in fsm.events: + if not E.name.isA([S.CheckAlarm, S.iret]): + continue + old_states = set([T.source for T in E.transitions]) + new_state = [T.source for T in E.transitions][0] + def renamer(state): + if state in old_states: + return new_state + return state + fsm.rename(states = renamer) + tgt = {(T.source, T.target): T for T in E.transitions} + E.transitions = tgt.values() + + for trans in self.system_graph.idle_subtask.fsm.transitions: + if trans.event.isA(S.Idle): + trans.target = trans.source + +fsm_iter_cache = {} + +class ApplicationFSMIterator: + """The Application FSM Iterator is a wrapper for APP-FSM states to be + used by the symbolic system execution. It has a similar + interface to the AtomicBasicBlock. + """ + @staticmethod + def create(subtask, state): + if not (subtask, state) in fsm_iter_cache: + it = ApplicationFSMIterator() + it.__create__(subtask, state) + fsm_iter_cache[(subtask, state)] = it + return fsm_iter_cache[(subtask, state)] + + def __init__(self): + pass + + def __create__(self, subtask, state): + self.subtask = subtask + self.__state = state + self.dynamic_priority = self.__consistent( + self.__originating_blocks(), + lambda x: x.dynamic_priority + ) + computations = self.__originating_blocks(True) + if computations: + self.interrupt_block_all = self.__consistent( + computations, + lambda x: x.interrupt_block_all + ) + self.interrupt_block_os = self.__consistent( + computations, + lambda x: x.interrupt_block_os + ) + + self.possible_systemcalls = set() + for trans in self.subtask.fsm.get_outgoing_transitions(self.__state): + self.possible_systemcalls.add(trans.event) + + if self.__state != self.subtask.fsm.initial_state \ + and self.subtask.is_user_thread(): + # Besides the initial state, we give back an additional + # computation block as possible system-call. + edges = self.subtask.fsm.state_mapping[self.__state] + computations = [x.event for x in edges if x.event.isA(S.computation)] + abb = AtomicBasicBlock(self.subtask.system_graph) + abb.make_it_a_syscall(S.CheckIRQ, computations) + self.possible_systemcalls.add(abb) + + self.possible_systemcalls = list(self.possible_systemcalls) + + + + def __originating_blocks(self, only_computation = False): + blocks = [x.event for x in self.subtask.fsm.state_mapping[self.__state]] + if only_computation: + blocks = [x for x in blocks if x.isA(S.computation)] + return blocks + + def __consistent(self, seq, mapper=lambda x:x): + ret = [mapper(x) for x in seq] + assert len(ret) > 0, "To have a consistent value, at least one value must be present" + assert all([ret[0] == ret[i] for i in range(1, len(ret))]), "Inconsistent %s" % seq + return ret[0] + + def __repr__(self): + try: + return "" %(self.subtask.name, self.__state, self.dynamic_priority) + except: + return "" %(self.subtask.name, self.__state) + + def isA(self, cls): + return self.__consistent( + self.__originating_blocks(), + lambda x: x.isA(cls) + ) + + def path(self): + return "%s/%d" % (self.subtask, self.__state) + + @property + def abb_id(self): + return self.__state + + + def get_blocks(self): + return self.__originating_blocks() + + def next_iterators(self, event): + ret = [] + for trans in self.subtask.fsm.get_outgoing_transitions(self.__state): + if trans.event == event: + ret.append(self.create(self.subtask, trans.target)) + # No computation block should ever arrive here as event + assert not event.isA(S.computation) + return ret - subtask.conf.fsm = app_fsm - print() - print(app_fsm) diff --git a/generator/analysis/DynamicPriorityAnalysis.py b/generator/analysis/DynamicPriorityAnalysis.py index ca7dd32..fb02e96 100644 --- a/generator/analysis/DynamicPriorityAnalysis.py +++ b/generator/analysis/DynamicPriorityAnalysis.py @@ -102,8 +102,10 @@ class DynamicPriorityAnalysis(Analysis): # Blocks within a non-preemtable subtask cannot be # rescheduled (except for ISR2) if not abb.function.subtask.conf.preemptable and \ - not abb.isA(S.kickoff): + not abb.isA(S.kickoff) and \ + not abb.subtask.conf.is_isr: dynamic_priority = RES_SCHEDULER.conf.static_priority + # Each abb has a dynamic priority abb.dynamic_priority = dynamic_priority @@ -112,7 +114,7 @@ class DynamicPriorityAnalysis(Analysis): # StartOS), the priority is the idle priority. for syscall in self.system_graph.syscalls: precessors = syscall.get_incoming_nodes(E.task_level) - if syscall.isA(S.kickoff) or syscall.isA(S.WaitEvent): + if syscall.isA(S.kickoff): syscall.dynamic_priority = syscall.function.subtask.static_priority elif len(precessors) == 1: syscall.dynamic_priority = precessors[0].dynamic_priority diff --git a/generator/analysis/PreciseSystemState.py b/generator/analysis/PreciseSystemState.py index 168cea4..249261e 100644 --- a/generator/analysis/PreciseSystemState.py +++ b/generator/analysis/PreciseSystemState.py @@ -19,45 +19,51 @@ class PreciseSystemState(): __slots__ = ["frozen", "states", "call_stack", "continuations", "current_abb", "__hash", "__next_states", "__prev_states", "events"] - def __init__(self, system_graph): + def __init__(self, system_graph, init = True): PreciseSystemState.system_graph = system_graph self.frozen = False + self.__hash = None + self.__next_states = [] + self.__prev_states = [] + + if not init: + return size = len(self.system_graph.subtasks) self.states = [0] * size self.continuations = [None] * size self.current_abb = None - self.__hash = None - self.__next_states = [] - self.__prev_states = [] self.events = [0] * size self.call_stack = [] for i in range(0, size): self.call_stack.append(list()) - def add_cfg_edge(self, block, ty): - self.__next_states.append((ty, block)) - block.__prev_states.append((ty, self)) + def new(self): + return PreciseSystemState(self.system_graph) + + def add_cfg_edge(self, block, ty, label = None): + self.__next_states.append((ty, block, label)) + block.__prev_states.append((ty, self, label)) def remove_cfg_edge(self, block, ty): for i, elem in enumerate(self.__next_states): - if elem == (ty, block): + if tuple(elem[0:2]) == (ty, block): del self.__next_states[i] break for i, elem in enumerate(block.__prev_states): - if elem == (ty, self): + if tuple(elem[0:2]) == (ty, self): del block.__prev_states[i] break def get_outgoing_nodes(self, ty): - return [block for Ty,block in self.__next_states if Ty == ty] + return [block for Ty,block,label in self.__next_states if Ty == ty] def get_incoming_nodes(self, ty): - return [block for Ty,block in self.__prev_states if Ty == ty] + return [block for Ty,block,label in self.__prev_states if Ty == ty] - def new(self): - return PreciseSystemState(self.system_graph) + def get_outgoing_edges(self, ty): + return [(block, label) for Ty,block,label in self.__next_states if Ty == ty] def copy_if_needed(self, multiple=None): if self.frozen: @@ -74,17 +80,18 @@ class PreciseSystemState(): # Increase the copy counter SystemState.copy_count += 1 - state = self.new() + # For faster copying, we use the do-not-init constructor and + # do everything ourselves here. + state = PreciseSystemState(self.system_graph, init = False) state.current_abb = self.current_abb - def copyto(dst, src): - dst[:] = src - - copyto(state.states, self.states) - copyto(state.continuations, self.continuations) - copyto(state.events, self.events) + # Shallow copies + state.states = self.states[:] + state.continuations = self.continuations[:] + state.events = self.events[:] + state.call_stack = [] for subtask_id in range(0, len(self.states)): - state.call_stack[subtask_id] = list(self.call_stack[subtask_id]) + state.call_stack.append(self.call_stack[subtask_id][:]) return state @@ -116,6 +123,9 @@ class PreciseSystemState(): def is_surely_ready(self, subtask): return self.states[subtask.subtask_id] == self.READY + def is_surely_waiting(self, subtask): + return self.states[subtask.subtask_id] == self.WAITING + def is_maybe_ready(self, subtask): return self.READY & self.states[subtask.subtask_id] @@ -129,9 +139,13 @@ class PreciseSystemState(): def get_continuations(self, subtask): if type(subtask) == int: return set([self.continuations[subtask]]) - return set([self.continuations[subtask.subtask_id]]) + def get_continuation(self, subtask): + if type(subtask) == int: + return self.continuations[subtask] + return self.continuations[subtask.subtask_id] + def set_continuation(self, subtask, abb): assert not self.frozen self.continuations[subtask.subtask_id] = abb @@ -160,36 +174,72 @@ class PreciseSystemState(): return self.call_stack[subtask.subtask_id] # Events + def __events(self, subtask, set_events = None, set_block_list = None): + events = self.events[subtask.subtask_id] & 0xffff + block_list = (self.events[subtask.subtask_id] >> 16) & 0xffff + if not set_events is None: + assert (set_events & 0xffff == set_events) + self.events[subtask.subtask_id] = (set_events | (block_list << 16)) + events = set_events + if not set_block_list is None: + assert (set_block_list & 0xffff == set_block_list) + self.events[subtask.subtask_id] = (events | (set_block_list << 16)) + block_list = set_block_list + + return (events, block_list) + def get_events(self, subtask): """Return a tuple (None, set)""" - events = self.events[subtask.subtask_id] + events, _ = self.__events(subtask) return (subtask.event_mask_valid ^ events, events) def set_events(self, subtask, event_list): mask = Event.combine_event_masks(event_list) - self.events[subtask.subtask_id] |= mask + self.__events(subtask, set_events = mask) def clear_events(self, subtask, event_list): mask = Event.combine_event_masks(event_list) - self.events[subtask.subtask_id] &= ~mask + events, bl = self.__events(subtask) + events &= ~mask + assert bl == 0 + self.__events(subtask, set_events = events) - def maybe_waiting(self, subtask, event_list): - """Returns True, if the task may block be waiting at this point""" + def clear_block_list(self, subtask): + self.__events(subtask, set_block_list = 0) + + def set_block_list(self, subtask, event_list): mask = Event.combine_event_masks(event_list) - if (self.events[subtask.subtask_id] & mask) == 0: + self.__events(subtask, set_block_list = mask) + + def get_block_list(self, subtask): + events, bl = self.__events(subtask) + return bl + + def maybe_waiting(self, subtask): + """Returns True, if the task may block be waiting at this point""" + events, block_list = self.__events(subtask) + if (block_list & events) == 0: return True return False - def maybe_not_waiting(self, subtask, event_list): + def maybe_not_waiting(self, subtask): """Returns True, if the task may be continue without blocking""" # In the precise system state, this is the exact opposite - return not self.maybe_waiting(subtask, event_list) + return not self.maybe_waiting(subtask) def is_event_set(self, subtask, event): - return (self.events[subtask.subtask_id] & event.event_mask) != 0 + events, block_list = self.__events(subtask) + + return (events & event.event_mask) != 0 + + def is_event_waiting(self, subtask, event): + events, block_list = self.__events(subtask) + return (block_list & event.event_mask) != 0 def is_event_cleared(self, subtask, event): - return (self.events[subtask.subtask_id] & event.event_mask) == 0 + events, block_list = self.__events(subtask) + + return (events & event.event_mask) == 0 ## Continuation accesors def was_surely_not_kickoffed(self, subtask): @@ -235,7 +285,7 @@ class PreciseSystemState(): @property def current_subtask(self): - return self.current_abb.function.subtask + return self.current_abb.subtask def merge_with(self, other): """Returns a newly created state that is the result of the merge of @@ -303,6 +353,7 @@ class PreciseSystemState(): for event in subtask.events: SET = self.is_event_set(subtask, event) CLEARED = self.is_event_cleared(subtask, event) + WAITING = self.is_event_waiting(subtask, event) if SET and CLEARED: ret.append("%s:*" % event.conf.name) elif SET: @@ -310,6 +361,8 @@ class PreciseSystemState(): else: assert CLEARED ret.append("%s:0" % event.conf.name) + if WAITING: + ret.append("W") return " ".join(ret) diff --git a/generator/analysis/PrioritySpreadingPass.py b/generator/analysis/PrioritySpreadingPass.py index 7a3ead9..64f9a79 100644 --- a/generator/analysis/PrioritySpreadingPass.py +++ b/generator/analysis/PrioritySpreadingPass.py @@ -1,3 +1,4 @@ +import logging from .Analysis import Analysis from .Subtask import Subtask @@ -34,6 +35,7 @@ class PrioritySpreadingPass(Analysis): p[0] = prio p[1].conf.static_priority = prio self.prio_to_participant[prio] = p[1] + logging.debug("Prio %d: %s", prio, p[1]) prio += 1 assert participants[0][1] == self.system_graph.get(Subtask, "Idle") diff --git a/generator/analysis/Sporadic.py b/generator/analysis/Sporadic.py index c4de7f7..96a5926 100644 --- a/generator/analysis/Sporadic.py +++ b/generator/analysis/Sporadic.py @@ -41,13 +41,18 @@ class SporadicEvent: assert state.is_surely_suspended(self.handler), (state, self.handler) # Save current IP - current_subtask = state.current_abb.function.subtask + current_subtask = state.current_abb.subtask copy_state.set_continuation(current_subtask, state.current_abb) # Dispatch to Event Handler - copy_state.set_continuation(self.handler, self.handler.entry_abb) + entry_abb = self.handler.entry_abb + # If we use the APP-FSM method to do the SSE, then we have + # this field available in the handler (== ISR Subtask) + if hasattr(self.handler, "ApplicationFSMIterator"): + entry_abb = self.handler.ApplicationFSMIterator(self.handler, self.handler.fsm.initial_state) + copy_state.set_continuation(self.handler, entry_abb) copy_state.set_ready(self.handler) - copy_state.current_abb = self.handler.entry_abb + copy_state.current_abb = entry_abb return copy_state diff --git a/generator/analysis/Subtask.py b/generator/analysis/Subtask.py index b1c0284..6cf530a 100644 --- a/generator/analysis/Subtask.py +++ b/generator/analysis/Subtask.py @@ -18,6 +18,8 @@ class Subtask(Function, SystemObject): self._events = {} # A mask that is the combination of all event masks self.event_mask_valid = 0 + # Field is used by ApplicationFSM + self.fsm = None def find(self, cls, name): if issubclass(cls, Event): diff --git a/generator/analysis/SymbolicSystemExecution.py b/generator/analysis/SymbolicSystemExecution.py index 2239e83..536649b 100644 --- a/generator/analysis/SymbolicSystemExecution.py +++ b/generator/analysis/SymbolicSystemExecution.py @@ -23,11 +23,13 @@ class SymbolicSystemExecution(Analysis, GraphObject): """ pass_alias = "sse" - def __init__(self): + def __init__(self, use_app_fsm = False): Analysis.__init__(self) GraphObject.__init__(self, "SymbolicSystemState", root = True) self.states = None self.states_by_abb = None + # Should the application fsm pass be used as a basis + self.use_app_fsm = use_app_fsm # A member for the RunningTask analysis self.running_task = None @@ -42,6 +44,8 @@ class SymbolicSystemExecution(Analysis, GraphObject): def requires(self): # We require all possible system edges to be contructed + if self.use_app_fsm: + return ["ApplicationFSM"] return ["DynamicPriorityAnalysis", "InterruptControlAnalysis"] def get_edge_filter(self): @@ -62,22 +66,22 @@ class SymbolicSystemExecution(Analysis, GraphObject): M[state] = wrapper cont = GraphObjectContainer(str(abb), color="red", subobjects=subobjs) - cont.data = {"ABB": str(abb), "func": abb.function.name} + cont.data = {"ABB": abb.path()} cont.abb = abb ret.append(cont) for state, wrapper in M.items(): for next_state in state.get_outgoing_nodes(StateTransition): cont.edges.append(Edge(wrapper, M[next_state], color="red")) - for next_state in state.get_outgoing_nodes(SavedStateTransition): - cont.edges.append(Edge(wrapper, M[next_state], color="green")) + for next_state, label in state.get_outgoing_edges(SavedStateTransition): + cont.edges.append(Edge(wrapper, M[next_state], color="green", label=label)) ret = list(sorted(ret, key=lambda x: x.abb.abb_id)) return ret - def state_transition(self, source_block, source_state, target_block, target_state): + def state_transition(self, syscall, source_block, source_state, target_block, target_state): # print(source_block.path(),"->", target_block.path()) # Do not allow self loops #if source_state == target_state: @@ -88,26 +92,40 @@ class SymbolicSystemExecution(Analysis, GraphObject): assert False if target_state in self.states: real_instance = self.states[target_state] - source_state.add_cfg_edge(real_instance, StateTransition) + source_state.add_cfg_edge(real_instance, StateTransition, label=syscall) else: - self.working_stack.push((source_state, target_state)) + self.working_stack.push((syscall, source_state, target_state)) def state_functor(self, state): - # Do the System Call - after_states = self.system_call_semantic.do_SystemCall( - state.current_abb, state, self.transitions) + def state_functor__(state_ptr): + after_states = self.system_call_semantic.do_SystemCall( + state_ptr.current_abb, state_ptr, self.transitions) + + # Schedule on each possible block + for syscall, next_state in after_states: + edges = list(self.system_call_semantic.schedule(state_ptr.current_abb, next_state.copy())) + for (source, target, new_state) in edges: + assert new_state.frozen + # Re-step system state, if syscall is None. (Happens in CheckAlarm for use_app_fsm) + if syscall == None: + for (syscall, _, target, new_state) in state_functor__(new_state): + yield (syscall, source, target, new_state) + else: + yield (syscall, source, target, new_state) - # Schedule on each possible block - for next_state in after_states: - self.system_call_semantic.schedule(state.current_abb, next_state, - lambda source, target, new_state: \ - self.state_transition(source, state, target, new_state)) + for (syscall, source, target, new_state) in state_functor__(state): + # otherwise: Add state transition + self.state_transition(syscall, source, state, target, new_state) - def do_computation_with_sporadic_events(self, block, before): - after_states = self.system_call_semantic.do_computation_with_callstack(block, before) + def do_computation_with_sporadic_events(self, cont, before, syscall): + after_states = self.system_call_semantic.do_computation_with_callstack(cont, before, syscall) + return after_states + self.do_sporadic_events(cont, before, syscall) + def do_sporadic_events(self, cont, before, syscall): + after_states = [] # Handle sporadic events events = 0 + sporadic_events = list(self.system_graph.isrs) if self.system_graph.AlarmHandlerSubtask: sporadic_events.append(self.system_graph.AlarmHandlerSubtask) @@ -117,18 +135,30 @@ class SymbolicSystemExecution(Analysis, GraphObject): continue after = sporadic_event.trigger(before) - after_states.append(after) + after_states.append((syscall, after)) events += 1 - block.sporadic_trigger_count = events + cont.sporadic_trigger_count = events return after_states + def do_CheckIRQ(self, cont, before, syscall): + after_states = self.do_sporadic_events(cont, before, syscall) + ret = [] + for checkirq, kickoff_state in after_states: + # We return None here as the issuing systemcall, in order + # to redo the systemcall immediately. This results in no + # CheckIRQ edges! + ret.append( (None, kickoff_state) ) + + return ret + + def do(self): old_copy_count = SystemState.copy_count self.running_task = self.get_analysis(CurrentRunningSubtask.name()) # Instantiate a new system call semantic - self.system_call_semantic = SystemCallSemantic(self.system_graph, self.running_task) + self.system_call_semantic = SystemCallSemantic(self.system_graph, self.use_app_fsm) scc = self.system_call_semantic self.transitions = {S.StartOS : scc.do_StartOS, @@ -161,6 +191,8 @@ class SymbolicSystemExecution(Analysis, GraphObject): S.GetEvent : scc.do_computation, # ignore # Alarm handler support S.CheckAlarm : scc.do_CheckAlarm, + # IRQ Support for ApplicationFSM + S.CheckIRQ : self.do_CheckIRQ, S.Idle : scc.do_Idle, S.iret : scc.do_TerminateTask} @@ -176,25 +208,25 @@ class SymbolicSystemExecution(Analysis, GraphObject): # first part of the tuple is none, we have the starting # condition. self.working_stack = stack() - self.working_stack.push((None, before_StartOS)) + self.working_stack.push((None, None, before_StartOS)) state_count = 0 ignored_count = 0 while not self.working_stack.isEmpty(): # Current is a system state and its state predecessor - before_current, current = self.working_stack.pop() + old_syscall, before_current, current = self.working_stack.pop() # State was already marked as done! if current in self.states: # Although it was already done, we have to add the edge # noted in the working stack. current = self.states[current] - before_current.add_cfg_edge(current, StateTransition) + before_current.add_cfg_edge(current, StateTransition, label = old_syscall) ignored_count += 1 continue elif before_current: # Add the state edge - before_current.add_cfg_edge(current, StateTransition) + before_current.add_cfg_edge(current, StateTransition, label = old_syscall) # The current state is marked as done. This dictionary is # used to translate all equal system states to a single instance/object. self.states[current] = current @@ -211,11 +243,12 @@ class SymbolicSystemExecution(Analysis, GraphObject): # Before we transform the state graph, we copy the original # state graph away for outgoing_state in self.states: - for incoming_state in outgoing_state.get_outgoing_nodes(StateTransition): - outgoing_state.add_cfg_edge(incoming_state, SavedStateTransition) + for incoming_state, label in outgoing_state.get_outgoing_edges(StateTransition): + outgoing_state.add_cfg_edge(incoming_state, SavedStateTransition, label=label) # Cut out the isr transitions to match the SSF GCFG - self.transform_isr_transitions() + if not self.use_app_fsm: + self.transform_isr_transitions() # Group States by ABB self.states_by_abb = group_by(self.states, "current_abb") @@ -233,9 +266,9 @@ class SymbolicSystemExecution(Analysis, GraphObject): # level to interrupt level. We connect the interrupt handler # continuation with the block that activates the interrupt. def is_isr_state(state): - if not state.current_abb.function.subtask: + if not state.current_abb.subtask: return False - return state.current_abb.function.subtask.conf.is_isr + return state.current_abb.subtask.conf.is_isr del_edges = [] add_edges = [] for app_level in [x for x in self.states if not is_isr_state(x)]: @@ -264,6 +297,8 @@ class SymbolicSystemExecution(Analysis, GraphObject): source.add_cfg_edge(target, StateTransition) def statistics(self): + if self.use_app_fsm: + return ################################################################ # Statistics ################################################################ @@ -315,10 +350,21 @@ class SymbolicSystemExecution(Analysis, GraphObject): state_ids = set([id(X) for X in self.states]) for sse_state in self.states: followup_states = set() + # All incomin nodes have to be valid states for X in sse_state.get_incoming_nodes(SavedStateTransition): assert id(X) in state_ids, X + # All outgoing nodes have to be states, and every state + # may only be once there. for X in sse_state.get_outgoing_nodes(SavedStateTransition): - assert not id(X) in followup_states + # With FSM-SSE: We can have the same sse_state as + # successor through multiple different systemcalls. + # ---- TerminateTask/ABB12 --- + # / \ + # S1 S2 + # \ / + # ----- TerminateTask/ABB11 ---- + assert not id(X) in followup_states or self.use_app_fsm, \ + "Doubled followup state"+ str(sse_state) + str(sse_state.current_abb.possible_systemcalls) + str(X) followup_states.add(id(X)) assert id(X) in state_ids, X diff --git a/generator/analysis/SystemSemantic.py b/generator/analysis/SystemSemantic.py index e8d7d61..1bc50dd 100644 --- a/generator/analysis/SystemSemantic.py +++ b/generator/analysis/SystemSemantic.py @@ -6,14 +6,35 @@ from .Event import Event from .common import Node, Edge, EdgeType, NodeType from .SystemState import SystemState from .PreciseSystemState import PreciseSystemState +from .ApplicationFSM import ApplicationFSMIterator class SystemCallSemantic: - def __init__(self, system_graph, running_task): - self.running_task = running_task + def __init__(self, system_graph, use_app_fsm = False): self.system_graph = system_graph + self.use_app_fsm = use_app_fsm - def do_StartOS(self, block, before): + def __entry_point(self, subtask): + if self.use_app_fsm: + return ApplicationFSMIterator.create(subtask, subtask.fsm.initial_state) + else: + return subtask.entry_abb + + def __next_continuations(self, cont, before_state, action): + assert type(self.use_app_fsm) == bool + if self.use_app_fsm: + return cont.next_iterators(action) + else: + assert cont == action + return action.get_outgoing_nodes(E.task_level) + + def __next_continuation(self, cont, before_state, action): + ret = self.__next_continuations(cont, before_state, action) + assert len(ret) == 1 + return ret[0] + + + def do_StartOS(self, _, before, syscall): state = before.copy_if_needed() # In the StartOS node all tasks are suspended before, # and afterwards the idle loop and the autostarted @@ -23,184 +44,194 @@ class SystemCallSemantic: state.set_ready(subtask) else: state.set_suspended(subtask) - state.set_continuation(subtask, subtask.entry_abb) - state.current_abb = block - return [state] + state.set_continuation(subtask, self.__entry_point(subtask)) + return [(syscall, state)] - def do_ActivateTask(self, block, before): + def do_ActivateTask(self, cont, before, syscall): after = before.copy_if_needed() # EnsureComputationBlocks ensures that after an activate task # only one ABB can be located - cont = block.definite_after(E.task_level) - after.set_continuation(self.running_task.for_abb(block), - cont) - activated = block.arguments[0] - if not after.is_surely_ready(activated): - after.add_continuation(activated, activated.entry_abb) + next_cont = self.__next_continuation(cont, before, syscall) + after.set_continuation(cont.subtask, next_cont) + activated = syscall.arguments[0] + if not (after.is_surely_ready(activated) or after.is_surely_waiting(activated)): + after.add_continuation(activated, self.__entry_point(activated)) # Clear the events after.clear_events(activated, activated.events) after.set_ready(activated) - return [after] + return [(syscall, after)] - def do_TerminateTask(self, block, before): + def do_TerminateTask(self, cont, before, syscall): after = before.copy_if_needed() - calling_task = self.running_task.for_abb(block) - after.set_continuation(calling_task, calling_task.entry_abb) + calling_task = cont.subtask + after.set_continuation(calling_task, self.__entry_point(calling_task)) after.set_suspended(calling_task) - return [after] + return [(syscall, after)] - def do_ChainTask(self, block, before): + def do_ChainTask(self, cont, before, syscall): after = before.copy_if_needed() # Suspend the current Task, this also sets the # continuations correctly - calling_task = self.running_task.for_abb(block) - after.set_continuation(calling_task, calling_task.entry_abb) + calling_task = cont.subtask + after.set_continuation(calling_task, self.__entry_point(calling_task)) after.set_suspended(calling_task) # Activate other Task - activated = block.arguments[0] - if not after.is_surely_ready(block.arguments[0]): - after.add_continuation(activated, activated.entry_abb) + activated = syscall.arguments[0] + if not (after.is_surely_ready(activated) or after.is_surely_waiting(activated)): + after.add_continuation(activated, self.__entry_point(activated)) # Clear the events after.clear_events(activated, activated.events) after.set_ready(activated) - return [after] + return [(syscall, after)] - def do_AdvanceCounter(self, block, before): + def do_AdvanceCounter(self, cont, before, syscall): # Either we directly return notrigger = before.copy_if_needed() - cont = block.definite_after(E.task_level) - notrigger.set_continuation(self.running_task.for_abb(block), - cont) - ret = [notrigger] + cont_after = cont.definite_after(E.task_level) + notrigger.set_continuation(cont.subtask, cont_after) + ret = [(syscall, notrigger)] # Or we trigger the counter - counter = block.arguments[0] + counter = syscall.arguments[0] sporadic_events = [] for alarm in self.system_graph.alarms: if not(isinstance(alarm , Alarm) and alarm.conf.counter == counter): continue after = before.copy() - cont = block.definite_after(E.task_level) - after.set_continuation(self.running_task.for_abb(block), - cont) + cont_after = cont.definite_after(E.task_level) + after.set_continuation(cont.subtask, cont_after) activated = alarm.conf.subtask assert alarm.conf.event is None if not after.is_surely_ready(activated): - after.add_continuation(activated, activated.entry_abb) + after.add_continuation(activated, self.__entry_point(activated)) # Clear the events after.clear_events(activated, activated.events) after.set_ready(activated) - ret.append(after) + ret.append((syscall, after)) assert len(ret) > 1, "No Alarm for Soft-Counter defined (%s)" % counter return ret - def do_WaitEvent(self, block, before): - event_list = block.arguments[0] - calling_task = block.subtask + def do_WaitEvent(self, cont, before, syscall): + event_list = syscall.arguments[0] + calling_task = cont.subtask ret = [] - if before.maybe_waiting(calling_task, event_list): - after = before.copy() + after = before.copy() + after.set_block_list(calling_task, event_list) + if after.maybe_waiting(calling_task): after.set_waiting(calling_task) - after.set_continuation(calling_task, block) - ret.append(after) + next_cont = self.__next_continuation(cont, before, syscall) + after.set_continuation(calling_task, next_cont) + ret.append((syscall, after)) - if before.maybe_not_waiting(calling_task, event_list): - after = before.copy() + after = before.copy() + after.set_block_list(calling_task, event_list) + if after.maybe_not_waiting(calling_task): after.set_ready(calling_task) - cont = block.definite_after(E.task_level) - after.set_continuation(calling_task, cont) - ret.append(after) + after.clear_block_list(calling_task) + next_cont = self.__next_continuation(cont, before, syscall) + after.set_continuation(calling_task, next_cont) + ret.append((syscall, after)) return ret - def do_SetEvent(self, block, before): - event_list = block.arguments[0] - calling_task = block.subtask + def do_SetEvent(self, cont, before, syscall): + event_list = syscall.arguments[0] + calling_task = cont.subtask unblocked_task = event_list[0].task after = before.copy_if_needed() after.set_events(unblocked_task, event_list) - - waiting_block = after.get_continuations(unblocked_task) - assert(len(waiting_block) == 1) - waiting_block = list(waiting_block)[0] - if waiting_block.isA(S.WaitEvent): - # Recheck the blocking state - block_list = waiting_block.arguments[0] - # Check if the unblocked task is still blocking - if after.maybe_not_waiting(unblocked_task, block_list): - after.set_ready(unblocked_task) + if after.maybe_not_waiting(unblocked_task): + after.set_ready(unblocked_task) + # WE DO NOT CLEAR THE BLOCK LIST HERE, BUT IN THE NEXT + # DISPATCH. By this, we indicated, that the block was + # woken up (important for non-preemptable extended tasks) + # Look at the dispatcher # We've done our system call, continue at successor - cont = block.definite_after(E.task_level) + cont = self.__next_continuation(cont, before, syscall) after.set_continuation(calling_task, cont) - return [after] + return [(syscall, after)] - def do_ClearEvent(self, block, before): - event_list = block.arguments[0] - calling_task = block.subtask + def do_ClearEvent(self, cont, before, syscall): + event_list = syscall.arguments[0] + calling_task = cont.subtask after = before.copy_if_needed() after.clear_events(calling_task, event_list) - cont = block.definite_after(E.task_level) + # We've done our system call, continue at successor + cont = self.__next_continuation(cont, before, syscall) after.set_continuation(calling_task, cont) - return [after] + return [(syscall, after)] + + def do_CheckAlarm(self, cont, before, syscall): + alarm_object = syscall.arguments[0] + next_cont = self.__next_continuations(cont, before, syscall) + syscalls = next_cont[:] # COPY! + if self.use_app_fsm: + for idx, cont in enumerate(next_cont): + follower = cont.possible_systemcalls + assert len(follower) == 1, follower + syscalls[idx] = follower[0] - def do_CheckAlarm(self, block, before): chain_item = None - alarm_object = block.arguments[0] - outgoing = block.get_outgoing_nodes(E.task_level) - if outgoing[0] == alarm_object.carried_syscall: - action_syscall, chain_item = outgoing + if syscalls[0] == alarm_object.carried_syscall: + action_syscall, chain_item = next_cont else: - assert outgoing[1] == alarm_object.carried_syscall - chain_item, action_syscall = outgoing + assert syscalls[1] == alarm_object.carried_syscall + chain_item, action_syscall = next_cont - ret = [before.copy()] - ret[0].set_continuation(block.subtask, chain_item) + ret = [(syscall, before.copy())] + ret[0][1].set_continuation(syscall.subtask, chain_item) if alarm_object.can_trigger(before): - ret.append(before.copy()) - ret[1].set_continuation(block.subtask, action_syscall) + ret.append( (syscall, before.copy()) ) + ret[1][1].set_continuation(syscall.subtask, action_syscall) + + # If we use the Application FSMs, we redo both system calls to + # elimiate the CheckAlarm syscall edges + if self.use_app_fsm: + for idx, (_, state) in enumerate(ret): + ret[idx] = (None, state) return ret - def do_Idle(self, block, before): + def do_Idle(self, cont, before, syscall): after = before.copy_if_needed() # EnsureComputationBlocks ensures that after the Idle() function # only one ABB can be located - cont = block.definite_after(E.task_level) - after.set_continuation(self.running_task.for_abb(block), - cont) - return [after] - - def do_computation(self, block, before): - next_blocks = block.get_outgoing_nodes(E.task_level) - ret = [before.copy() for _ in range(0, len(next_blocks))] - calling_task = self.running_task.for_abb(block) + next_cont = self.__next_continuation(cont, before, syscall) + after.set_continuation(cont.subtask, next_cont) + return [(syscall, after)] + + def do_computation(self, cont, before, syscall): + next_blocks = self.__next_continuations(cont, before, syscall) + ret = [(syscall, before.copy()) for _ in range(0, len(next_blocks))] + calling_task = cont.subtask for i in range(0, len(next_blocks)): - ret[i].set_continuation(calling_task, next_blocks[i]) + ret[i][1].set_continuation(calling_task, next_blocks[i]) return ret - def do_computation_with_callstack(self, block, before): - calling_task = self.running_task.for_abb(block) + def do_computation_with_callstack(self, cont, before, syscall): + calling_task = cont.subtask - if block.function.exit_abb == block: + if syscall.function.exit_abb == syscall: # Function return is done from calling stack after = before.copy_if_needed() next_abb = after.get_call_stack(calling_task).pop() after.set_continuation(calling_task, next_abb) # print "Return from %s -> %s" % (block, next_abb) - return [after] + return [(syscall, after)] else: - next_blocks = block.get_outgoing_nodes(E.task_level) - ret = before.copy_if_needed(len(next_blocks)) + next_blocks = self.__next_continuations(cont, before, syscall) + # Get enought return block copies + ret = [(syscall, x) for x in before.copy_if_needed(len(next_blocks))] for i in range(0, len(next_blocks)): next_abb = next_blocks[i] - after = ret[i] + after = ret[i][1] # If next abb is entry node, push the current abb if next_abb.function.entry_abb == next_abb: # CALL @@ -217,15 +248,31 @@ class SystemCallSemantic: return ret - def do_SystemCall(self, block, before, system_calls): - if block.syscall_type in system_calls: - after = system_calls[block.syscall_type](block, before) - return after + def do_SystemCall(self, cont, before, system_calls): + if self.use_app_fsm and isinstance(cont, ApplicationFSMIterator): + ret = [] + syscalls = cont.possible_systemcalls + #if not "Alarm" in str(cont): + # print(str(before).count("RDY"), cont, "->", syscalls) + for syscall in syscalls: + after = system_calls[syscall.syscall_type](cont, before, syscall) + ret.extend(after) + return ret else: - panic("BlockType %s is not supported yet" % block.syscall_type) + if cont.syscall_type in system_calls: + # Returns [(ABB, State)] + return system_calls[cont.syscall_type](cont, before, cont) + else: + panic("BlockType %s is not supported yet" % cont.syscall_type) + + def dynamic_priority(self, state, block): + subtask = block.subtask + if state.get_block_list(subtask) != 0: + return subtask.conf.static_priority + return block.dynamic_priority def find_possible_next_blocks(self, source, state): - current_running = self.running_task.for_abb(source) + current_running = source.subtask # If the current task is not preemptable, we can just continue # on the local task graph or on ISR blocks @@ -236,8 +283,10 @@ class SystemCallSemantic: if not current_running.conf.is_isr: for subtask in state.get_subtasks(): if subtask.conf.is_isr and state.is_maybe_ready(subtask): + isr_blocks = state.get_continuations(subtask) assert state.is_surely_ready(subtask) - isr_conts.append(subtask.entry_abb) + assert len(isr_blocks) == 1 + isr_conts.extend(isr_blocks) if isr_conts: return isr_conts else: @@ -252,36 +301,37 @@ class SystemCallSemantic: conts = state.get_continuations(subtask) assert len (conts) > 0, \ "Every surely running task must have one continuation point, %s has none: %s" % (subtask, state) - minimum_return_prio = min([x.dynamic_priority for x in conts]) - for B in conts: - possible_blocks.append([B, B.dynamic_priority <= minimum_return_prio]) + conts_prio = [(B, self.dynamic_priority(state, B)) for B in conts] + minimum_return_prio = min([prio for B, prio in conts_prio]) + for B, prio in conts_prio: + possible_blocks.append(( B, prio, prio <= minimum_return_prio)) elif state.is_maybe_ready(subtask): for B in state.get_continuations(subtask): - possible_blocks.append([B, False]) + prio = self.dynamic_priority(state, B) + possible_blocks.append((B, prio, False)) # Then we sort the continuing blocks after their dynamic priority possible_blocks = list(sorted(possible_blocks, - key = lambda x: x[0].dynamic_priority, + key = lambda x: x[1], # (block, prio, surely_ready) reverse = True)) ret = [] # Now we take all possible blocks until we find a block, that # belongs to a surely runnning block minimum_system_prio = 0 - for block, surely in possible_blocks: + for block, prio, surely in possible_blocks: if not surely: continue if surely: minimum_system_prio = max(minimum_system_prio, block.dynamic_priority) break - for block, surely in possible_blocks: - if minimum_system_prio <= block.dynamic_priority: + for block, prio, surely in possible_blocks: + if minimum_system_prio <= prio: ret.append(block) return ret - def schedule(self, source, state, set_state_on_edge): + def schedule_imprecise(self, source, state): possible_blocks = self.find_possible_next_blocks(source, state) - #print(source, [(x.dynamic_priority, x.path()) for x in possible_blocks], state) # The possible blocks are ordered with their dynamic priority. # [....., Block, ....] @@ -293,39 +343,39 @@ class SystemCallSemantic: state = None # Just a guard # Our target is surely running - copy_state.set_ready(target.function.subtask) + copy_state.set_ready(target.subtask) # The currently running subtask has no saved continuations - copy_state.set_continuations(target.function.subtask, []) + copy_state.set_continuations(target.subtask, []) # Idle subtask: reset to entry_abb, if we dispatch to # another subtask (user subtask idle = self.system_graph.idle_subtask - if target.function.subtask != idle and not target.function.subtask.conf.is_isr: - copy_state.set_continuation(idle, idle.entry_abb) + if target.subtask != idle and not target.subtask.conf.is_isr: + copy_state.set_continuation(idle, self.__entry_point(idle)) not_taken = set(possible_blocks[:i]) # We can wipe out all continuations that are not taken, if # a subtask has no possible continuations anymore, it is surely suspended for cont in not_taken: - subtask = cont.function.subtask + subtask = cont.subtask # For the own subtask we already know where we are - if subtask == target.function.subtask: + if subtask == target.subtask: continue copy_state.remove_continuation(subtask, cont) if len(copy_state.get_continuations(subtask)) == 0: copy_state.set_suspended(subtask) - copy_state.set_continuation(subtask, subtask.entry_abb) + copy_state.set_continuation(subtask, self.__entry_point(subtask)) # print subtask, " cannot be running in ", target copy_state.current_abb = target # If the target is not in the idle loop, we reset the idle # loop, since it always starts from the beginning. But # only if the target is not an ISR2 - if not target.function.subtask or \ - (target.function.subtask != self.system_graph.idle_subtask \ - and not target.function.subtask.conf.is_isr): + if not target.subtask or \ + (target.subtask != self.system_graph.idle_subtask \ + and not target.subtask.conf.is_isr): copy_state.set_continuation(self.system_graph.idle_subtask, - self.system_graph.idle_subtask.entry_abb) + self.__entry_point(self.system_graph.idle_subtask)) # If the new state will resume to a WaitEvent, we redo the # wait event to succeed to the next block. We do this only, if we resume from another subtask @@ -341,8 +391,42 @@ class SystemCallSemantic: # Mark the new state as frozen! copy_state.frozen = True - set_state_on_edge(source, target, copy_state) - - return - + yield (source, target, copy_state) + def schedule(self, source, state): + current_running = source.subtask + # Find continuation with highest priority + target = None + prio = 0 + for subtask in state.get_unordered_subtasks(): + if state.is_surely_ready(subtask): + cont = state.get_continuation(subtask) + cont_prio = self.dynamic_priority(state, cont) + if not target or cont_prio > prio: + prio = cont_prio + target = cont + else: + assert state.is_surely_suspended(subtask) or \ + state.is_surely_waiting(subtask) + # If the current task is not preemptable, we can just continue + # on the local task graph or on ISR blocks + if current_running and not current_running.conf.preemptable \ + and state.is_surely_ready(current_running): + task_cont = state.get_continuation(current_running) + # The non-preemptable task can only be preempted by an ISR + if not target.subtask.conf.is_isr: + target = task_cont + + # Dispatch! + copy_state = state.copy() + copy_state.current_abb = target + # Clear the block this. This indicates that non-preemptable + # tasks take the RES_SCHEDULER after being woken up again. + copy_state.clear_block_list(target.subtask) + # Reset the idle task + idle = self.system_graph.idle_subtask + if target.subtask != idle and not target.subtask.conf.is_isr: + copy_state.set_continuation(idle, self.__entry_point(idle)) + copy_state.set_continuation(target.subtask, None) + copy_state.frozen = True + yield (source, target, copy_state) diff --git a/generator/analysis/SystemState.py b/generator/analysis/SystemState.py index ff486af..526f04f 100644 --- a/generator/analysis/SystemState.py +++ b/generator/analysis/SystemState.py @@ -27,6 +27,7 @@ class SystemState(Node): self.continuations = [None] * size self.events_cleared = [0] * size self.events_set = [0] * size + self.events_waiting = [0] * size self.call_stack = [None] * size for i in range(0, size): @@ -99,6 +100,9 @@ class SystemState(Node): def is_surely_ready(self, subtask): return self.states[subtask.subtask_id] == self.READY + def is_surely_waiting(self, subtask): + return self.states[subtask.subtask_id] == self.WAITING + def is_maybe_ready(self, subtask): return self.READY & self.states[subtask.subtask_id] @@ -119,6 +123,9 @@ class SystemState(Node): return (self.events_cleared[subtask.subtask_id], self.events_set[subtask.subtask_id]) + def get_block_list(self, subtask): + return (self.events_waiting[subtask.subtask_id]) + def is_event_set(self, subtask, event): return (self.events_set[subtask.subtask_id] & event.event_mask) != 0 @@ -141,7 +148,7 @@ class SystemState(Node): def remove_continuation(self, subtask, abb): assert not self.frozen - assert abb in self.continuations[subtask.subtask_id] + assert abb in self.continuations[subtask.subtask_id], (abb, self.continuations[subtask.subtask_id]) self.continuations[subtask.subtask_id].discard(abb) def add_continuation(self, subtask, abb): diff --git a/generator/analysis/SystemStateFlow.py b/generator/analysis/SystemStateFlow.py index 81728bb..22563d1 100644 --- a/generator/analysis/SystemStateFlow.py +++ b/generator/analysis/SystemStateFlow.py @@ -86,8 +86,8 @@ class SystemStateFlow(Analysis): wrapped_isr = SSF_SporadicEvent(isr, self.system_call_semantic) self.sporadic_events.append(wrapped_isr) - def do_computation_with_sporadic_events(self, block, before): - after_states = self.system_call_semantic.do_computation(block, before) + def do_computation_with_sporadic_events(self, block, before, syscall): + after_states = self.system_call_semantic.do_computation(block, before, syscall) # Handle sporadic events events = 0 @@ -139,8 +139,10 @@ class SystemStateFlow(Analysis): S.Idle : scc.do_Idle}) # Schedule depending on the possible output state - for after in after_states: - self.system_call_semantic.schedule(block, after, self.set_state_on_edge) + for (sycall, after_state) in after_states: + edges = self.system_call_semantic.schedule_imprecise(block, after_state) + for (source, target, new_state) in edges: + self.set_state_on_edge(source, target, new_state) self.debug("}}}") @@ -159,7 +161,7 @@ class SystemStateFlow(Analysis): self.edge_states = {} # ABB -> SystemState - self.system_call_semantic = SystemCallSemantic(self.system_graph, self.running_task) + self.system_call_semantic = SystemCallSemantic(self.system_graph) self.install_sporadic_events() @@ -289,7 +291,7 @@ class SSF_SporadicEvent(SporadicEvent): def can_trigger(self, state): return self.wrapped_event.can_trigger(state) - def do_iret(self, block, before): + def do_iret(self, block, before, syscall): # When there is no further local abb node, we have reached the # end of the interrupt handler self.irq_exit_state.merge_with(before) @@ -318,8 +320,10 @@ class SSF_SporadicEvent(SporadicEvent): S.CheckAlarm : self.system_call_semantic.do_CheckAlarm, S.iret: self.do_iret}) # Schedule depending on the possible output states - for after in after_states: - self.system_call_semantic.schedule(block, after, self.set_state_on_edge) + for (syscall, after_state) in after_states: + edges = self.system_call_semantic.schedule_imprecise(block, after_state) + for (source, target, new_state) in edges: + self.set_state_on_edge(source, target, new_state) # This has to be done after the system call handling, since # new irq links could have been introduced @@ -368,7 +372,7 @@ class SSF_SporadicEvent(SporadicEvent): # the entry_abb ret_state.add_continuation(subtask, subtask.entry_abb) - return ret_state + return (None, ret_state) def fixup_before_states(self): for abb in self.wrapped_event.handler.abbs: diff --git a/generator/analysis/common.py b/generator/analysis/common.py index 0e6532a..68c783a 100644 --- a/generator/analysis/common.py +++ b/generator/analysis/common.py @@ -105,11 +105,11 @@ class Node(GraphObject): if edge.level in self.current_edge_filter] return self.outgoing_edges - def add_cfg_edge(self, target, level): + def add_cfg_edge(self, target, level, label=''): self.check_edge_filter(level) assert not target in self.get_outgoing_edges(level), \ "Cannot add edge of the same type twice" - edge = self.edge_factory(self, target, level) + edge = self.edge_factory(self, target, level, label=label) self.outgoing_edges.append(edge) target.incoming_edges.append(edge) diff --git a/generator/analysis/types.py b/generator/analysis/types.py index ed22f59..7753ed8 100644 --- a/generator/analysis/types.py +++ b/generator/analysis/types.py @@ -36,8 +36,8 @@ class ControlFlowEdge(Edge): that stay on the task level (aka. always on the same stack/same task context)""" - def __init__(self, source, target, level = E.task_level): - Edge.__init__(self, source, target, level, color = E.color(level)) + def __init__(self, source, target, level = E.task_level, label =''): + Edge.__init__(self, source, target, level, color = E.color(level), label='') @unique class SyscallType(IntEnum): @@ -48,7 +48,8 @@ class SyscallType(IntEnum): StartOS = 2 Idle = 3 CheckAlarm = 4 - iret = 5 + CheckIRQ = 5 + iret = 6 # real system calls kickoff = 19 diff --git a/generator/main.py b/generator/main.py index 736f19e..54af079 100755 --- a/generator/main.py +++ b/generator/main.py @@ -202,12 +202,12 @@ if __name__ == "__main__": syscall_rules = FullSystemCalls() elif conf.os.systemcalls == "fsm_pla": - assert conf.arch.self == "posix", "FSM Encoding is only supported for arch=posix" + pass_manager.get_pass("sse").use_app_fsm = True pass_manager.enqueue_analysis("LogicMinimizer") pass_manager.enqueue_analysis("fsm") syscall_rules = FSMSystemCalls(use_pla = True) elif conf.os.systemcalls == "fsm": - assert conf.arch.self == "posix", "FSM Encoding is only supported for arch=posix" + pass_manager.get_pass("sse").use_app_fsm = True pass_manager.enqueue_analysis("fsm") syscall_rules = FSMSystemCalls() else: diff --git a/generator/tools/__init__.py b/generator/tools/__init__.py index b4b3113..9fb66f7 100644 --- a/generator/tools/__init__.py +++ b/generator/tools/__init__.py @@ -53,9 +53,20 @@ def wrap_in_list(seq): class stack(list): def push(self, item): self.append(item) + def pull(self): + return self.pop() def isEmpty(self): return not self +class queue(list): + def push(self, item): + self.insert(0, item) + def pull(self): + return self.pop() + def isEmpty(self): + return not self + + def select_distinct(seq, field): ret = set() for item in seq: diff --git a/generator/transform/FiniteStateMachineBuilder.py b/generator/transform/FiniteStateMachineBuilder.py index cc55f76..7b6779d 100644 --- a/generator/transform/FiniteStateMachineBuilder.py +++ b/generator/transform/FiniteStateMachineBuilder.py @@ -1,5 +1,5 @@ from generator.analysis.common import * -from generator.analysis import Analysis, SavedStateTransition, S, E +from generator.analysis import Analysis, SavedStateTransition, S from generator.tools import pairwise from collections import namedtuple, defaultdict from datastructures.sage_finite_state_machine import Transducer, full_group_by, Automaton @@ -53,10 +53,20 @@ class FiniteStateMachineBuilder(Analysis, GraphObject): def graph_edges(self): ret = [] - for P in self.fsm.events: + fsm = self.fsm + #fsm.rename(events = lambda x: fsm.event_mapping[x], + # actions = lambda x: fsm.action_mapping[x]) + + + def subtask(state): + if state in fsm.state_mapping: + if fsm.state_mapping[state].current_subtask: + return fsm.state_mapping[state].current_subtask.name + return "XXX" + for P in fsm.events: for T in P.transitions: - ret.append(self.SimpleEdge(source = T.source, - target = T.target, + ret.append(self.SimpleEdge(source = "%s_%s" % (subtask(T.source), T.source), + target = "%s_%s" % (subtask(T.target), T.target), label = str(P.name) + "\\n| " + str(T.action))) return ret @@ -89,8 +99,34 @@ class FiniteStateMachineBuilder(Analysis, GraphObject): changed = True return ec + def do_from_app_fsm(self): + # Construct the Event/Transition Model + self.fsm = FiniteStateMachine() + + events = defaultdict(list) + for start_state in self.sse.states: + for next_state, label in start_state.get_outgoing_edges(SavedStateTransition): + initial_ec = next_state.current_subtask + if label.isA(S.CheckIRQ): + initial_ec = start_state.current_subtask + + events[label] += [Transition(start_state, next_state, initial_ec)] + for abb, transitions in events.items(): + event = Event(name = abb, transitions = transitions) + if abb.isA(S.StartOS): + assert len(transitions) == 1 + self.fsm.initial_state = transitions[0].source + + self.fsm.add_event(event) + + self.fsm.rename(states = True) + self.__minimize() + def do(self): self.sse = self.system_graph.get_pass("SymbolicSystemExecution") + if self.sse.use_app_fsm: + self.do_from_app_fsm() + return def isSyscall(state): return not state.current_abb.isA([S.computation, S.CheckAlarm]) @@ -112,7 +148,7 @@ class FiniteStateMachineBuilder(Analysis, GraphObject): # A system call block! if isSyscall(sse_state): syscall_states.add(state) - + # For each system call ret block, we find those states that # are equivalent to the return state remapped = set() @@ -159,6 +195,9 @@ class FiniteStateMachineBuilder(Analysis, GraphObject): self.fsm.add_event(event) self.fsm.state_mapping = map_to_SystemState + self.__minimize() + + def __minimize(self): def count(iter): return sum(1 for _ in iter) @@ -172,7 +211,6 @@ class FiniteStateMachineBuilder(Analysis, GraphObject): len(self.fsm.states), count(self.fsm.transitions)) - class FiniteStateMachineMinimizer: @staticmethod def __equivalence_classes(fsm): @@ -196,6 +234,7 @@ class FiniteStateMachineMinimizer: classes_current = [equivalence_class for (key,equivalence_class) in states_grouped] + while len(classes_current) != len(classes_previous): class_of = {} followup_classes_of = {} @@ -287,7 +326,7 @@ class FiniteStateMachineMinimizer: to_state = t[1], word_in = [t[2]], word_out = [t[3]]) - return new + return new, state_mapping @staticmethod def minimize(old_fsm): @@ -296,12 +335,11 @@ class FiniteStateMachineMinimizer: """ old_fsm.rename(events = True, actions = True) # For Debugging: self.rename(events = str, actions = str) - sage = old_fsm.to_sage_fsm() # We use our own simpliciation algorithm here ec = FiniteStateMachineMinimizer.__equivalence_classes(sage) - new_fsm = FiniteStateMachineMinimizer.__quotient(sage, ec) + new_fsm, state_mapping = FiniteStateMachineMinimizer.__quotient(sage, ec) # The resulting fsm MUST be deterministic. assert new_fsm.is_deterministic() -- GitLab