SparseAbstractInterpretation.h

Go to the documentation of this file.

//===- SparseAbstractInterpretation.h -- Sparse Abstract Execution------//
//
//                     SVF: Static Value-Flow Analysis
//
// Copyright (C) <2013->  <Yulei Sui>
//
 
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU Affero General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
 
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU Affero General Public License for more details.
 
// You should have received a copy of the GNU Affero General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
//
//===---------------------------------------------------------------------===//
 
#ifndef INCLUDE_AE_SVFEXE_SPARSEABSTRACTINTERPRETATION_H_
#define INCLUDE_AE_SVFEXE_SPARSEABSTRACTINTERPRETATION_H_
 
#include "AE/Svfexe/AbstractInterpretation.h"
#include <memory>
 
namespace SVF
{
 
class SVFG;
class SVFGBuilder;
class IndirectSVFGEdge;
class VFGNode;
 
class SemiSparseAbstractInterpretation : public AbstractInterpretation
{
public:
    SemiSparseAbstractInterpretation()
    {
        preAnalysis->initCycleValVars();
    }
    ~SemiSparseAbstractInterpretation() override = default;
 
protected:
    AbstractState getFullCycleHeadState(const ICFGCycleWTO* cycle) override;
 
    bool widenCycleState(const AbstractState& prev,
                         const AbstractState& cur,
                         const ICFGCycleWTO* cycle) override;
 
    bool narrowCycleState(const AbstractState& prev,
                          const AbstractState& cur,
                          const ICFGCycleWTO* cycle) override;
 
    const AbstractValue& getAbsValue(const ValVar* var, const ICFGNode* node) override;
    using AbstractInterpretation::getAbsValue;
 
    bool hasAbsValue(const ValVar* var, const ICFGNode* node) const override;
    using AbstractInterpretation::hasAbsValue;
 
    void updateAbsValue(const ValVar* var, const AbstractValue& val, const ICFGNode* node) override;
    using AbstractInterpretation::updateAbsValue;
 
    void updateAbsState(const ICFGNode* node, const AbstractState& state) override;
 
    void joinStates(AbstractState& dst, const AbstractState& src) override;
 
    const ICFGNode* getICFGNode(const ValVar* var) const;
};
 
class FullSparseAbstractInterpretation : public SemiSparseAbstractInterpretation
{
public:
    FullSparseAbstractInterpretation()
    {
        buildSVFG();
    }
    ~FullSparseAbstractInterpretation() override;
 
protected:
    void joinStates(AbstractState& dst, const AbstractState& src) override;
 
    void storeValue(const ValVar* pointer, const AbstractValue& val,
                    const ICFGNode* node) override;
 
    bool mergeStatesFromPredecessors(const ICFGNode* node) override;
 
    void recordBranchRefinement(NodeID objId, const IntervalValue& narrowed,
                                AbstractState& as, const ICFGNode* loadIcfg,
                                const ICFGNode* succ) override;
 
private:
    void pullObjValueFlows(const ICFGNode* node);
 
    bool isIndirectSVFGEdgeFeasible(const IndirectSVFGEdge* edge,
                                    const VFGNode* dst);
 
    bool isICFGPathFeasible(const ICFGNode* src, const ICFGNode* dst);
 
    bool isIntraEdgeBranchFeasible(const IntraCFGEdge* edge,
                                   const ICFGNode* src);
 
    void propagateAndApplyRefinement(const ICFGNode* node);
 
    Map<const ICFGNode*, Map<NodeID, IntervalValue>> refinementTrace;
 
    void buildSVFG();
 
    std::unique_ptr<SVFGBuilder> svfgBuilder;
    SVFG* svfg{nullptr};
};
 
} // namespace SVF
 
#endif /* INCLUDE_AE_SVFEXE_SPARSEABSTRACTINTERPRETATION_H_ */