| /******************************************************************************* |
| * 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: 23 juil. 2008 |
| * |
| * Contributors: |
| * Arnault Lapitre (CEA LIST) arnault.lapitre@cea.fr |
| * - Initial API and implementation |
| ******************************************************************************/ |
| |
| #ifndef FORMULACOVERAGEFILTER_H_ |
| #define FORMULACOVERAGEFILTER_H_ |
| |
| #include <fam/coverage/BaseCoverageFilter.h> |
| |
| #include <common/AvmPointer.h> |
| #include <common/Element.h> |
| #include <common/BF.h> |
| |
| #include <collection/Bitset.h> |
| #include <collection/Typedef.h> |
| |
| #include <fml/executable/ExecutableForm.h> |
| |
| #include <sew/Configuration.h> |
| |
| #include <solver/api/SolverDef.h> |
| |
| |
| namespace sep |
| { |
| |
| class AvmCode; |
| class ExecutionContext; |
| class WObject; |
| class SatSolver; |
| |
| |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // FormulaData |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| |
| |
| class FormulaData : public Element , |
| AVM_INJECT_INSTANCE_COUNTER_CLASS( FormulaData ) |
| { |
| |
| AVM_DECLARE_CLONABLE_CLASS( FormulaData ) |
| |
| |
| public: |
| /** |
| * ATTRIBUTES |
| */ |
| BF formula; |
| std::string label; |
| avm_offset_t offset; |
| |
| Element * compiled; |
| |
| ListOfExecutionContext satEC; |
| |
| |
| public: |
| FormulaData(const BF & aFormula, const std::string & aLabel, |
| avm_offset_t anOffset, Element * favmFormula) |
| : Element( CLASS_KIND_T( FormulaData ) ), |
| formula( aFormula ), |
| label( aLabel ), |
| offset( anOffset ), |
| |
| compiled( favmFormula ), |
| satEC( ) |
| { |
| //!! NOTHING |
| } |
| |
| |
| /** |
| * DESTRUCTOR |
| */ |
| virtual ~FormulaData() |
| { |
| //!! NOTHING |
| } |
| |
| |
| /** |
| *************************************************************************** |
| * SERIALIZATION |
| *************************************************************************** |
| */ |
| |
| virtual void report(OutStream & os) const; |
| |
| |
| inline std::string str() const |
| { |
| StringOutStream oss( AVM_NO_INDENT ); |
| |
| toStream(oss); |
| |
| return( oss.str() ); |
| } |
| |
| inline void toStream(OutStream & os) const |
| { |
| os << TAB << "<< " << offset << ":" << label << ": " |
| << formula.str() << " >>" << EOL_FLUSH; |
| } |
| |
| inline void toFscn(OutStream & os) const |
| { |
| os << TAB << str() << EOL << std::flush; |
| } |
| |
| }; |
| |
| |
| |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // FormulaCoverageFilter |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| |
| |
| class FormulaCoverageFilter : |
| public AutoRegisteredCoverageProcessorUnit< FormulaCoverageFilter > |
| { |
| |
| AVM_DECLARE_CLONABLE_CLASS( FormulaCoverageFilter ) |
| |
| |
| /** |
| * PROCESSOR FACTORY |
| * for automatic registration in the processor repository |
| * the [ [ FULLY ] QUALIFIED ] NAME ID |
| */ |
| AVM_INJECT_AUTO_REGISTER_QUALIFIED_ID_KEY_2( |
| "avm::processor.FORMULA_COVERAGE", |
| "avm::core.filter.FORMULA_COVERAGE" ) |
| // end registration |
| |
| |
| protected: |
| /** |
| * ATTRIBUTES |
| */ |
| SolverDef::SOLVER_KIND mSolverKind; |
| |
| ExecutableForm mLocalExecutableForm; |
| |
| BF mTrigger; |
| |
| |
| BFVector mFormulaTable; |
| BFList mListOfUncoveredFormula; |
| |
| Bitset mFormulaTruthTable; |
| VectorOfInt mFormulaLinkTable; |
| |
| |
| BFVector mMocTable; |
| BFList mListOfUnCoveredMoc; |
| |
| Bitset mMocTruthTable; |
| VectorOfInt mMocLinkTable; |
| |
| AvmCoverageStatistics mMocCoverageStatistics; |
| |
| |
| public: |
| /** |
| * CONSTRUCTOR |
| * Default |
| */ |
| FormulaCoverageFilter( |
| SymbexControllerUnitManager & aManager, WObject * wfParameterObject) |
| : RegisteredCoverageProcessorUnit(aManager, wfParameterObject, |
| AVM_PREPOST_FILTERING_STAGE, PRECEDENCE_OF_FORMULA_COVERAGE), |
| mSolverKind( SolverDef::SOLVER_UNDEFINED_KIND ), |
| mLocalExecutableForm( getConfiguration().getExecutableSystem() , 0 ), |
| mTrigger( ), |
| |
| mFormulaTable( ), |
| mListOfUncoveredFormula(), |
| mFormulaTruthTable(), |
| mFormulaLinkTable( ), |
| |
| mMocTable( ), |
| mListOfUnCoveredMoc(), |
| mMocTruthTable(), |
| mMocLinkTable( ), |
| mMocCoverageStatistics( ) |
| { |
| //!! NOTHING |
| } |
| |
| /** |
| * DESTRUCTOR |
| */ |
| virtual ~FormulaCoverageFilter() |
| { |
| //!! NOTHING |
| } |
| |
| |
| /** |
| * CONFIGURE |
| */ |
| virtual bool configureImpl(); |
| |
| |
| /** |
| * REPORT TRACE |
| */ |
| virtual void reportDefault(OutStream & os) const; |
| |
| |
| /** |
| * postEval Filter |
| */ |
| virtual bool postfilter(ExecutionContext & anEC); |
| |
| |
| //////////////////////////////////////////////////////////////////////////// |
| // CHECK FORMULA |
| //////////////////////////////////////////////////////////////////////////// |
| bool checksatFormula(ExecutionContext * anEC, |
| const BF & aFormula, FormulaData * aFD); |
| |
| void checkFormula(ExecutionContext * anEC); |
| bool checkFormula(ExecutionContext * anEC, FormulaData * aFD); |
| |
| void checkFormulaAfter(ExecutionContext * anEC); |
| bool checkFormulaAfter(ExecutionContext * anEC, FormulaData * aFD); |
| |
| |
| //////////////////////////////////////////////////////////////////////////// |
| // CHECK MOC |
| //////////////////////////////////////////////////////////////////////////// |
| |
| bool checksatMoc(const BF & aMoc); |
| |
| void mocAppendFormulaLink(const BF & aMoc); |
| void mocRemoveFormulaLink(const BF & aMoc); |
| void mocUpdateUncoveredFormula(); |
| |
| void checkMoc(ExecutionContext * anEC); |
| |
| |
| /* |
| * GETTER |
| * mTrigger |
| */ |
| inline void setTrigger(const BF & aTrigger) |
| { |
| mTrigger = aTrigger; |
| } |
| |
| inline BF & getTrigger() |
| { |
| return( mTrigger); |
| } |
| |
| /* |
| * GETTER |
| * mVectorOfFormula |
| */ |
| BF appendFormula(const BF & aFormula, |
| const std::string & label, Element * favmFormula = NULL); |
| |
| inline BF & getFormula(const std::string & label) |
| { |
| BFVector::iterator itForm = mFormulaTable.begin(); |
| BFVector::iterator endForm = mFormulaTable.end(); |
| for( ; itForm != endForm ; ++itForm ) |
| { |
| if( (*itForm).to_ptr< FormulaData >()->label == label ) |
| { |
| return( *itForm ); |
| } |
| } |
| |
| return( BF::REF_NULL ); |
| } |
| |
| |
| inline BFVector & getFormulaTable() |
| { |
| return( mFormulaTable ); |
| } |
| |
| |
| /* |
| * GETTER |
| * mListOfUncoveredFormula |
| */ |
| inline const BFList & getListOfUnCoveredFormula() const |
| { |
| return( mListOfUncoveredFormula ); |
| } |
| |
| |
| /* |
| * GETTER |
| * mVectorOfMoc |
| */ |
| BF appendMoc(const BF & aMoc, |
| const std::string & label, Element * favmFormula = NULL); |
| |
| inline BFVector & getMocTable() |
| { |
| return( mMocTable ); |
| } |
| |
| BF buildMoc(const BF & aMoc); |
| |
| }; |
| |
| |
| |
| |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| // FormulaCoverageFilter Information |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| |
| class FormulaCoverageFilterInfo : |
| public Element , |
| AVM_INJECT_INSTANCE_COUNTER_CLASS( FormulaCoverageFilterInfo ) |
| { |
| |
| AVM_DECLARE_CLONABLE_CLASS( FormulaCoverageFilterInfo ) |
| |
| |
| protected: |
| /** |
| * ATTRIBUTES |
| */ |
| BFList mFormulaTable; |
| |
| BFList mMocTable; |
| |
| |
| public: |
| /** |
| * CONSTRUCTOR |
| * Default |
| */ |
| FormulaCoverageFilterInfo() |
| : Element( CLASS_KIND_T( FormulaCoverageFilterInfo ) ), |
| mFormulaTable( ), |
| mMocTable( ) |
| { |
| //!! NOTHING |
| } |
| |
| |
| /** |
| * CONSTRUCTOR |
| * Copy |
| */ |
| FormulaCoverageFilterInfo(const FormulaCoverageFilterInfo & anInfo) |
| : Element( anInfo ), |
| mFormulaTable(anInfo.mFormulaTable), |
| mMocTable( anInfo.mMocTable ) |
| { |
| //!! NOTHING |
| } |
| |
| |
| /** |
| * DESTRUCTOR |
| */ |
| virtual ~FormulaCoverageFilterInfo() |
| { |
| //!! NOTHING |
| } |
| |
| /* |
| * GETTER -- SETTER |
| * mFormulaTable |
| */ |
| inline void appendFormula(const BF & aFD) |
| { |
| mFormulaTable.append( aFD ); |
| } |
| |
| inline BFList & getFormulaTable() |
| { |
| return( mFormulaTable ); |
| } |
| |
| |
| /* |
| * GETTER -- SETTER |
| * mMocTable |
| */ |
| inline void appendMoc(BF & aFD) |
| { |
| mMocTable.append( aFD ); |
| } |
| |
| inline void appendMoc(BFList & aTable) |
| { |
| mMocTable.append( aTable ); |
| } |
| |
| inline void appendMoc(BFVector & aTable) |
| { |
| mMocTable.append( aTable ); |
| } |
| |
| inline BFList & getMocTable() |
| { |
| return( mMocTable ); |
| } |
| |
| |
| /** |
| * Serialization |
| */ |
| void toStream(OutStream & os) const; |
| |
| void toFscn(OutStream & os) const; |
| |
| }; |
| |
| |
| |
| } |
| |
| #endif /* FORMULACOVERAGEFILTER_H_ */ |