From 56c0064963298b3404f5483c5522484cd100d92f Mon Sep 17 00:00:00 2001 From: Christian Dietrich <christian.dietrich@informatik.uni-erlangen.de> Date: Wed, 22 Jan 2014 15:00:50 +0100 Subject: [PATCH] analysis/RunningTask: refactor testcases RunningTaskToolbox is a class, that provides testing functions for the global flow graph. This toolbox is now used throughout all verify scripts. Change-Id: If149cf41c0c5b8ff7cb9e6506f3a1829e96a6e26 --- app/bcc1/alarm1/verify_a.py | 29 +++++++--------- app/bcc1/alarm1/verify_b.py | 27 +++++++-------- app/bcc1/alarm1/verify_c.py | 26 ++++++--------- app/bcc1/alarm1/verify_d.py | 28 +++++++--------- app/bcc1/alarm1/verify_e.py | 30 ++++++++--------- app/bcc1/complex1/verify_a.py | 28 +++++++--------- app/bcc1/complex1/verify_b.py | 26 ++++++--------- app/bcc1/complex1/verify_c.py | 34 ++++++++----------- app/bcc1/isr2/verify_a.py | 29 +++++++--------- app/bcc1/isr2/verify_b.py | 31 +++++++---------- app/bcc1/isr2/verify_c.py | 36 +++++++++----------- app/bcc1/isr2/verify_d.py | 16 ++++----- app/bcc1/task1/verify_a.py | 41 ++++++++++------------- app/bcc1/task1/verify_b.py | 24 ++++++-------- app/bcc1/task1/verify_c.py | 22 +++++-------- app/bcc1/task1/verify_d.py | 26 +++++++-------- app/bcc1/task1/verify_e.py | 23 ++++++------- app/bcc1/task1/verify_f.py | 22 +++++-------- app/bcc1/task1/verify_g.py | 24 ++++++-------- app/bcc1/task2/verify_a.py | 28 ++++++++-------- app/bcc1/task2/verify_b.py | 24 +++++++------- generator/graph/RunningTask.py | 6 ++-- generator/graph/common.py | 32 ------------------ generator/graph/verifier_tools.py | 55 +++++++++++++++++++++++++++++++ toolchain/app.cmake | 2 +- 25 files changed, 299 insertions(+), 370 deletions(-) create mode 100644 generator/graph/verifier_tools.py diff --git a/app/bcc1/alarm1/verify_a.py b/app/bcc1/alarm1/verify_a.py index 36731d3..523af7e 100644 --- a/app/bcc1/alarm1/verify_a.py +++ b/app/bcc1/alarm1/verify_a.py @@ -1,31 +1,26 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) # H1 and H3 are not activated - syscalls.update(set(H1.get_syscalls())) - syscalls.update(set(H3.get_syscalls())) + t.mark_syscalls_in_function(H1) + t.mark_syscalls_in_function(H3) - test(StartOS, "StartOS", [], # => - [Idle]) + t.reachability(StartOS, "StartOS", [], # => + [Idle]) - activated_test(analysis, [Idle], # => - H2) + t.activate([Idle], # => + H2) - test(H2, "TerminateTask", [], # => - [Idle]) + t.reachability(H2, "TerminateTask", [], # => + [Idle]) - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \ - %(set(analysis.system.get_syscalls()) - syscalls) - + t.promise_all_syscalls_checked() diff --git a/app/bcc1/alarm1/verify_b.py b/app/bcc1/alarm1/verify_b.py index 121a361..0716ee7 100644 --- a/app/bcc1/alarm1/verify_b.py +++ b/app/bcc1/alarm1/verify_b.py @@ -1,36 +1,31 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) # H3 are not activated - syscalls.update(set(H3.get_syscalls())) + t.mark_syscalls_in_function(H3) - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Idle]) - activated_test(analysis, [Idle], # => - H2) + t.activate([Idle], # => + H2) - test(H2, "ActivateTask", [H1], # => + t.reachability(H2, "ActivateTask", [H1], # => [H1]) - test(H2, "TerminateTask", [], # => + t.reachability(H2, "TerminateTask", [], # => [Idle]) - test(H1, "TerminateTask", [], # => + t.reachability(H1, "TerminateTask", [], # => [H2]) - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \ - %(set(analysis.system.get_syscalls()) - syscalls) - + t.promise_all_syscalls_checked() diff --git a/app/bcc1/alarm1/verify_c.py b/app/bcc1/alarm1/verify_c.py index b0d4de9..6f5dc42 100644 --- a/app/bcc1/alarm1/verify_c.py +++ b/app/bcc1/alarm1/verify_c.py @@ -1,33 +1,27 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) - + t = RunningTaskToolbox(analysis) # H3 are not activated - syscalls.update(set(H3.get_syscalls())) + t.mark_syscalls_in_function(H3) - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Idle]) - activated_test(analysis, [Idle, H1], # => - H2) + t.activate([Idle, H1], # => + H2) - test(H2, "ChainTask", [H1], # => + t.reachability(H2, "ChainTask", [H1], # => [H1]) - test(H1, "TerminateTask", [], # => + t.reachability(H1, "TerminateTask", [], # => [H2, Idle]) - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \ - %(set(analysis.system.get_syscalls()) - syscalls) - + t.promise_all_syscalls_checked() diff --git a/app/bcc1/alarm1/verify_d.py b/app/bcc1/alarm1/verify_d.py index 31d0c85..ca826c1 100644 --- a/app/bcc1/alarm1/verify_d.py +++ b/app/bcc1/alarm1/verify_d.py @@ -1,36 +1,32 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) - test(StartOS, "StartOS", [], # => + + t.reachability(StartOS, "StartOS", [], # => [Idle]) - activated_test(analysis, [Idle, H1, H3], # => - H2) + t.activate([Idle, H1, H3], # => + H2) - test(H1, "ActivateTask", [H3], # => + t.reachability(H1, "ActivateTask", [H3], # => [H1]) - test(H2, "ChainTask", [H1], # => + t.reachability(H2, "ChainTask", [H1], # => [H1]) - test(H1, "TerminateTask", [], # => + t.reachability(H1, "TerminateTask", [], # => [H2, H3]) - test(H3, "TerminateTask", [], # => + t.reachability(H3, "TerminateTask", [], # => [Idle]) - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \ - %(set(analysis.system.get_syscalls()) - syscalls) - + t.promise_all_syscalls_checked() diff --git a/app/bcc1/alarm1/verify_e.py b/app/bcc1/alarm1/verify_e.py index 98f50c0..d36f624 100644 --- a/app/bcc1/alarm1/verify_e.py +++ b/app/bcc1/alarm1/verify_e.py @@ -1,42 +1,38 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Idle]) - activated_test(analysis, [Idle, H1, H3], # => - H2) + t.activate([Idle, H1, H3], # => + H2) - test(H1, "TerminateTask", [], # => + t.reachability(H1, "TerminateTask", [], # => [H2, H3]) - test(H2, "ActivateTask", [H3], # => + t.reachability(H2, "ActivateTask", [H3], # => [H2]) - test(H2, "TerminateTask", [], # => + t.reachability(H2, "TerminateTask", [], # => [H3, Idle]) - test(H1, "TerminateTask", [], # => + t.reachability(H1, "TerminateTask", [], # => [H2, H3]) - test(H3, "ActivateTask", [H1], # => + t.reachability(H3, "ActivateTask", [H1], # => [H1]) - test(H3, "TerminateTask", [], # => + t.reachability(H3, "TerminateTask", [], # => [Idle]) - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \ - %(set(analysis.system.get_syscalls()) - syscalls) + t.promise_all_syscalls_checked() diff --git a/app/bcc1/complex1/verify_a.py b/app/bcc1/complex1/verify_a.py index 515eb31..efbfbdb 100644 --- a/app/bcc1/complex1/verify_a.py +++ b/app/bcc1/complex1/verify_a.py @@ -1,35 +1,29 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS, ISR1) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"]) - syscalls = set() - syscalls.update(set(H3.get_syscalls())) - syscalls.update(set(ISR1.get_syscalls())) + t = RunningTaskToolbox(analysis) + t.mark_syscalls_in_function(H3) + t.mark_syscalls_in_function(ISR1) - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) - return abb - - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Idle]) - test(H2, "TerminateTask", [], # => + t.reachability(H2, "TerminateTask", [], # => [Idle]) - test(H1, "TerminateTask", [], # => + t.reachability(H1, "TerminateTask", [], # => [H2, # Activated by Alarm Idle, ]) - activated_test(analysis, [Idle, H1], # => - H2) + t.activate([Idle, H1], # => + H2) - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \ - %(analysis.system.get_syscalls(), syscalls) + t.promise_all_syscalls_checked() diff --git a/app/bcc1/complex1/verify_b.py b/app/bcc1/complex1/verify_b.py index 5b7047a..2e9847b 100644 --- a/app/bcc1/complex1/verify_b.py +++ b/app/bcc1/complex1/verify_b.py @@ -1,36 +1,30 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS, ISR1) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"]) - syscalls = set() - syscalls.update(set(H1.get_syscalls())) - syscalls.update(set(ISR1.get_syscalls())) + t = RunningTaskToolbox(analysis) + t.mark_syscalls_in_function(H1) + t.mark_syscalls_in_function(ISR1) - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) - return abb - - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Idle]) - test(H2, "TerminateTask", [], # => + t.reachability(H2, "TerminateTask", [], # => [Idle, H3]) # H3 could be activated by ISR1 - test(H3, "TerminateTask", [], # => + t.reachability(H3, "TerminateTask", [], # => [Idle]) - activated_test(analysis, [Idle, H3], # => + t.activate([Idle, H3], # => H2) # H2.entry can be reached by H3.entry, when alarm was running assert H2.entry_abb in H3.entry_abb.get_outgoing_nodes('global') - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \ - %(analysis.system.get_syscalls(), syscalls) + t.promise_all_syscalls_checked() diff --git a/app/bcc1/complex1/verify_c.py b/app/bcc1/complex1/verify_c.py index c8521f5..ccb5a5f 100644 --- a/app/bcc1/complex1/verify_c.py +++ b/app/bcc1/complex1/verify_c.py @@ -1,46 +1,40 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS, ISR1) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"]) - syscalls = set() - syscalls.update(set(H1.get_syscalls())) - syscalls.update(set(ISR1.get_syscalls())) + t = RunningTaskToolbox(analysis) + t.mark_syscalls_in_function(H1) + t.mark_syscalls_in_function(ISR1) - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) - return abb - - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Idle]) - test(H2, "TerminateTask", [], # => + t.reachability(H2, "TerminateTask", [], # => [Idle, H3]) # H3 could be activated by ISR1 - test(H3, "ChainTask", [H1], # => + t.reachability(H3, "ChainTask", [H1], # => [H1]) - test(H1, "TerminateTask", [], # => + t.reachability(H1, "TerminateTask", [], # => [H2, # Could be activated by Alarm H3, # Could be activated by ISR Idle, # Nothing could have happended ]) - activated_test(analysis, [Idle, H3, H1], # => - H2) + t.activate([Idle, H3, H1], # => + H2) - activated_test(analysis, [H3], # => - H1) + t.activate([H3], # => + H1) # H2.entry can be reached by H3.entry, when alarm was running assert H2.entry_abb in H3.entry_abb.get_outgoing_nodes('global') - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \ - %(analysis.system.get_syscalls(), syscalls) + t.promise_all_syscalls_checked() diff --git a/app/bcc1/isr2/verify_a.py b/app/bcc1/isr2/verify_a.py index 3aacaa8..517c166 100644 --- a/app/bcc1/isr2/verify_a.py +++ b/app/bcc1/isr2/verify_a.py @@ -1,33 +1,26 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS, ISR1) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"]) - syscalls = set() - syscalls.update(set(H1.get_syscalls())) - syscalls.update(set(H3.get_syscalls())) - syscalls.update(set(ISR1.get_syscalls())) + t = RunningTaskToolbox(analysis) + t.mark_syscalls_in_function(H1) + t.mark_syscalls_in_function(H3) + t.mark_syscalls_in_function(ISR1) - - - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) - - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Idle]) - test(H2, "TerminateTask", [], # => + t.reachability(H2, "TerminateTask", [], # => [Idle]) - activated_test(analysis, [Idle], # => - H2) + t.activate([Idle], # => + H2) # Idle handler is never left - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \ - %(analysis.system.get_syscalls(), syscalls) + t.promise_all_syscalls_checked() diff --git a/app/bcc1/isr2/verify_b.py b/app/bcc1/isr2/verify_b.py index 15f9d32..015326d 100644 --- a/app/bcc1/isr2/verify_b.py +++ b/app/bcc1/isr2/verify_b.py @@ -1,39 +1,32 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS, ISR1) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"]) - syscalls = set() - syscalls.update(set(H1.get_syscalls())) - syscalls.update(set(ISR1.get_syscalls())) + t = RunningTaskToolbox(analysis) + t.mark_syscalls_in_function(H1) + t.mark_syscalls_in_function(ISR1) - - - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) - - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Idle]) - test(H2, "ActivateTask", [H3], # => + t.reachability(H2, "ActivateTask", [H3], # => [H2]) - test(H2, "TerminateTask", [], # => + t.reachability(H2, "TerminateTask", [], # => [H3]) - test(H3, "TerminateTask", [], # => + t.reachability(H3, "TerminateTask", [], # => [Idle]) - activated_test(analysis, [Idle, H3], # => - H2) + t.activate([Idle, H3], # => + H2) # Idle handler is never left - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \ - %(set(analysis.system.get_syscalls()) - syscalls) + t.promise_all_syscalls_checked() diff --git a/app/bcc1/isr2/verify_c.py b/app/bcc1/isr2/verify_c.py index 94cef5d..21f19e6 100644 --- a/app/bcc1/isr2/verify_c.py +++ b/app/bcc1/isr2/verify_c.py @@ -1,49 +1,45 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS, ISR1) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"]) - syscalls = set() - - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) - return abb + t = RunningTaskToolbox(analysis) # In H2: - AT3 = test(H2, "ActivateTask", [H3], # => - [H2]) + AT3 = t.reachability(H2, "ActivateTask", [H3], # => + [H2]) state_before_AT3 = analysis.for_abb(AT3) - state_after_AT3 = analysis.for_abb(AT3.get_outgoing_nodes('global')[0]) + state_after_AT3 = analysis.for_abb(AT3.definite_after('local')) # Could be entered by H3 or Idle loop assert state_before_AT3.is_unsure_ready_state(H3) assert state_after_AT3.is_surely_ready(H3) ## Before ActivateTask(H1) the state of H3 is known - AT1 = test(H2, "ActivateTask", [H1], # => - [H1]) + AT1 = t.reachability(H2, "ActivateTask", [H1], # => + [H1]) state_before_AT1 = analysis.for_abb(AT1) assert state_before_AT1.is_surely_ready(H3) - TT3 = test(H2, "TerminateTask", [], # => - [H3]) + TT3 = t.reachability(H2, "TerminateTask", [], # => + [H3]) returned_nodes = TT3.get_outgoing_nodes('global') + assert len(returned_nodes) == 2 # When H3 was not preempted, then we start in the entry node assert H3.entry_abb in returned_nodes # When H3 was interrupted by ISR1, then it was preempted, and # should continue after the computation block assert H3.entry_abb.definite_after('local') in returned_nodes - test(StartOS, "StartOS", [], # => - [Idle]) + t.reachability(StartOS, "StartOS", [], # => + [Idle]) - activated_test(analysis, [Idle, H3], # => - H2) + t.activate([Idle, H3], # => + H2) # Idle handler is never left - test(Idle, "Idle", [], # => - [Idle]) + t.reachability(Idle, "Idle", [], # => + [Idle]) diff --git a/app/bcc1/isr2/verify_d.py b/app/bcc1/isr2/verify_d.py index 560f93a..7b3fc72 100644 --- a/app/bcc1/isr2/verify_d.py +++ b/app/bcc1/isr2/verify_d.py @@ -1,20 +1,16 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (H1, H2, H3, Idle, StartOS, ISR1) = \ get_functions(analysis.system, ["H1", "H2", "H3", "Idle", "StartOS", "ISR1"]) - syscalls = set() + t = RunningTaskToolbox(analysis) - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) - - test(H1, "TerminateTask", [], # => - [H3, # If interrupt was triggered - Idle, # If Interrupt wasn't triggered - ]) + t.reachability(H1, "TerminateTask", [], # => + [H3, # If interrupt was triggered + Idle, # If Interrupt wasn't triggered + ]) isr_entry_state = analysis.for_abb(ISR1.entry_abb) for st in (H1, H2, H3): diff --git a/app/bcc1/task1/verify_a.py b/app/bcc1/task1/verify_a.py index a77cb42..b745407 100644 --- a/app/bcc1/task1/verify_a.py +++ b/app/bcc1/task1/verify_a.py @@ -1,43 +1,38 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (Handler11, Handler12, Handler13, Idle, StartOS) = \ - get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"]) + get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) # Handler11 has higher priority than Handler12 - test(StartOS, "StartOS", [], # => - [Handler11]) + t.reachability(StartOS, "StartOS", [], # => + [Handler11]) # Handler11 has higher priority than Handler12 - test(Handler11, "ActivateTask", [Handler12], # => - [Handler11]) + t.reachability(Handler11, "ActivateTask", [Handler12], # => + [Handler11]) # Handler13 is directly started - test(Handler11, "ActivateTask", [Handler13], # => - [Handler13]) + t.reachability(Handler11, "ActivateTask", [Handler13], # => + [Handler13]) # Handler12 is always activated afterwards - test(Handler13, "TerminateTask", [], # => - [Handler11]) + t.reachability(Handler13, "TerminateTask", [], # => + [Handler11]) # Handler12 is always activated afterwards - test(Handler11, "TerminateTask", [], # => - [Handler12]) + t.reachability(Handler11, "TerminateTask", [], # => + [Handler12]) # Handler12 is always activated afterwards - test(Handler12, "TerminateTask", [], # => - [Idle]) + t.reachability(Handler12, "TerminateTask", [], # => + [Idle]) # Idle handler is never left - test(Idle, "Idle", [], # => - [Idle]) - - assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \ - %(set(analysis.system.get_syscalls()) - syscalls) + t.reachability(Idle, "Idle", [], # => + [Idle]) + t.promise_all_syscalls_checked() diff --git a/app/bcc1/task1/verify_b.py b/app/bcc1/task1/verify_b.py index 0c6f2ea..181c42e 100644 --- a/app/bcc1/task1/verify_b.py +++ b/app/bcc1/task1/verify_b.py @@ -1,4 +1,4 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_CurrentRunningSubtask(analysis): (Handler11, bar) = \ @@ -22,39 +22,35 @@ def after_RunningTaskAnalysis(analysis): (Handler11, Handler12, Handler13, bar, Idle, StartOS) = \ get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "bar", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) # Handler11 has higher priority than Handler12 - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Handler11]) # Handler11 has higher priority than Handler12 - test(Handler11, "ActivateTask", [Handler12], # => + t.reachability(Handler11, "ActivateTask", [Handler12], # => [Handler11]) # Handler13 is directly started - test(Handler11, "ChainTask", [Handler13], # => + t.reachability(Handler11, "ChainTask", [Handler13], # => [Handler13]) # bar is called by Handler11 - test(bar, "ActivateTask", [Handler12], # => + t.reachability(bar, "ActivateTask", [Handler12], # => [Handler11]) # Handler 13 does always lead to the activated handler 12 - test(Handler13, "TerminateTask", [], # => + t.reachability(Handler13, "TerminateTask", [], # => [Handler12]) # Handler12 is always activated afterwards - test(Handler12, "TerminateTask", [], # => + t.reachability(Handler12, "TerminateTask", [], # => [Idle]) # Idle handler is never left - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - # All system calls were checked - assert set(analysis.system.get_syscalls()) == syscalls + t.promise_all_syscalls_checked() diff --git a/app/bcc1/task1/verify_c.py b/app/bcc1/task1/verify_c.py index 208ce6f..85763c4 100644 --- a/app/bcc1/task1/verify_c.py +++ b/app/bcc1/task1/verify_c.py @@ -1,4 +1,4 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_CurrentRunningSubtask(analysis): (Handler11, bar) = \ @@ -22,35 +22,31 @@ def after_RunningTaskAnalysis(analysis): (Handler11, Handler12, Handler13, bar, Idle, StartOS) = \ get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "bar", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) - + t = RunningTaskToolbox(analysis) # Handler11 has higher priority than Handler12 - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Handler11]) # Handler13 is directly started - test(Handler11, "ChainTask", [Handler13], # => + t.reachability(Handler11, "ChainTask", [Handler13], # => [Handler13]) # bar is called by Handler11 - test(bar, "ActivateTask", [Handler12], # => + t.reachability(bar, "ActivateTask", [Handler12], # => [Handler11]) # Handler 13 does always lead to the activated handler 12 - test(Handler13, "TerminateTask", [], # => + t.reachability(Handler13, "TerminateTask", [], # => [Handler12, Idle]) # Handler12 is always activated afterwards - test(Handler12, "TerminateTask", [], # => + t.reachability(Handler12, "TerminateTask", [], # => [Idle]) # Idle handler is never left - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls + t.promise_all_syscalls_checked() diff --git a/app/bcc1/task1/verify_d.py b/app/bcc1/task1/verify_d.py index 47c3e74..086b688 100644 --- a/app/bcc1/task1/verify_d.py +++ b/app/bcc1/task1/verify_d.py @@ -1,4 +1,4 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_CurrentRunningSubtask(analysis): (Handler11, bar) = \ @@ -22,35 +22,31 @@ def after_RunningTaskAnalysis(analysis): (Handler11, Handler12, Handler13, bar, Idle, StartOS) = \ get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "bar", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) - - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Handler11]) - test(Handler11, "ActivateTask", [Handler12], # => + t.reachability(Handler11, "ActivateTask", [Handler12], # => [Handler11]) - test(bar, "ActivateTask", [Handler13], # => + t.reachability(bar, "ActivateTask", [Handler13], # => [Handler13]) - test(Handler11, "ActivateTask", [Handler13], # => + t.reachability(Handler11, "ActivateTask", [Handler13], # => [Handler13]) - test(Handler13, "TerminateTask", [], # => + t.reachability(Handler13, "TerminateTask", [], # => [Handler11]) - test(Handler11, "TerminateTask", [], # => + t.reachability(Handler11, "TerminateTask", [], # => [Handler12, Idle]) - test(Handler12, "TerminateTask", [], # => + t.reachability(Handler12, "TerminateTask", [], # => [Idle]) # Idle handler is never left - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls + t.promise_all_syscalls_checked() diff --git a/app/bcc1/task1/verify_e.py b/app/bcc1/task1/verify_e.py index 4f516ce..e7fa842 100644 --- a/app/bcc1/task1/verify_e.py +++ b/app/bcc1/task1/verify_e.py @@ -1,36 +1,33 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (Handler11, Handler12, Handler13, Idle, StartOS) = \ get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Handler11]) - test(Handler13, "ActivateTask", [Handler12], # => + t.reachability(Handler13, "ActivateTask", [Handler12], # => [Handler13]) - test(Handler11, "ActivateTask", [Handler13], # => + t.reachability(Handler11, "ActivateTask", [Handler13], # => [Handler13]) - test(Handler13, "TerminateTask", [], # => + t.reachability(Handler13, "TerminateTask", [], # => [Handler11]) # Handler13 did non nessecary run! - test(Handler11, "TerminateTask", [], # => + t.reachability(Handler11, "TerminateTask", [], # => [Handler12, Idle]) - test(Handler12, "TerminateTask", [], # => + t.reachability(Handler12, "TerminateTask", [], # => [Idle]) # Idle handler is never left - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => [Idle]) - assert set(analysis.system.get_syscalls()) == syscalls + t.promise_all_syscalls_checked() diff --git a/app/bcc1/task1/verify_f.py b/app/bcc1/task1/verify_f.py index 7e64e39..992da4c 100644 --- a/app/bcc1/task1/verify_f.py +++ b/app/bcc1/task1/verify_f.py @@ -1,33 +1,29 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (Handler11, Handler12, Handler13, Idle, StartOS) = \ get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Handler11]) - test(Handler11, "ChainTask", [Handler13], # => + t.reachability(Handler11, "ChainTask", [Handler13], # => [Handler13]) - test(Handler13, "ActivateTask", [Handler12], # => + t.reachability(Handler13, "ActivateTask", [Handler12], # => [Handler13]) - test(Handler13, "TerminateTask", [], # => + t.reachability(Handler13, "TerminateTask", [], # => [Handler12]) - test(Handler12, "ChainTask", [Handler11], # => + t.reachability(Handler12, "ChainTask", [Handler11], # => [Handler11]) # Idle handler is never left - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => []) - assert set(analysis.system.get_syscalls()) == syscalls, "%s != %s" \ - %(analysis.system.get_syscalls(), syscalls) + t.promise_all_syscalls_checked() diff --git a/app/bcc1/task1/verify_g.py b/app/bcc1/task1/verify_g.py index 18632c2..e9fb054 100644 --- a/app/bcc1/task1/verify_g.py +++ b/app/bcc1/task1/verify_g.py @@ -1,36 +1,32 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (Handler11, Handler12, Handler13, Idle, StartOS, bar) = \ get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS", "bar"]) - syscalls = set() - def test(func, syscall, args, expected_subtasks): - abb = reachability_test(analysis, func, syscall, args, expected_subtasks) - syscalls.add(abb) + t = RunningTaskToolbox(analysis) - test(StartOS, "StartOS", [], # => + t.reachability(StartOS, "StartOS", [], # => [Handler11]) - test(Handler11, "ChainTask", [Handler13], # => + t.reachability(Handler11, "ChainTask", [Handler13], # => [Handler13]) - test(Handler13, "ActivateTask", [Handler12], # => + t.reachability(Handler13, "ActivateTask", [Handler12], # => [Handler13]) - test(Handler13, "TerminateTask", [], # => + t.reachability(Handler13, "TerminateTask", [], # => [Handler12, Handler11]) - test(Handler12, "ChainTask", [Handler11], # => + t.reachability(Handler12, "ChainTask", [Handler11], # => [Handler11]) - test(bar, "ActivateTask", [Handler13], # => + t.reachability(bar, "ActivateTask", [Handler13], # => [Handler13]) # Idle handler is never left - test(Idle, "Idle", [], # => + t.reachability(Idle, "Idle", [], # => []) - assert set(analysis.system.get_syscalls()) == syscalls, "missing %s" \ - %(set(analysis.system.get_syscalls()) - syscalls) + t.promise_all_syscalls_checked() diff --git a/app/bcc1/task2/verify_a.py b/app/bcc1/task2/verify_a.py index 34e7a75..06a5e97 100644 --- a/app/bcc1/task2/verify_a.py +++ b/app/bcc1/task2/verify_a.py @@ -1,48 +1,46 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (Handler11, Handler12, Handler13, Idle, StartOS) = \ get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"]) - def reachability(function, syscall, arguments, reaching_subtasks): - syscall = analysis.system.find_syscall(function, syscall, arguments) - assert syscall - reachable_tasks = analysis.reachable_subtasks_from_abb(syscall) - assert(reachable_tasks == set(reachable_tasks)) + t = RunningTaskToolbox(analysis) # Handler11 has higher priority than Handler12 - reachability(StartOS, "StartOS", [], + t.reachability(StartOS, "StartOS", [], # => [Handler11]) # Handler11 has higher priority than Handler12 - reachability(Handler11, "ActivateTask", [Handler12], + t.reachability(Handler11, "ActivateTask", [Handler12], # => [Handler11]) # Handler11 is preemptable - reachability(Handler11, "ActivateTask", [Handler13], + t.reachability(Handler11, "ActivateTask", [Handler13], # => [Handler11]) # Handler12 is always activated afterwards - reachability(Handler11, "TerminateTask", [], + t.reachability(Handler11, "TerminateTask", [], # => [Handler13]) # Handler12 is always activated afterwards - reachability(Handler13, "TerminateTask", [], + t.reachability(Handler13, "TerminateTask", [], # => [Handler12]) # Handler12 is always activated afterwards - reachability(Handler12, "TerminateTask", [], + t.reachability(Handler12, "TerminateTask", [], # => [Idle]) # Idle handler is never left - reachability(Idle, "Idle", [], - # => - []) + t.reachability(Idle, "Idle", [], + # => + [Idle]) + + t.promise_all_syscalls_checked() diff --git a/app/bcc1/task2/verify_b.py b/app/bcc1/task2/verify_b.py index 3dd8019..686a264 100644 --- a/app/bcc1/task2/verify_b.py +++ b/app/bcc1/task2/verify_b.py @@ -1,28 +1,24 @@ -from generator.graph.common import * +from generator.graph.verifier_tools import * def after_RunningTaskAnalysis(analysis): # Find all three systemcall handlers (Handler11, Handler12, Handler13, Idle, StartOS) = \ get_functions(analysis.system, ["Handler11", "Handler12", "Handler13", "Idle", "StartOS"]) - def reachability(function, syscall, arguments, reaching_subtasks): - syscall = analysis.system.find_syscall(function, syscall, arguments) - assert syscall - reachable_tasks = analysis.reachable_subtasks_from_abb(syscall) - assert(reachable_tasks == set(reachable_tasks)) + t = RunningTaskToolbox(analysis) # Handler11 has higher priority than Handler12 - reachability(StartOS, "StartOS", [], + t.reachability(StartOS, "StartOS", [], # => [Handler11]) # Handler11 has higher priority than Handler12 - reachability(Handler11, "ActivateTask", [Handler12], + t.reachability(Handler11, "ActivateTask", [Handler12], # => [Handler11]) # Handler11 is preemptable - reachability(Handler11, "ActivateTask", [Handler13], + t.reachability(Handler11, "ActivateTask", [Handler13], # => [Handler11]) @@ -32,19 +28,21 @@ def after_RunningTaskAnalysis(analysis): for x in syscalls: tasks = set(analysis.reachable_subtasks_from_abb(x)) assert tasks == set([Handler12]) or tasks == set([Handler13]) + t.mark_syscall(x) # Handler12 is always activated afterwards - reachability(Handler13, "TerminateTask", [], + t.reachability(Handler13, "TerminateTask", [], # => [Handler12]) # Handler12 is always activated afterwards - reachability(Handler12, "TerminateTask", [], + t.reachability(Handler12, "TerminateTask", [], # => [Idle]) # Idle handler is never left - reachability(Idle, "Idle", [], + t.reachability(Idle, "Idle", [], # => - []) + [Idle]) + t.promise_all_syscalls_checked() diff --git a/generator/graph/RunningTask.py b/generator/graph/RunningTask.py index f0103b3..a87a770 100644 --- a/generator/graph/RunningTask.py +++ b/generator/graph/RunningTask.py @@ -450,12 +450,14 @@ class RunningTaskAnalysis(Analysis): subtasks.add(st) return subtasks - def activated_by(self, subtask): + def activating_subtasks(self, subtask): subtasks = set() + abbs = set() for reaching in subtask.entry_abb.get_incoming_nodes('global'): st = self.running_task.for_abb(reaching) subtasks.add(st) - return subtasks + abbs.add(reaching) + return subtasks, abbs def for_abb(self, abb): return self.before_abb_states[abb] diff --git a/generator/graph/common.py b/generator/graph/common.py index ad9c627..fea23dd 100644 --- a/generator/graph/common.py +++ b/generator/graph/common.py @@ -144,38 +144,6 @@ class FixpointIteraton: def is_local_edge(edge): return edge.is_local() -def get_functions(system, names): - """A helper for verify scripts to find quickly a set of subtask handlers""" - ret = [] - for x in names: - for name, func in system.functions.items(): - if x == name or \ - "OSEKOS_TASK_" + x == name or \ - "OSEKOS_ISR_" + x == name: - ret.append(func) - return tuple(ret) - -def syscall_test(analysis, function, syscall_name, arguments): - """Tests wheter a syscall exists and returns it""" - syscall = analysis.system.find_syscall(function, syscall_name, arguments) - assert syscall, "%s:%s(%s) not found" %(function.function_name, syscall_name, arguments) - return syscall - - -def reachability_test(analysis, function, syscall_name, arguments, possible_subtasks): - syscall = analysis.system.find_syscall(function, syscall_name, arguments) - assert syscall, "%s:%s(%s) not found" %(function.function_name, syscall_name, arguments) - reachable_subtasks = analysis.reachable_subtasks_from_abb(syscall) - assert(set(reachable_subtasks) == set(possible_subtasks)), "%s:%s(%s)::: %s != %s" %( - function.function_name, syscall_name, arguments, list(possible_subtasks), list(reachable_subtasks)) - - return syscall - -def activated_test(analysis, possible_subtasks, function): - reachable_subtasks = analysis.activated_by(function) - assert(set(reachable_subtasks) == set(possible_subtasks)), "SetReady(%s):: %s != %s" %( - function.function_name, list(possible_subtasks), list(reachable_subtasks)) - # Hook for coloured tracebacks on the console :-) def myexcepthook(type, value, tb): diff --git a/generator/graph/verifier_tools.py b/generator/graph/verifier_tools.py new file mode 100644 index 0000000..7c44687 --- /dev/null +++ b/generator/graph/verifier_tools.py @@ -0,0 +1,55 @@ +def get_functions(system, names): + """A helper for verify scripts to find quickly a set of subtask handlers""" + ret = [] + for x in names: + for name, func in system.functions.items(): + if x == name or \ + "OSEKOS_TASK_" + x == name or \ + "OSEKOS_ISR_" + x == name: + ret.append(func) + return tuple(ret) + +class RunningTaskToolbox: + def __init__(self, analysis): + self.analysis = analysis + self.checked_syscalls = set() + + def mark_syscall(self, syscall): + """Mark syscall as checked""" + self.checked_syscalls.add(syscall) + + def mark_syscalls_in_function(self, function): + """Mark all syscalls in functions as checked""" + for syscall in function.get_syscalls(): + self.mark_syscall(syscall) + + def promise_all_syscalls_checked(self): + assert set(self.analysis.system.get_syscalls()) == self.checked_syscalls, "missing %s" \ + %(set(self.analysis.system.get_syscalls()) - self.checked_syscalls) + + def syscall(self, function, syscall_name, arguments): + """Tests wheter a syscall exists and returns it""" + syscall = self.analysis.system.find_syscall(function, syscall_name, arguments) + assert syscall, "%s:%s(%s) not found" %(function.function_name, syscall_name, arguments) + return syscall + + def reachability(self, function, syscall_name, arguments, possible_subtasks): + """Check to which subtasks a certain syscall can dispatch. Syscall is + marked as visited""" + + syscall = self.syscall(function, syscall_name, arguments) + reachable_subtasks = self.analysis.reachable_subtasks_from_abb(syscall) + assert(set(reachable_subtasks) == set(possible_subtasks)), "%s:%s(%s)::: %s != %s" %( + function.function_name, syscall_name, arguments, list(possible_subtasks), list(reachable_subtasks)) + self.checked_syscalls.add(syscall) + + return syscall + + def activate(self, possible_subtasks, function): + """Check which subtasks can activate a given function. The activating + ABBs are returned""" + activating_subtasks, activating_abbs = self.analysis.activating_subtasks(function) + assert(set(activating_subtasks) == set(possible_subtasks)), "SetReady(%s):: %s != %s" %( + function.function_name, list(activating_subtasks), list(reachable_subtasks)) + + return activating_abbs diff --git a/toolchain/app.cmake b/toolchain/app.cmake index 0748ec0..39508a0 100644 --- a/toolchain/app.cmake +++ b/toolchain/app.cmake @@ -125,5 +125,5 @@ MACRO(COREDOS_BINARY) coredos_executable(${NAME} EXCLUDE_FROM_ALL ${COREDOS_SOURCE_SYSTEM_OBJECT} ${COREDOS_GENERATED_SOURCE}) - add_test(${NAME}-test make ${NAME}-generate) + add_test(${NAME}-test make ${NAME}-clean ${NAME}-generate) ENDMACRO(COREDOS_BINARY) -- GitLab