ROSE 0.11.145.147
ExternalFunctionUnit.h
1#ifndef ROSE_BinaryAnalysis_ModelChecker_ExternalFunctionUnit_H
2#define ROSE_BinaryAnalysis_ModelChecker_ExternalFunctionUnit_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_MODEL_CHECKER
5
6#include <Rose/BinaryAnalysis/ConcreteLocation.h>
7#include <Rose/BinaryAnalysis/ModelChecker/ExecutionUnit.h>
8#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
9
10namespace Rose {
11namespace BinaryAnalysis {
12namespace ModelChecker {
13
20class ExternalFunctionUnit: public ExecutionUnit {
21public:
22 using Ptr = ExternalFunctionUnitPtr;
23
24private:
25 Partitioner2::FunctionPtr function_;
26
27protected:
28 ExternalFunctionUnit() = delete;
29 ExternalFunctionUnit(const Partitioner2::FunctionPtr&, const SourceLocation&);
30public:
31 ~ExternalFunctionUnit();
32
33public:
39 static Ptr instance(const Partitioner2::FunctionPtr&, const SourceLocation&);
40
41public:
48 Partitioner2::FunctionPtr function() const;
49
50public:
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;
59 virtual Sawyer::Optional<rose_addr_t> address() const override;
60 virtual std::vector<TagPtr> execute(const SettingsPtr&, const SemanticCallbacksPtr&,
61 const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
62
63private:
64 // Read a calling convention parameter location
65 InstructionSemantics::BaseSemantics::SValuePtr
66 readLocation(const InstructionSemantics::BaseSemantics::DispatcherPtr&, const ConcreteLocation&,
67 const InstructionSemantics::BaseSemantics::SValuePtr &dfltValue);
68
69 // Write to a calling convention parameter location
70 void
71 writeLocation(const InstructionSemantics::BaseSemantics::DispatcherPtr&, const ConcreteLocation&,
72 const InstructionSemantics::BaseSemantics::SValuePtr &value);
73
74 // Set function return values to free variables
75 void clearReturnValues(const InstructionSemantics::BaseSemantics::DispatcherPtr&);
76
77 // Simulate a function return
78 void simulateReturn(const InstructionSemantics::BaseSemantics::DispatcherPtr&);
79};
80
81
82} // namespace
83} // namespace
84} // namespace
85
86#endif
87#endif
Holds a value or nothing.
Definition Optional.h:56
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
The ROSE library.