| /******************************************************************************* |
| * 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 */ |