1#ifndef ROSE_BinaryAnalysis_ModelChecker_ExternalFunctionUnit_H
2#define ROSE_BinaryAnalysis_ModelChecker_ExternalFunctionUnit_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_MODEL_CHECKER
6#include <Rose/BinaryAnalysis/ConcreteLocation.h>
7#include <Rose/BinaryAnalysis/ModelChecker/ExecutionUnit.h>
8#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
11namespace BinaryAnalysis {
12namespace ModelChecker {
20class ExternalFunctionUnit:
public ExecutionUnit {
22 using Ptr = ExternalFunctionUnitPtr;
25 Partitioner2::FunctionPtr function_;
28 ExternalFunctionUnit() =
delete;
29 ExternalFunctionUnit(
const Partitioner2::FunctionPtr&,
const SourceLocation&);
31 ~ExternalFunctionUnit();
39 static Ptr instance(
const Partitioner2::FunctionPtr&,
const SourceLocation&);
48 Partitioner2::FunctionPtr function()
const;
51 virtual std::string printableName()
const override;
52 virtual void printSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
53 size_t stepOrigin,
size_t maxSteps)
const override;
54 virtual void toYamlHeader(
const SettingsPtr&, std::ostream&,
const std::string &prefix)
const override;
55 virtual void toYamlSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
56 size_t stepOrigin,
size_t maxSteps)
const override;
57 virtual std::vector<Sarif::LocationPtr> toSarif(
size_t maxSteps)
const override;
58 virtual size_t nSteps()
const override;
60 virtual std::vector<TagPtr> execute(
const SettingsPtr&,
const SemanticCallbacksPtr&,
61 const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&)
override;
65 InstructionSemantics::BaseSemantics::SValuePtr
66 readLocation(
const InstructionSemantics::BaseSemantics::DispatcherPtr&,
const ConcreteLocation&,
67 const InstructionSemantics::BaseSemantics::SValuePtr &dfltValue);
71 writeLocation(
const InstructionSemantics::BaseSemantics::DispatcherPtr&,
const ConcreteLocation&,
72 const InstructionSemantics::BaseSemantics::SValuePtr &value);
75 void clearReturnValues(
const InstructionSemantics::BaseSemantics::DispatcherPtr&);
78 void simulateReturn(
const InstructionSemantics::BaseSemantics::DispatcherPtr&);
Holds a value or nothing.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.