Z3 DSE crashes on SmartCardProtocol
Summary
Performing Z3 DSE on the SmartCardProtocol project from the in-built repository crashes.
Steps to reproduce
- Load the SmartCardProtocol from the in-built repository.
- Switch to Mapping1 and start Z3 DSE.
What is the current bug behavior?
The process fails with the following error:
ERROR: Z3 Unknown Exception: Cannot invoke "tmltranslator.TMLTask.getOperation()" because "tmlTask" is null
What is the expected correct behavior?
The process completes successfully, e.g.:
Optimized mapping found
The optimal mapping solution is:
(1) Spatial mapping of tasks:
TASK --> PLATFORM NODE
AppC__InterfaceDevice --> cpu0
AppC__SmartCard --> cpu0
AppC__TCPIP --> cpu0
AppC__Application --> cpu0
AppC__Timer --> cpu0
(2) Temporal mapping of tasks:
cpu0 : AppC__Timer at 0 ; AppC__Application at 1 ;
(3) Spatial mapping of channels onto controllers:
Channel(InterfaceDevice,SmartCard) --> cpu0
Channel(SmartCard,TCPIP) --> cpu0
Channel(SmartCard,InterfaceDevice) --> cpu0
Channel(TCPIP,TCPIP) --> cpu0
Channel(TCPIP,Application) --> cpu0
Channel(TCPIP,SmartCard) --> cpu0
Channel(Application,TCPIP) --> cpu0
Possible fixes
The issue is masked or possibly resolved by rolling back the following change: !107 (diffs) The change is undocumented and the intention is not obvious.
Relevant logs and/or screenshots
Debugging the code check above with a "task name | writers.Empty() | readers.Empty()" scheme yields:
[tmltranslator.dsez3engine.InputInstance] AppC__Timer true true
[tmltranslator.dsez3engine.InputInstance] AppC__InterfaceDevice false false
[tmltranslator.dsez3engine.InputInstance] AppC__TCPIP false false
[tmltranslator.dsez3engine.InputInstance] fAppC__Application false true
[tmltranslator.dsez3engine.InputInstance] AppC__SmartCard false false
Thus, AppC__Timer
is not picked as final task with the change from the MR, but is picked prior.