blob: 8e955874f40b97003fe126fc5a1c0989fd0a626d [file] [log] [blame]
/*******************************************************************************
* Copyright (c) 2016 CEA LIST.
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Created on: 7 janv. 2014
*
* Contributors:
* Arnault Lapitre (CEA LIST) arnault.lapitre@cea.fr
* - Initial API and implementation
******************************************************************************/
#include "BaseHitProcessor.h"
#include <builder/Builder.h>
#include <computer/EvaluationEnvironment.h>
#include <fam/hitorjump/AvmHitOrJumpProcessor.h>
#include <fml/executable/ExecutableForm.h>
#include <fml/executable/ExecutableSystem.h>
#include <fml/executable/InstanceOfData.h>
#include <fml/expression/AvmCode.h>
#include <fml/type/TypeSpecifier.h>
#include <fml/trace/TraceFactory.h>
#include <fml/workflow/Query.h>
#include <fml/workflow/WObject.h>
#include <sew/Configuration.h>
#include <solver/api/SolverFactory.h>
namespace sep
{
/**
* CONSTRUCTOR
* Default
*/
BaseHitProcessor::BaseHitProcessor(AvmHitOrJumpProcessor & hojProcessor,
EvaluationEnvironment & anENV, Operator * op)
: mHitOrJumpProcessor( hojProcessor ),
mCoverageStatistics( hojProcessor.getCoverageStatistics() ),
ENV( anENV ),
mSolverKind( SolverDef::SOLVER_UNDEFINED_KIND ),
mLocalExecutableForm(
mHitOrJumpProcessor.getConfiguration().getExecutableSystem(), 0 ),
mTraceChecker( anENV, &mLocalExecutableForm ),
mTraceObjective( op ),
isPureStateTransitionNatureFlag( false ),
// Computing Local Variables
traceOffset( 0 ),
mRelativeRootEC( hojProcessor.mRelativeRootEC ),
ecIt( ),
ecItEnd( ),
mRelativeLeafEC( hojProcessor.mRelativeLeafEC ),
mAbsoluteLeafEC( hojProcessor.mAbsoluteLeafEC ),
mBlackHoleEC( hojProcessor.mBlackHoleEC ),
mBacktrackHitEC( hojProcessor.mBacktrackHitEC ),
mBacktrackFlag( hojProcessor.mBacktrackFlag ),
mJumpHeight( 0 ),
mMaxHitEC( ),
hitOffset( 0 ),
hitOffsetEnd( 0 ),
mHitCount( 0 ),
ecChildIt( ),
ecChildItEnd( )
{
//!! NOTHING
}
/**
* GETTER
* mTraceObjective
*/
bool BaseHitProcessor::isPureStateTransitionObjective() const
{
for( avm_size_t offset = 0 ; offset < mTraceObjective.size() ; ++offset )
{
if( mTraceChecker.isPointNature(mTraceObjective[offset],
ENUM_TRACE_POINT::TRACE_TRANSITION_NATURE) )
{
//!! CONTINUE
}
else if( mTraceChecker.isPointNature(mTraceObjective[offset],
ENUM_TRACE_POINT::TRACE_STATE_NATURE) )
{
//!! CONTINUE
}
else if( mTraceChecker.isPointNature(mTraceObjective[offset],
ENUM_TRACE_POINT::TRACE_STATEMACHINE_NATURE) )
{
//!! CONTINUE
}
else
{
return( false );
}
}
return( true );
}
/*
prototype process::hit_or_jump as &avm::processor.HIT_OR_JUMP is
section REPORT
...
endsection REPORT
section PROPERTY
...
endsection PROPERTY
// Declaration part
section POINT
@assign = "sens";
@newfresh = "sens";
@signal#sens = "sens";
@port = "env";
@input = "env";
@output = "env";
@output = "Thermostat->dt";
@input = "Thermostat->equip";
@output2 = "Equipment->error";
endsection POINT
section TRACE
@trace = ${ && "signal#sens" "output2" };
@trace = [ "signal#sens" , "output2" ];
@point = ( "signal#sens" || "output2" );
@composite = ${ xor "signal#sens" "output2" };
@assign = "sens";
@newfresh = "sens";
@signal = "sens";
@port = "env";
@input = "env";
@output = "env";
@output = "Thermostat->dt";
@input = "Thermostat->equip";
@output = "Equipment->error";
endsection TRACE
endprototype
*/
////////////////////////////////////////////////////////////////////////////////
// CONFIGURE API
////////////////////////////////////////////////////////////////////////////////
bool BaseHitProcessor::configure(WObject * wfParameterObject)
{
const ExecutableSystem & anExecutableSystem =
mHitOrJumpProcessor.getConfiguration().getExecutableSystem();
mCoverageStatistics.resetCounter();
WObject * thePROPERTY = Query::getRegexWSequence(
wfParameterObject, OR_WID2("property", "PROPERTY"));
if( thePROPERTY != WObject::_NULL_ )
{
std::string mSolverName =
Query::getWPropertyString(thePROPERTY, "solver", "");
if( mSolverName.empty() )
{
AVM_IF_DEBUG_FLAG( SOLVING )
thePROPERTY->warningLocation(AVM_OS_WARN)
<< "Unexpected an empty solver engine kind!!!!!" << std::endl;
AVM_ENDIF_DEBUG_FLAG( SOLVING )
}
mSolverKind = SolverDef::toSolver(
mSolverName, SolverDef::DEFAULT_SOLVER_KIND);
}
else
{
mSolverKind = SolverDef::SOLVER_CVC4_KIND;
}
mTraceChecker.setSolverKind( mSolverKind );
WObject * theDATA = Query::getRegexWSequence(
wfParameterObject, OR_WID2("data", "DATA"));
if( theDATA != WObject::_NULL_ )
{
anExecutableSystem.initProcessExecutableForm(
mLocalExecutableForm, theDATA->ownedSize());
List< WObject * > listOfLocalVar;
Query::getListWObject(theDATA, listOfLocalVar);
TypeSpecifier aTypeSpecifier;
List< WObject * >::iterator it = listOfLocalVar.begin();
List< WObject * >::iterator itEnd = listOfLocalVar.end();
for( avm_offset_t offset = 0 ; it != itEnd ; ++it , ++offset )
{
aTypeSpecifier = ENV.getBuilder().getCompiler().
compileTypeSpecifier(&mLocalExecutableForm,
(*it)->getQualifiedTypeNameID() );
BF anInstance( new InstanceOfData(
IPointerDataNature::POINTER_STANDARD_NATURE,
&mLocalExecutableForm, NULL, aTypeSpecifier,
(*it)->getFullyQualifiedNameID(), offset) );
mLocalExecutableForm.setData( offset , anInstance );
}
}
else
{
anExecutableSystem.initProcessExecutableForm(
mLocalExecutableForm, 0);
}
WObject * theTRACE = Query::getRegexWSequence(
wfParameterObject, OR_WID2("trace", "TRACE"));
if( (theTRACE == WObject::_NULL_) || theTRACE->hasnoOwnedElement() )
{
return true;
}
// Configuration of TRACE
TraceFactory traceFactory(mHitOrJumpProcessor.getConfiguration(),
ENV, wfParameterObject, &mLocalExecutableForm);
if( traceFactory.configure(& mTraceObjective) )
{
// return( false );
}
AVM_IF_DEBUG_LEVEL_FLAG( LOW , CONFIGURING )
AVM_OS_LOG << "The parsed trace :> " << std::endl;
mTraceObjective.toStream( AVM_OS_LOG << AVM_TAB1_INDENT );
mLocalExecutableForm.toStream( AVM_OS_LOG);
AVM_OS_LOG << END_INDENT << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( LOW , CONFIGURING )
mCoverageStatistics.mNumberOfElements = mTraceObjective.size();
mCoverageStatistics.mCoverageBitset.resize(
mCoverageStatistics.mNumberOfElements, false);
isPureStateTransitionNatureFlag = isPureStateTransitionObjective();
return( mCoverageStatistics.mNumberOfElements > 0 );
}
////////////////////////////////////////////////////////////////////////////////
// CONFIGURE API
////////////////////////////////////////////////////////////////////////////////
bool BaseHitProcessor::resetConfig()
{
mCoverageStatistics.resetCoverageCounter();
return( true );
}
////////////////////////////////////////////////////////////////////////////////
// FILTERING TOOLS
////////////////////////////////////////////////////////////////////////////////
bool BaseHitProcessor::isAbsoluteLeaf(ExecutionContext * anEC)
{
if( (not anEC->hasNext()) && ((anEC->getHeight() < mJumpHeight) ||
(not mRelativeLeafEC.contains(anEC)) ) )
{
//!! DeadLock or Absolute Stop ?
mAbsoluteLeafEC.append( anEC );
AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , PROCESSOR )
AVM_OS_TRACE << "<<<<< HoJ< DeadLock or Absolute Stop > >>>>> EC< id:"
<< anEC->getIdNumber() << " >" << std::endl;
AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , PROCESSOR )
return( true );
}
return( false );
}
////////////////////////////////////////////////////////////////////////////////
// SERIALIZATION API
////////////////////////////////////////////////////////////////////////////////
void BaseHitProcessor::toStreamCovered(OutStream & os) const
{
os << TAB << "hit<covered> { " << mHitOrJumpProcessor.strScheduler();
if( mCoverageStatistics.mCoverageBitset.anyTrue() )
{
os << EOL_INCR_INDENT;
for( avm_size_t traceOffset = 0 ;
traceOffset != mCoverageStatistics.mNumberOfElements ;
++traceOffset )
{
if( mCoverageStatistics.mCoverageBitset.test(traceOffset) )
{
mTraceObjective[traceOffset].toStream(os);
}
}
os << DECR_INDENT_TAB ;
}
else
{
os << " ";
}
os << "}" << EOL;
}
void BaseHitProcessor::toStreamUncovered(OutStream & os) const
{
os << TAB << "hit<uncovered> { " << mHitOrJumpProcessor.strScheduler();
if( mCoverageStatistics.mCoverageBitset.anyFalse() )
{
os << EOL_INCR_INDENT;
avm_size_t offset = 0;
for( ; offset != mCoverageStatistics.mNumberOfElements ; ++offset )
{
if( not mCoverageStatistics.mCoverageBitset.test(offset) )
{
mTraceObjective[offset].toStream(os);
}
}
os << DECR_INDENT_TAB ;
}
else
{
os << " ";
}
os << "}" << EOL;
}
} /* namespace sep */