Commit 905a87f6 authored by Maxime Perrotin's avatar Maxime Perrotin

Create new repo for taste model checker

parents
This repository contains all the components of the [future] TASTE Model Checker.
ITERATORS_PREFIX?=/usr/local
all:
@echo You can install with "sudo make install"
@echo A testcase can be build from source with "make test"
install:
install -d $(ITERATORS_PREFIX)/share/taste
install -m 644 stg/ada_iterators-iterators-adb.stg $(ITERATORS_PREFIX)/share/taste
install -m 644 stg/ada_iterators-iterators-ads.stg $(ITERATORS_PREFIX)/share/taste
install -m 644 stg/ada_iterators.stg $(ITERATORS_PREFIX)/share/taste
install -m 755 src/taste-asn1-iterators $(ITERATORS_PREFIX)/bin
install -d /usr/share/ada/adainclude/asn1_iterators
install -m 644 src/asn1_iterators.gpr /usr/share/ada/adainclude
install -d /usr/lib/i386-linux-gnu/ada/adalib/asn1_iterators
install -m 644 src/*.ad? /usr/share/ada/adainclude/asn1_iterators
cd src && mkdir -p tmp && cd tmp && gnat make -c -O2 ../*.ad? && \
install -m 644 *.ali /usr/lib/i386-linux-gnu/ada/adalib/asn1_iterators && \
ar r libasn1_iterators.so *.o && cp libasn1_iterators.so /usr/lib/i386-linux-gnu && \
cd ../.. && rm -rf src/tmp
test_install: clean
mkdir -p build_test
cp test/DataView.asn build_test
cp test/test_generic.gpr build_test
cp test/test_generic.adb build_test
cd build_test && taste-asn1-iterators DataView.asn && gprbuild test_generic.gpr
test: test_install
build_test/test_generic
clean:
@rm -rf build_test
.PHONY: all clean install test_install
asn1-iterators
==============
(c) 2016-2017 European Space Agency
Author/Contact: Maxime.Perrotin@esa.int
Generic iterator functions in Ada for generating all combinations of values of ASN.1 data types
v0.1 support for INTEGER with a range and SEQUENCE OF INTEGER (fixed and variable size arrays)
test:
cd src
make
Work in progress... Part of the TASTE project.
-- (c) 2017 European Space Agency / TASTE Project
package body ASN1_Iterators.Exhaustive_Simulation is
function State_Hash(Context: Context_Ty) return Hash_Type is
(Ada.Strings.Hash(gnat.md5.digest(as_sea_ptr(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: State_Access;
New_Hash : Hash_Type;
New_Edge : constant Edge_ty := (event => event, state => backup_hash);
begin
New_Hash := State_Hash(Process_Ctxt.all);
if not Grafset.Contains(Key => New_Hash) then
New_State := new Global_State;
New_State.context := Process_Ctxt.all;
Grafset.Insert(Key => New_Hash, New_Item => New_State);
else
New_State := Grafset.Element(Key => New_Hash);
end if;
New_State.edges.append(New_Edge);
return New_Hash;
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;
begin
count := count + 1;
if check_properties(errno) then
put_line("Property " & errno'img & " is verified, at step " & count'img);
stop_condition := true;
if properties.Length <= 10 then
properties.include(s_hash);
end if;
end if;
if not visited.contains(s_hash) then
visited.insert(s_hash);
if stop_condition = false then
queue.append(S_Hash);
end if;
end if;
end;
procedure Generate_MSC is
package Loc_Maps is new Ordered_Maps(Key_Type => Hash_Type,
Element_Type => Boolean);
package Evt_Lists is new Vectors(Element_Type => Event_ty,
Index_Type => Vect_Count);
package Parent_Maps is new Ordered_Maps(Key_Type => Hash_Type,
Element_Type => Edge_ty);
function Find_Path(From: Hash_Type) return Evt_Lists.Vector is
Loc_Q : Lists.Vector;
Loc_Visited : Loc_Maps.Map;
Next_Hash : Hash_Type;
State : State_Access;
Parent_Map : Parent_Maps.Map;
Curr : Hash_Type;
Edge : Edge_Ty;
Scenario : Evt_Lists.Vector;
begin
Loc_Q.append(From);
Loc_Visited.Include(Key => From, New_Item => True);
while not Loc_Q.Is_Empty loop
Next_Hash := Loc_Q.Last_Element;
exit when Next_Hash = Start_Hash;
State := Grafset.Element(Key => Next_Hash);
for each_edge of State.Edges loop
if not Loc_Visited.Contains(each_edge.state) then
Loc_Q.append(Each_Edge.state);
Loc_Visited.Include(Key => each_edge.state,
New_Item => True);
Parent_Map.Include(Key => Each_Edge.State,
New_Item => (State => Next_Hash,
Event => Each_Edge.Event));
end if;
end loop;
Loc_Q.Delete_Last;
end loop;
Curr := Start_Hash;
Put_Line("Found path!");
while Parent_Map.Contains(Curr) loop
Edge := Parent_Map.Element(Curr);
Curr := Edge.State;
Scenario.Append(Edge.Event);
end loop;
return Scenario;
end;
Scenario : Evt_Lists.Vector;
begin
for each_hash of properties loop
put_line("Path from hash " & each_hash'img & " to hash " & start_hash'img);
Scenario := Find_Path(each_hash);
for each_evt of Scenario loop
Print_Event(each_evt);
end loop;
end loop;
end;
end ASN1_Iterators.Exhaustive_Simulation;
-- (c) 2017 European Space Agency / TASTE Project
with Ada.Unchecked_Conversion,
System,
Ada.Text_IO,
Ada.Streams,
Ada.Strings.Hash,
Ada.Containers.Ordered_Maps,
Ada.Containers.Ordered_Sets,
Ada.Containers.Vectors,
Ada.Calendar,
GNAT.MD5;
use Ada.Containers,
Ada.Calendar,
Ada.Streams,
Ada.Text_IO;
generic
type Context_ty is private;
Process_Ctxt: access Context_ty;
type Event_ty is private;
with procedure Print_Event(event: Event_ty);
with function Check_Properties(errno: out natural) return Boolean;
package ASN1_Iterators.Exhaustive_Simulation is
-- To save/restore the context when calling a PI:
backup_ctxt : Context_ty;
backup_hash : Hash_Type;
start_hash : Hash_Type;
-- Set a maximum size for vectors (set of states and edges)
subtype Vect_Count is Positive range 1 .. 1000000;
-- An edge is made of a past state reference and an event to leave it
type Edge_ty is
record
event : Event_ty;
state : Hash_Type;
end record;
package Edges_Pkg is new Vectors (Element_Type => Edge_ty,
Index_Type => Vect_Count);
-- A state is made of a context and a set of edges leading to it
type Global_State is
record
edges : Edges_Pkg.Vector := Edges_Pkg.Empty_Vector;
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(Context: Context_Ty) return Hash_Type;
-- 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;
-- To count the number of calls to the function's provided interfaces
Count : natural := 0;
-- Vector of hashes (integers) used for the model checking
package Lists is new Vectors (Element_Type => Hash_Type,
Index_type => Vect_Count);
package Sets is new Ordered_Sets(Element_Type => Hash_Type);
Queue : Lists.Vector;
Visited : Sets.Set;
Properties : Sets.Set;
-- Report the result of the property check to the user
procedure Check_And_Report (S_Hash: Hash_Type);
procedure Generate_MSC;
end ASN1_Iterators.Exhaustive_Simulation;
package body ASN1_Iterators.Generic_Basic is
procedure Initialize (self: in out Basic_ASN1_Iterator) is
begin
--Self.Value := create;
Self.Value.Initialize;
end;
function First (Item : Iterator) return Iterator_Ptr is
begin
Item.Ptr.Value.First;
return Item.Ptr;
end;
function Next (Item : Iterator;
Ptr : Iterator_Ptr) return Iterator_Ptr is
pragma Unreferenced (Item);
begin
Ptr.Value.Next;
return Ptr;
end;
function Iterate (self : Basic_ASN1_Iterator)
return Forward_Iterator is
begin
return I: Iterator do
I.Ptr := self'Unrestricted_Access;
end return;
end;
end;
with Ada.Iterator_Interfaces;
with Ada.Finalization;
use Ada.Finalization;
with ASN1_Iterators.SimpleTypes;
generic
with package P is new SimpleTypes (<>);
package ASN1_Iterators.Generic_Basic is
-- Provides an iterator for a basic type
subtype Element is P.Element;
type Basic_ASN1_Iterator is new Controlled
with record
Value : P.SimpleType;
end record
with Default_Iterator => Iterate,
Iterator_Element => P.Element,
Constant_Indexing => Elem_Value;
procedure Initialize(self: in out Basic_ASN1_Iterator);
type Iterator_Ptr is access all Basic_ASN1_Iterator;
function Has_Element (Ptr : Iterator_Ptr) return Boolean is
(Ptr.Value.Has_Element);
package Iterators is
new Ada.Iterator_Interfaces (Iterator_Ptr, Has_Element);
type Iterator is new Iterators.Forward_Iterator with record
Ptr : Iterator_Ptr;
end record;
function Ptr (Item: Iterator) return Iterator_Ptr is (Item.Ptr);
overriding function First (Item : Iterator) return Iterator_Ptr;
overriding function Next (Item : Iterator;
Ptr : Iterator_Ptr) return Iterator_Ptr;
subtype Forward_Iterator is Iterators.Forward_Iterator'Class;
function Iterate (self : Basic_ASN1_Iterator) return Forward_Iterator;
function Elem_Value (self : Basic_ASN1_Iterator;
Ptr : Iterator_Ptr)
return P.Element is (Ptr.Value.Element_Value);
end;
with Ada.Unchecked_Conversion;
package body ASN1_Iterators.Generic_Fixed_SeqOf is
procedure Initialize (self: in out ASN1_SeqOf) is
begin
self.value.length := self.length;
if self.length > 1 then
self.Rest := new ASN1_SeqOf(self.Length - 1);
self.RestIt := new ASN1_SeqOf_It'(ASN1_SeqOf_It(self.Rest.Iterate));
self.RestIt.Ptr := self.RestIt.First;
end if;
end;
function Has_Element_SeqOf (Ptr: ASN1_SeqOf_Ptr) return Boolean is
(P.Has_Element(P.Ptr(Ptr.FirstIt)));
function Iterate (self : ASN1_SeqOf)
return Iterators_SeqOf.Forward_Iterator'Class is
begin
return I: ASN1_SeqOf_It do
I.Ptr := self'Unrestricted_Access;
end return;
end;
function First (Item : ASN1_SeqOf_It) return ASN1_SeqOf_Ptr is
Ptr_elem : P.Iterator_Ptr := P.Ptr(Item.Ptr.FirstIt);
begin
-- Initialize the iterator (Compute first value)
Item.Ptr.FirstIt := P.Iterator(Item.Ptr.FirstVal.Iterate);
Ptr_elem := P.First(Item.Ptr.FirstIt);
Item.Ptr.Value.Data(1) := P.Elem_Value(Item.Ptr.FirstVal,
Ptr_elem);
if Item.Ptr.Length > 1 then
Item.Ptr.Value.Data(2 .. Item.Ptr.Length) :=
Item.Ptr.RestIt.Ptr.Value.Data(1..Item.Ptr.RestIt.Ptr.Length);
end if;
return Item.Ptr;
end;
function Next (Item : ASN1_SeqOf_It;
Ptr : ASN1_SeqOf_Ptr) return ASN1_SeqOf_Ptr is
pragma Unreferenced (Item);
Ptr_elem : P.Iterator_Ptr := P.Ptr(Ptr.FirstIt);
begin
if Ptr.Length > 1 then
Ptr.RestIt.Ptr := Ptr.RestIt.Next (Ptr.RestIt.Ptr);
if Has_Element_SeqOf (Ptr.RestIt.Ptr) then
Ptr.Value.Data (2..Ptr.Length) :=
Ptr.RestIt.Ptr.Value.Data (1..Ptr.RestIt.Ptr.Value.Length);
else
Ptr.RestIt.Ptr := Ptr.RestIt.First;
-- Exhausted "rest": iterate on the first item
Ptr_elem := P.Next(Ptr.FirstIt, Ptr_elem);
if P.Has_Element (Ptr_elem) then
Ptr.Value.Data(1) := P.Elem_Value(Ptr.FirstVal, Ptr_elem);
Ptr.Value.Data(2..Ptr.Length) := Ptr.RestIt.Ptr.Value.Data (1..Ptr.RestIt.Ptr.Length);
end if;
end if;
else
-- Size is 0 or 1
Ptr_elem := P.Next(Ptr.FirstIt, Ptr_elem);
if P.Has_Element (Ptr_elem) then
Ptr.Value.Data(1) := P.Elem_Value(Ptr.FirstVal, Ptr_elem);
end if;
end if;
return Ptr;
end;
end;
with Ada.Iterator_Interfaces;
with Ada.Finalization;
use Ada.Finalization;
with ASN1_Iterators.Generic_Basic;
generic
with package P is new Generic_Basic (<>);
package ASN1_Iterators.Generic_Fixed_SeqOf is
type DataArray is array(natural range <>) of P.Element;
type SeqOf (Max: Natural) is record
Length : Integer;
Data : DataArray(1..Max);
end record;
type ASN1_SeqOf_Ptr;
type ASN1_SeqOf_It;
type ASN1_SeqOf (Size: Natural) is new Controlled
with record
Length : Natural := Size;
Value : SeqOf (Size);
-- First value
FirstVal : P.Basic_ASN1_Iterator;
FirstIt : P.Iterator;
-- The rest (recursive)
Rest : access ASN1_SeqOf;
RestIt : access ASN1_SeqOf_It;
end record
with Default_Iterator => Iterate,
Iterator_Element => SeqOf,
Constant_Indexing => Element_SeqOf_Value;
type ASN1_SeqOf_Ptr is access all ASN1_SeqOf;
-- Constructor (called automatically)
procedure Initialize(self: in out ASN1_SeqOf);
function Has_Element_SeqOf (Ptr : ASN1_SeqOf_Ptr) return Boolean;
package Iterators_SeqOf is
new Ada.Iterator_Interfaces (ASN1_SeqOf_Ptr, Has_Element_SeqOf);
type ASN1_SeqOf_It is new Iterators_SeqOf.Forward_Iterator with record
Ptr : ASN1_SeqOf_Ptr;
end record;
overriding function First (Item : ASN1_SeqOf_It) return ASN1_SeqOf_Ptr;
overriding function Next (Item : ASN1_SeqOf_It;
Ptr : ASN1_SeqOf_Ptr) return ASN1_SeqOf_Ptr;
function Iterate (self : ASN1_SeqOf)
return Iterators_SeqOf.Forward_Iterator'Class;
function Element_SeqOf_Value (self : ASN1_SeqOf;
Ptr : ASN1_SeqOf_Ptr)
return SeqOf is (self.Value);
end;
with ASN1_Iterators.SimpleTypes,
ASN1_Iterators.Generic_Basic;
with Interfaces;
use Interfaces;
generic
Min: Interfaces.Integer_64;
Max: Interfaces.Integer_64;
package ASN1_Iterators.Generic_Integer is
function Elem_Init return Interfaces.Integer_64 is (Min);
function Has_Elem(Value: Interfaces.Integer_64) return Boolean is
(Value <= Max);
function Elem_First return Interfaces.Integer_64 is (Min);
function Elem_Next(Value: Interfaces.Integer_64) return Interfaces.Integer_64 is
(Value + 1);
package Integer_type is new SimpleTypes(Element => Interfaces.Integer_64,
Elem_Init => Elem_Init,
Has_Elem => Has_Elem,
Elem_First => Elem_First,
Elem_Next => Elem_Next);
package It is new Generic_Basic (P => Integer_type);
subtype Instance is It.Basic_ASN1_Iterator;
end;
package body ASN1_Iterators.Generic_SeqOf is
procedure Initialize (self: in out ASN1_Variable_SeqOf) is
begin
self.value.length := self.length;
if self.length >= 1 then
self.RestVal := new P.ASN1_SeqOf(Self.Length);
self.RestIt := new P.ASN1_SeqOf_It'(P.ASN1_SeqOf_It(Self.RestVal.Iterate));
self.RestIt.Ptr := self.RestIt.First;
end if;
end;
function Has_Element_Variable_SeqOf (Ptr: ASN1_Variable_SeqOf_Ptr)
return Boolean is (Length_Pkg.Has_Element(Length_Pkg.Ptr(Ptr.LenIt)));
function Iterate (self : ASN1_Variable_SeqOf)
return Iterators_Variable_SeqOf.Forward_Iterator'Class is
begin
return I: ASN1_Variable_SeqOf_It do
I.Ptr := Self'Unrestricted_Access;
end return;
end;
function First (Item : ASN1_Variable_SeqOf_It) return ASN1_Variable_SeqOf_Ptr is
begin
-- Initialize the iterator (Compute first value)
Item.Ptr.LenIt := Length_Pkg.Iterator(Item.Ptr.LenVal.Iterate);
--Item.Ptr.Value := Item.Ptr.RestIt.Ptr.Value;
-- Copy only the actual size, since the arrays may be different in size
Item.Ptr.Value.Data(1..Item.Ptr.RestIt.Ptr.Value.Data'Length) := Item.Ptr.RestIt.Ptr.Value.Data;
return Item.Ptr;
end;
function Next (Item : ASN1_Variable_SeqOf_It;
Ptr : ASN1_Variable_SeqOf_Ptr) return ASN1_Variable_SeqOf_Ptr is
pragma Unreferenced (Item);
Ptr_elem : Length_Pkg.Iterator_Ptr := Length_Pkg.Ptr(Ptr.LenIt);
begin
Ptr.RestIt.Ptr := Ptr.RestIt.Next (Ptr.RestIt.Ptr);
if P.Has_Element_SeqOf (Ptr.RestIt.Ptr) then
--Ptr.Value := Ptr.RestIt.Ptr.Value;
Ptr.Value.Data(1..Ptr.RestIt.Ptr.Value.Data'Length) := Ptr.RestIt.Ptr.Value.Data;
else
Ptr.RestIt.Ptr := Ptr.RestIt.First;
-- Exhausted "rest": iterate on the first item
Ptr_elem := Ptr.LenIt.Next(Ptr_elem);
if Length_Pkg.Has_Element (Ptr_elem) then
Ptr.Value.Length := Integer(Ptr_elem.Value.Value);
Ptr.Length := Ptr.Value.Length;
Ptr.RestVal := new P.ASN1_SeqOf(Ptr.Value.Length);
Ptr.RestIt := new P.ASN1_SeqOf_It'(P.ASN1_SeqOf_It(Ptr.RestVal.Iterate));
Ptr.RestIt.Ptr := Ptr.RestIt.First;
--Ptr.Value := Ptr.RestIt.Ptr.Value;
Ptr.Value.Data(1..Ptr.RestIt.Ptr.Value.Data'Length) := Ptr.RestIt.Ptr.Value.Data;
end if;
end if;
return Ptr;
end;
end;
with Ada.Iterator_Interfaces;
with Ada.Finalization;
use Ada.Finalization;
with ASN1_Iterators.Generic_Fixed_SeqOF,
ASN1_Iterators.Generic_Integer,
ASN1_Iterators.Generic_Basic;
with Interfaces;
use Interfaces;
-- Iterator for a variable-size array of basic type
generic
Min : Natural;
Max : Natural;
with package Basic is new Generic_Basic (<>);
package ASN1_Iterators.Generic_SeqOf is
Package P is new Generic_Fixed_SeqOF (P => Basic);
-- Create an integer type with a range constraint to iterate on
package Length_ty is new Generic_Integer (Integer_64(Min),
Integer_64(Max));
-- Instantiate the package to iterate on the integer for the length
package Length_Pkg renames Length_ty.It;
type ASN1_Variable_SeqOf_Ptr is private;
subtype MySeqOf is P.SeqOf(Max);
type ASN1_Variable_SeqOf is new Controlled
with record
Length : Natural := Min;
Value : MySeqOf; -- P.SeqOf(Max);
-- Iterate on the length
LenVal : Length_ty.Instance;
LenIt : Length_Pkg.Iterator;
-- And on the value
RestVal : access P.ASN1_SeqOf;
RestIt : access P.ASN1_SeqOf_It;
end record
with Default_Iterator => Iterate,
Iterator_Element => MySeqOf, --P.SeqOf,
Constant_Indexing => Element_Variable_SeqOf_Value;
-- Constructor (called automatically)
procedure Initialize(self: in out ASN1_Variable_SeqOf);
function Has_Element_Variable_SeqOf (Ptr : ASN1_Variable_SeqOf_Ptr)
return Boolean;
package Iterators_Variable_SeqOf is
new Ada.Iterator_Interfaces (ASN1_Variable_SeqOf_Ptr,
Has_Element_Variable_SeqOf);
type ASN1_Variable_SeqOf_It
is new Iterators_Variable_SeqOf.Forward_Iterator with record
Ptr : ASN1_Variable_SeqOf_Ptr;
end record;
overriding
function First (Item : ASN1_Variable_SeqOf_It)
return ASN1_Variable_SeqOf_Ptr;
overriding
function Next (Item : ASN1_Variable_SeqOf_It;
Ptr : ASN1_Variable_SeqOf_Ptr)
return ASN1_Variable_SeqOf_Ptr;
function Iterate (self : ASN1_Variable_SeqOf)
return Iterators_Variable_SeqOf.Forward_Iterator'Class;
function Element_Variable_SeqOf_Value (Self : ASN1_Variable_SeqOf;
Ptr : ASN1_Variable_SeqOf_Ptr)
--return P.SeqOf is (Self.Value);
return MySeqOf is (Self.Value);
subtype Instance is ASN1_Variable_SeqOf;
private
type ASN1_Variable_SeqOf_Ptr is access all ASN1_Variable_SeqOf;
end;
package body ASN1_Iterators.SimpleTypes is
procedure Initialize (Self : in out SimpleType) is
begin
Self.Value := Elem_Init;
end;
procedure First (Self : in out SimpleType) is
begin
Self.Value := Elem_First;
end;
procedure Next (Self : in out SimpleType) is
begin
Self.Value := Elem_Next (Self.Value);
end;
end;
generic
type Element is private;
with function Elem_Init return Element;
with function Has_Elem (Value: Element) return Boolean;
with function Elem_First return Element;
with function Elem_Next (Value: Element) return Element;
package ASN1_Iterators.SimpleTypes is
type SimpleType is tagged
record
Value: Element;
end record;
procedure Initialize (Self : in out SimpleType);
function Has_Element (Self : in out SimpleType) return Boolean is
(Has_Elem (Self.Value));
procedure First (Self : in out SimpleType);
procedure Next (Self : in out SimpleType);
function Element_Value (Self : in out SimpleType) return Element is
(Self.Value);