AbstractState.h

Go to the documentation of this file.

//===- AbstractExeState.h ----Interval Domain-------------------------//
//
//                     SVF: Static Value-Flow Analysis
//
// Copyright (C) <2013-2022>  <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/>.
//
//===----------------------------------------------------------------------===//
/*
 * IntervalExeState.h
 *
 *  Created on: Jul 9, 2022
 *      Author: Xiao Cheng, Jiawei Wang
 *
 *                         [-oo,+oo]
 *          /           /            \           \
 *       [-oo,1] ... [-oo,10] ... [-1,+oo] ... [0,+oo]
 *          \           \           /          /
 *           \            [-1,10]            /
 *            \        /         \         /
 *       ...   [-1,1]      ...     [0,10]      ...
 *           \    |    \         /       \    /
 *       ...   [-1,0]    [0,1]    ...     [1,9]  ...
 *           \    |   \    |   \        /
 *       ...  [-1,-1]  [0,0]     [1,1]  ...
 *         \    \        \        /      /
 *                          ⊥
 */
// The implementation is based on
// Xiao Cheng, Jiawei Wang and Yulei Sui. Precise Sparse Abstract Execution via Cross-Domain Interaction.
// 46th International Conference on Software Engineering. (ICSE24)
 
#ifndef Z3_EXAMPLE_INTERVAL_DOMAIN_H
#define Z3_EXAMPLE_INTERVAL_DOMAIN_H
 
#include "AE/Core/AbstractValue.h"
#include "AE/Core/IntervalValue.h"
#include "SVFIR/SVFVariables.h"
#include "Util/Z3Expr.h"
 
#include <iomanip>
 
namespace SVF
{
class AbstractState
{
    friend class SVFIR2AbsState;
    friend class RelationSolver;
public:
    typedef Map<u32_t, AbstractValue> VarToAbsValMap;
 
    typedef VarToAbsValMap AddrToAbsValMap;
 
public:
    AbstractState()
    {
    }
 
    AbstractState(VarToAbsValMap&_varToValMap, AddrToAbsValMap&_locToValMap) : _varToAbsVal(_varToValMap), _addrToAbsVal(_locToValMap) {}
 
    AbstractState(const AbstractState&rhs) : _varToAbsVal(rhs.getVarToVal()), _addrToAbsVal(rhs.getLocToVal())
    {
 
    }
 
    virtual ~AbstractState() = default;
 
    // getGepObjAddrs
    AddressValue getGepObjAddrs(u32_t pointer, IntervalValue offset);
 
    // initObjVar
    void initObjVar(ObjVar* objVar);
    // getElementIndex
    IntervalValue getElementIndex(const GepStmt* gep);
    // getByteOffset
    IntervalValue getByteOffset(const GepStmt* gep);
    // printAbstractState
    // loadValue
    AbstractValue loadValue(NodeID varId);
    // storeValue
    void storeValue(NodeID varId, AbstractValue val);
 
    u32_t getAllocaInstByteSize(const AddrStmt *addr);
 
 
    static inline u32_t getVirtualMemAddress(u32_t idx)
    {
        return AddressValue::getVirtualMemAddress(idx);
    }
 
    static inline bool isVirtualMemAddress(u32_t val)
    {
        return AddressValue::isVirtualMemAddress(val);
    }
 
    static inline u32_t getInternalID(u32_t idx)
    {
        return AddressValue::getInternalID(idx);
    }
 
    static inline bool isNullPtr(u32_t addr)
    {
        return getInternalID(addr) == 0;
    }
 
    AbstractState&operator=(const AbstractState&rhs)
    {
        if (rhs != *this)
        {
            _varToAbsVal = rhs._varToAbsVal;
            _addrToAbsVal = rhs._addrToAbsVal;
        }
        return *this;
    }
 
    AbstractState(AbstractState&&rhs) : _varToAbsVal(std::move(rhs._varToAbsVal)),
        _addrToAbsVal(std::move(rhs._addrToAbsVal))
    {
 
    }
 
    AbstractState&operator=(AbstractState&&rhs)
    {
        if (&rhs != this)
        {
            _varToAbsVal = std::move(rhs._varToAbsVal);
            _addrToAbsVal = std::move(rhs._addrToAbsVal);
        }
        return *this;
    }
 
    AbstractState bottom() const
    {
        AbstractState inv = *this;
        for (auto &item: inv._varToAbsVal)
        {
            if (item.second.isInterval())
                item.second.getInterval().set_to_bottom();
        }
        return inv;
    }
 
    AbstractState top() const
    {
        AbstractState inv = *this;
        for (auto &item: inv._varToAbsVal)
        {
            if (item.second.isInterval())
                item.second.getInterval().set_to_top();
        }
        return inv;
    }
 
    AbstractState sliceState(Set<u32_t> &sl)
    {
        AbstractState inv;
        for (u32_t id: sl)
        {
            inv._varToAbsVal[id] = _varToAbsVal[id];
        }
        return inv;
    }
 
protected:
    VarToAbsValMap _varToAbsVal; 
    AddrToAbsValMap
    _addrToAbsVal; 
 
public:
 
 
    inline virtual AbstractValue &operator[](u32_t varId)
    {
        return _varToAbsVal[varId];
    }
 
    inline virtual const AbstractValue &operator[](u32_t varId) const
    {
        return _varToAbsVal.at(varId);
    }
 
    inline bool inVarToAddrsTable(u32_t id) const
    {
        if (_varToAbsVal.find(id)!= _varToAbsVal.end())
        {
            if (_varToAbsVal.at(id).isAddr())
            {
                return true;
            }
        }
        return false;
    }
 
    inline virtual bool inVarToValTable(u32_t id) const
    {
        if (_varToAbsVal.find(id) != _varToAbsVal.end())
        {
            if (_varToAbsVal.at(id).isInterval())
            {
                return true;
            }
        }
        return false;
    }
 
    inline bool inAddrToAddrsTable(u32_t id) const
    {
        if (_addrToAbsVal.find(id)!= _addrToAbsVal.end())
        {
            if (_addrToAbsVal.at(id).isAddr())
            {
                return true;
            }
        }
        return false;
    }
 
    inline virtual bool inAddrToValTable(u32_t id) const
    {
        if (_addrToAbsVal.find(id) != _addrToAbsVal.end())
        {
            if (_addrToAbsVal.at(id).isInterval())
            {
                return true;
            }
        }
        return false;
    }
 
    const VarToAbsValMap&getVarToVal() const
    {
        return _varToAbsVal;
    }
 
    const AddrToAbsValMap&getLocToVal() const
    {
        return _addrToAbsVal;
    }
 
public:
 
    AbstractState widening(const AbstractState&other);
 
    AbstractState narrowing(const AbstractState&other);
 
    void joinWith(const AbstractState&other);
 
 
    void meetWith(const AbstractState&other);
 
    const SVFType* getPointeeElement(NodeID id);
 
 
    u32_t hash() const;
 
public:
    inline void store(u32_t addr, const AbstractValue &val)
    {
        assert(isVirtualMemAddress(addr) && "not virtual address?");
        if (isNullPtr(addr)) return;
        u32_t objId = getInternalID(addr);
        _addrToAbsVal[objId] = val;
    }
 
    inline virtual AbstractValue &load(u32_t addr)
    {
        assert(isVirtualMemAddress(addr) && "not virtual address?");
        u32_t objId = getInternalID(addr);
        return _addrToAbsVal[objId];
 
    }
 
 
    void printAbstractState() const;
 
    std::string toString() const
    {
        return "";
    }
 
    bool equals(const AbstractState&other) const;
 
 
    static bool eqVarToValMap(const VarToAbsValMap&lhs, const VarToAbsValMap&rhs)
    {
        if (lhs.size() != rhs.size()) return false;
        for (const auto &item: lhs)
        {
            auto it = rhs.find(item.first);
            if (it == rhs.end())
                return false;
            if (!item.second.equals(it->second))
                return false;
            else
            {
            }
        }
        return true;
    }
 
    static bool lessThanVarToValMap(const VarToAbsValMap&lhs, const VarToAbsValMap&rhs)
    {
        if (lhs.empty()) return !rhs.empty();
        for (const auto &item: lhs)
        {
            auto it = rhs.find(item.first);
            if (it == rhs.end()) return false;
            // judge from expr id
            if (item.second.getInterval().contain(it->second.getInterval())) return false;
        }
        return true;
    }
 
    // lhs >= rhs
    static bool geqVarToValMap(const VarToAbsValMap&lhs, const VarToAbsValMap&rhs)
    {
        if (rhs.empty()) return true;
        for (const auto &item: rhs)
        {
            auto it = lhs.find(item.first);
            if (it == lhs.end()) return false;
            // judge from expr id
            if (!it->second.getInterval().contain(
                        item.second.getInterval()))
                return false;
 
        }
        return true;
    }
 
    bool operator==(const AbstractState&rhs) const
    {
        return  eqVarToValMap(_varToAbsVal, rhs.getVarToVal()) &&
                eqVarToValMap(_addrToAbsVal, rhs.getLocToVal());
    }
 
    bool operator!=(const AbstractState&rhs) const
    {
        return !(*this == rhs);
    }
 
    bool operator<(const AbstractState&rhs) const
    {
        return !(*this >= rhs);
    }
 
 
    bool operator>=(const AbstractState&rhs) const
    {
        return geqVarToValMap(_varToAbsVal, rhs.getVarToVal()) && geqVarToValMap(_addrToAbsVal, rhs.getLocToVal());
    }
 
    void clear()
    {
        _addrToAbsVal.clear();
        _varToAbsVal.clear();
    }
 
};
 
}
 
 
#endif //Z3_EXAMPLE_INTERVAL_DOMAIN_H