Commit 688a4805 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Add checker.py

Template file for generating a model checker for the given sdl model
parent bf1383dc
#!/usr/bin/python
# -*- coding: utf-8 -*-
''' Property parser for SDL systems
Template for a simple model checker
(c) European Space Agency, 2015-2017
Author: Maxime Perrotin
'''
from stringtemplate3 import StringTemplateGroup, StringTemplate
import opengeode
asn1_module = '''with <module>;
use <module>;
'''
provided_interface = '''<interface>_pi'''
required_interface = '''<interface>_ri'''
event = '''when <interface>_pi =>
<if(param)>
<interface>_Param: aliased asn1Scc<sort>;
<else>
null;
<endif>'''
check_ppty = u'''errno := <num>;
res := <model>_stop_conditions.p\u00dcproperty_<num>;
if res then
return res;
end if;'''
exhaust_procedure = '''procedure exhaust_<interface> is
<if(param)><interface>_it : <sort>_pkg.Instance;<endif>
event : Event_ty(<interface>);
S_Hash : Hash_Type;
begin
backup_ctxt := Process_Ctxt;
<if(param)>
for each of <interface>_it loop
event.<interface>_param := each;
<model>.<interface>(event.<interface>_param'access);
count := count + 1;
S_Hash := Add_to_graph(event => event);
check_and_report(S_Hash);
Process_Ctxt := backup_ctxt;
end loop;
<else>
<model>.<interface>;
count := count + 1;
S_Hash := Add_to_graph(event => event);
check_and_report(S_Hash);
<endif>
end;'''
exhaust = '''if Process_Ctxt.State in <states;separator= " | "> then
exhaust_<interface>;
end if;'''
checker_template = '''with <model>;
use <model>;
with <model>_stop_conditions;
with asn1_iterators;
use asn1_iterators;
<asn1_modules;separator="\n">
with Ada.Text_IO;
use Ada.Text_IO;
with GNAT.MD5;
with Ada.Streams;
use Ada.Streams;
with Ada.Unchecked_Conversion;
with System;
with Ada.Strings.Hash;
with Ada.Containers.Ordered_maps;
with Ada.Containers.Vectors;
use Ada.Containers;
with Ada.Calendar;
use Ada.Calendar;
procedure model_checker is
subtype Context_ty is <model>_ctxt_ty;
Process_Ctxt : Context_ty renames <model>_Ctxt;
-- To save/restore the context when calling a PI:
backup_ctxt : Context_ty;
-- Type representing an event (input or output)
type Interfaces is (start, <interfaces;separator=", ">);
type Event_ty (Option: Interfaces) is
record
case Option is
when start =>
null;
<events;separator="\n">
end case;
end record;
-- Type representing an entry in the state graph
type Global_State (I: Interfaces) is
record
event : Event_ty(I);
context : Context_ty;
end record;
-- We store only pointers to graph states in the map
type State_Access is access Global_State;
-- The state graph itself is stored in a dictionary type (map)
package State_graph is new Ordered_Maps (Key_Type => Hash_Type,
Element_Type => State_Access);
Grafset : State_graph.Map;
-- State graph index: Use md5 first to get a string representing
-- the context object, then strings.hash to get a number that can be used
-- as a map key. This can surely be improved!
Ctxt_Size: constant stream_element_offset :=
Context_ty'object_size / stream_element'size;
type SEA_Pointer is
access all Stream_Element_Array (1 .. Ctxt_Size);
function As_SEA_Ptr is
new Ada.Unchecked_Conversion (System.Address, SEA_Pointer);
function State_Hash(state: State_Access) return Hash_Type is
(Ada.Strings.Hash(gnat.md5.digest(as_sea_ptr(state.context'address).all)));
-- Add a state to the graph: compute the hash (key) and store if not already there
function Add_to_graph(event : Event_ty) return Hash_Type is
New_State: constant State_Access := new Global_State(event.Option);
New_Hash : Hash_Type;
begin
New_State.event := event;
New_State.context := Process_Ctxt;
New_Hash := State_Hash(New_State);
if not Grafset.Contains(Key => New_Hash) then
Grafset.Insert(Key => New_Hash, New_Item => New_State);
end if;
return New_Hash;
end;
-- To count the number of calls to the function's provided interfaces
count : natural := 0;
-- Vector of hashes (integers) used for the model checking
subtype Vect_Count is Positive range 1 .. 1000;
package Lists is new Vectors (Element_Type => Hash_Type,
Index_type => Vect_Count);
use Lists;
queue : Lists.Vector;
visited : Lists.Vector;
-- Check all properties in one go, and if one fails, set errno
function check_properties(errno: out natural) return boolean is
res : Boolean := false;
begin
<check_properties;separator="\n">
return res;
end;
-- Report the result of the property check to the user
procedure check_and_report (S_Hash: Hash_Type) is
errno: Natural := 0;
stop_condition: boolean := false;
done : boolean := false;
begin
if check_properties(errno) then
put_line("Property " & errno'img & " is verified, at step " & count'img);
stop_condition := true;
end if;
for each_hash of visited loop
if each_hash = S_Hash then
done := true;
exit;
end if;
end loop;
if not done then
visited.append(S_Hash);
if stop_condition = false then
queue.append(S_Hash);
end if;
end if;
end;
-- One function per PI to exhaust the interface parameters
<exhaust_procedures;separator="\n\n">
procedure exhaustive_simulation is
begin
<exhausts;separator="\n">
end;
event : Event_ty(start);
S_Hash : Hash_Type;
Start_Time : Time := Clock;
begin
put_line("Exhaustive simulation. Hit Ctrl-C to stop if it is too long...");
orchestrator.startup;
S_Hash := Add_to_graph(event => event);
check_and_report(S_Hash);
queue.append(S_Hash);
visited.append(S_Hash);
while queue.Length > 0 loop
Process_Ctxt := Grafset.Element(Key => queue.Last_Element).Context;
exhaustive_simulation;
queue.delete_last;
end loop;
put_line("Executed" & count'img & " functions");
put_line("Visited" & Grafset.Length'img & " states");
Put_Line("Execution time:" & Duration'Image(Clock - Start_Time) & "s.");
end;
'''
def generate(ast, stop_conditions):
''' Generate the code for the model checker '''
process = ast.processes[0]
# Set up a StringTemplate group (needed to configure angle-bracket)
group = StringTemplateGroup('checker', '/tmp', lexer='angle-bracket')
# List of ASN.1 modules
asn1 = [name.replace('-', '_') for name in ast.asn1Modules]
# Provided interfaces (process.input_signals)
pis = {pi['name']: pi.get('type', None) for pi in process.input_signals}
# Required interfaces (process.output_signals)
ris = {ri['name']: ri.get('type', None) for ri in process.output_signals}
# Instiantate and fill in the templates with the model data
asn1_modules = []
for each in asn1:
asn1_tpl = StringTemplate(asn1_module, group=group)
asn1_tpl['module'] = each
asn1_modules.append(str(asn1_tpl))
provided_interfaces = []
for each in pis.keys():
pi_tpl = StringTemplate(provided_interface, group=group)
pi_tpl['interface'] = each
provided_interfaces.append(str(pi_tpl))
required_interfaces = []
for each in ris.keys():
ri_tpl = StringTemplate(required_interface, group=group)
ri_tpl['interface'] = each
required_interfaces.append(str(ri_tpl))
events = []
for name, sort in pis.viewitems():
event_tpl = StringTemplate(event, group=group)
event_tpl['interface'] = name
event_tpl['param'] = True if sort else False
event_tpl['sort'] = (opengeode.AdaGenerator.type_name(sort,
use_prefix=False)
if sort else "")
events.append(str(event_tpl))
check_ppties = []
for idx in range(len(stop_conditions)):
check_ppty_tpl = StringTemplate(check_ppty, group=group)
check_ppty_tpl['model'] = process.processName
check_ppty_tpl['num'] = str(idx)
check_ppties.append(unicode(check_ppty_tpl))
exhaust_procedures = []
for name, sort in pis.viewitems():
exhaust_procedure_tpl = StringTemplate(exhaust_procedure, group=group)
exhaust_procedure_tpl['interface'] = name
exhaust_procedure_tpl['param'] = True if sort else False
exhaust_procedure_tpl['sort'] = (opengeode.AdaGenerator.type_name(sort,
use_prefix=False)
if sort else '')
exhaust_procedure_tpl['model'] = process.processName
exhaust_procedures.append(str(exhaust_procedure_tpl))
exhausts = []
for name, sort in pis.viewitems():
exhaust_tpl = StringTemplate(exhaust, group=group)
exhaust_tpl['interface'] = name
# get a mapping {input: {state : transition}}
opengeode.Helper.flatten(process, sep=u'\u00dc')
mapping = opengeode.Helper.map_input_state(process)
states = [state for state in mapping[name].keys() if "START" not
in state]
exhaust_tpl['states'] = states
exhausts.append(str(exhaust_tpl))
complete = StringTemplate(checker_template, group=group)
complete['model'] = process.processName
complete['asn1_modules'] = asn1_modules
complete['interfaces'] = provided_interfaces
complete['events'] = events
complete['check_properties'] = check_ppties
complete['exhaust_procedures'] = exhaust_procedures
complete['exhausts'] = exhausts
with open('model_checker.adb', 'w') as ada_file:
ada_file.write(unicode(complete).encode('latin1'))
......@@ -31,6 +31,8 @@ import argparse
from ColorFormatter import ColorFormatter
import opengeode
import checker
# Set up the logging facilities
log = logging.getLogger(__name__)
console = logging.StreamHandler(sys.__stdout__)
......@@ -79,6 +81,10 @@ def parse_input_files(pr_files, ppty_file, simu=True):
if syntax or semantic or warnings or not stop_conditions:
raise IOError('Error parsing stop conditions - Aborting')
if not simu:
# Generate code for the model checker (not for interactive simulation)
checker.generate(ast[0], stop_conditions)
# Set the context in the Ada generator
opengeode.AdaGenerator.TYPES = process.dataview
opengeode.AdaGenerator.VARIABLES = process.variables
......@@ -130,12 +136,12 @@ def parse_input_files(pr_files, ppty_file, simu=True):
# gather asn.1 files and modules
asn1_files = ' '.join(ast[0].asn1_filenames)
asn1_modules = ' '.join(name.lower().replace('-', '_') + '.o'
asn1_modules_o = ' '.join(name.lower().replace('-', '_') + '.o'
for name in ast[0].asn1Modules)
with open('Makefile.properties', 'w') as Makefile:
Makefile.write(MAKEFILE_TEMPLATE.format(name=process.processName,
asn1=asn1_files,
modules=asn1_modules))
modules=asn1_modules_o))
def cli():
''' Application entry point, when used from the command line '''
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment