ROSE 0.11.145.317
PartitionerModel.h
1#ifndef ROSE_BinaryAnalysis_ModelChecker_PartitionerModel_H
2#define ROSE_BinaryAnalysis_ModelChecker_PartitionerModel_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_MODEL_CHECKER
5
6#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
7#include <Rose/BinaryAnalysis/ModelChecker/SemanticCallbacks.h>
8#include <Rose/BinaryAnalysis/ModelChecker/Variables.h>
9#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
10#include <Rose/BinaryAnalysis/Variables.h>
11
12#include <Sawyer/CommandLine.h>
13#include <Sawyer/Stack.h>
14
15namespace Rose {
16namespace BinaryAnalysis {
17namespace ModelChecker {
18
27namespace PartitionerModel {
28
30// Settings for this model checker
32
34struct Settings {
36 enum class MemoryType {
37 LIST,
38 MAP
39 };
40
41 TestMode nullRead = TestMode::MUST;
42 TestMode nullWrite = TestMode::MUST;
43 TestMode oobRead = TestMode::OFF;
44 TestMode oobWrite = TestMode::OFF;
45 TestMode uninitVar = TestMode::OFF;
46 Address maxNullAddress = 4095;
47 bool debugNull = false;
48 Sawyer::Optional<Address> initialStackVa;
49 MemoryType memoryType = MemoryType::MAP;
50 bool solverMemoization = false;
51 bool traceSemantics = false;
52};
53
54class SemanticCallbacks;
55
59void commandLineDebugSwitches(Sawyer::CommandLine::SwitchGroup&, Settings&);
60
65Sawyer::CommandLine::SwitchGroup commandLineModelSwitches(Settings&);
66
72
74// Function call stack
76
78class FunctionCall {
79 Partitioner2::FunctionPtr function_;
80 Address initialStackPointer_ = 0;
81 Address framePointerDelta_ = (Address)(-4); // Normal frame pointer w.r.t. initial stack pointer
82 Sawyer::Optional<Address> returnAddress_;
83 Variables::StackVariables stackVariables_;
84
85public:
86 ~FunctionCall();
87 FunctionCall(const Partitioner2::FunctionPtr&, Address initialSp, Sawyer::Optional<Address> returnAddress,
88 const Variables::StackVariables&);
89
91 Partitioner2::FunctionPtr function() const;
92
96 Address initialStackPointer() const;
97
99 const Variables::StackVariables& stackVariables() const;
100
106 Address framePointerDelta() const;
107 void framePointerDelta(Address);
113 Address framePointer(size_t nBits) const;
114
118 Sawyer::Optional<Address> returnAddress() const;
119 void returnAddress(Sawyer::Optional<Address>);
123 std::string printableName(size_t nBits) const;
124};
125
129using FunctionCallStack = Sawyer::Container::Stack<FunctionCall>;
130
132// Instruction semantics value
134
138class SValue: public InstructionSemantics::SymbolicSemantics::SValue {
139public:
141 using Super = InstructionSemantics::SymbolicSemantics::SValue;
142
144 using Ptr = SValuePtr;
145
146private:
147 AddressInterval region_;
148
149#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
150private:
151 friend class boost::serialization::access;
152
153 template<class S>
154 void serialize(S &s, const unsigned /*version*/) {
155 s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
156 s & BOOST_SERIALIZATION_NVP(region_);
157 }
158#endif
159
160public:
161 ~SValue();
162
163protected:
164 SValue();
165
166 SValue(size_t nBits, uint64_t number);
167
168 explicit SValue(const SymbolicExpression::Ptr&);
169
170public:
174 static Ptr instance();
175
177 static Ptr instanceBottom(size_t nBits);
178
180 static Ptr instanceUndefined(size_t nBits);
181
183 static Ptr instanceUnspecified(size_t nBits);
184
186 static Ptr instanceInteger(size_t nBits, uint64_t value);
187
189 static Ptr instanceSymbolic(const SymbolicExpression::Ptr &value);
190
191public:
192 virtual InstructionSemantics::BaseSemantics::SValuePtr bottom_(size_t nBits) const override;
193 virtual InstructionSemantics::BaseSemantics::SValuePtr undefined_(size_t nBits) const override;
194 virtual InstructionSemantics::BaseSemantics::SValuePtr unspecified_(size_t nBits) const override;
195 virtual InstructionSemantics::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) const override;
196 virtual InstructionSemantics::BaseSemantics::SValuePtr boolean_(bool value) const override;
197 virtual InstructionSemantics::BaseSemantics::SValuePtr copy(size_t newNBits = 0) const override;
198
200 createOptionalMerge(const InstructionSemantics::BaseSemantics::SValuePtr &other,
201 const InstructionSemantics::BaseSemantics::MergerPtr&,
202 const SmtSolverPtr&) const override;
203
204public:
208 static Ptr promote(const InstructionSemantics::BaseSemantics::SValuePtr&);
209
210public:
217 AddressInterval region() const;
218 void region(const AddressInterval&);
221public:
222 virtual void print(std::ostream&, InstructionSemantics::BaseSemantics::Formatter&) const override;
223 virtual void hash(Combinatorics::Hasher&) const override;
224};
225
227// Instruction semantics state
229
231using StatePtr = boost::shared_ptr<class State>;
232
234class State: public InstructionSemantics::SymbolicSemantics::State {
235public:
237 using Super = InstructionSemantics::SymbolicSemantics::State;
238
240 using Ptr = StatePtr;
241
242private:
243 FunctionCallStack callStack_;
244
245protected:
246 State();
247 State(const InstructionSemantics::BaseSemantics::RegisterStatePtr&,
248 const InstructionSemantics::BaseSemantics::MemoryStatePtr&);
249
250 // Deep copy
251 State(const State&);
252
253public:
255 static Ptr instance(const InstructionSemantics::BaseSemantics::RegisterStatePtr&,
256 const InstructionSemantics::BaseSemantics::MemoryStatePtr&);
257
259 static Ptr instance(const StatePtr&);
260
262 virtual InstructionSemantics::BaseSemantics::StatePtr
263 create(const InstructionSemantics::BaseSemantics::RegisterStatePtr&,
264 const InstructionSemantics::BaseSemantics::MemoryStatePtr&) const override;
265
267 virtual InstructionSemantics::BaseSemantics::StatePtr clone() const override;
268
270 static Ptr promote(const InstructionSemantics::BaseSemantics::StatePtr&);
271
272public:
278 const FunctionCallStack& callStack() const;
279 FunctionCallStack& callStack();
281};
282
284// Instruction semantics domain
286
288class RiscOperators: public InstructionSemantics::SymbolicSemantics::RiscOperators {
289public:
290 using Super = InstructionSemantics::SymbolicSemantics::RiscOperators;
291
292 using Ptr = RiscOperatorsPtr;
293
294private:
295 const Settings settings_;
296 Partitioner2::PartitionerConstPtr partitioner_; // not null
297 SmtSolver::Ptr modelCheckerSolver_; // solver used for model checking, different than RISC operators
298 size_t nInstructions_ = 0;
299 SemanticCallbacks *semantics_ = nullptr;
300 AddressInterval stackLimits_; // where the stack can exist in memory
301 bool computeMemoryRegions_ = false; // compute memory regions. This is needed for OOB analysis.
302 const Variables::GlobalVariables &gvars_;
303
304 mutable SAWYER_THREAD_TRAITS::Mutex variableFinderMutex_; // protects the following data members
305 Variables::VariableFinderPtr variableFinder_unsync; // shared by all RiscOperator objects
306
307protected:
308 RiscOperators(const Settings&, const Partitioner2::PartitionerConstPtr&, ModelChecker::SemanticCallbacks*,
309 const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr&,
310 const Variables::VariableFinderPtr&, const Variables::GlobalVariables&);
311
312 RiscOperators(
313 const RiscOperators &, const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &
314 );
315
316public: // Standard public construction-like functions
317 ~RiscOperators();
318
319 static Ptr instance(const Settings&, const Partitioner2::PartitionerConstPtr&, ModelChecker::SemanticCallbacks*,
320 const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr&,
321 const Variables::VariableFinderPtr&, const Variables::GlobalVariables&);
322
323 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
324 create(const InstructionSemantics::BaseSemantics::SValuePtr&, const SmtSolverPtr&) const override;
325
326 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
327 create(const InstructionSemantics::BaseSemantics::StatePtr&, const SmtSolverPtr&) const override;
328
329 static Ptr promote(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &x);
330
331public: // Supporting functions
335 Partitioner2::PartitionerConstPtr partitioner() const;
336
343 SmtSolver::Ptr modelCheckerSolver() const;
344 void modelCheckerSolver(const SmtSolver::Ptr&);
350 SemanticCallbacks* semanticCallbacks() const;
351
357 bool computeMemoryRegions() const;
358 void computeMemoryRegions(bool);
368 void checkNullAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode);
369
373 void checkOobAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode, size_t nBytes);
374
378 void checkUninitVar(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, size_t nBytes);
379
386 size_t nInstructions() const;
387 void nInstructions(size_t);
391 void maybeInitCallStack(Address insnVa);
392
394 void pushCallStack(const Partitioner2::FunctionPtr &callee, Address initialSp, Sawyer::Optional<Address> returnVa);
395
400 void popCallStack();
401
408 size_t pruneCallStack();
409
411 void printCallStack(std::ostream&, const std::string &prefix);
412
427 InstructionSemantics::BaseSemantics::SValuePtr
428 assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result);
429
430 InstructionSemantics::BaseSemantics::SValuePtr
431 assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result,
432 const InstructionSemantics::BaseSemantics::SValuePtr &a);
433
434 InstructionSemantics::BaseSemantics::SValuePtr
435 assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result,
436 const InstructionSemantics::BaseSemantics::SValuePtr &a,
437 const InstructionSemantics::BaseSemantics::SValuePtr &b);
440public: // Override RISC operations
441 virtual void finishInstruction(SgAsmInstruction*) override;
442
443 virtual InstructionSemantics::BaseSemantics::SValuePtr
444 number_(size_t nBits, uint64_t value) override;
445
446 virtual InstructionSemantics::BaseSemantics::SValuePtr
447 extract(const InstructionSemantics::BaseSemantics::SValuePtr&, size_t begin, size_t end) override;
448
449 virtual InstructionSemantics::BaseSemantics::SValuePtr
450 concat(const InstructionSemantics::BaseSemantics::SValuePtr &lowBits,
451 const InstructionSemantics::BaseSemantics::SValuePtr &highBits) override;
452
453 virtual InstructionSemantics::BaseSemantics::SValuePtr
454 shiftLeft(const InstructionSemantics::BaseSemantics::SValuePtr &a,
455 const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override;
456
457 virtual InstructionSemantics::BaseSemantics::SValuePtr
458 shiftRight(const InstructionSemantics::BaseSemantics::SValuePtr &a,
459 const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override;
460
461 virtual InstructionSemantics::BaseSemantics::SValuePtr
462 shiftRightArithmetic(const InstructionSemantics::BaseSemantics::SValuePtr &a,
463 const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override;
464
465 virtual InstructionSemantics::BaseSemantics::SValuePtr
466 unsignedExtend(const InstructionSemantics::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
467
468 virtual InstructionSemantics::BaseSemantics::SValuePtr
469 signExtend(const InstructionSemantics::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
470
471 virtual InstructionSemantics::BaseSemantics::SValuePtr
472 add(const InstructionSemantics::BaseSemantics::SValuePtr &a,
473 const InstructionSemantics::BaseSemantics::SValuePtr &b) override;
474
475 virtual InstructionSemantics::BaseSemantics::SValuePtr
476 addCarry(const InstructionSemantics::BaseSemantics::SValuePtr &a,
477 const InstructionSemantics::BaseSemantics::SValuePtr &b,
478 InstructionSemantics::BaseSemantics::SValuePtr &carryOut /*out*/,
479 InstructionSemantics::BaseSemantics::SValuePtr &overflowed /*out*/) override;
480
481 virtual InstructionSemantics::BaseSemantics::SValuePtr
482 subtract(const InstructionSemantics::BaseSemantics::SValuePtr &a,
483 const InstructionSemantics::BaseSemantics::SValuePtr &b) override;
484
485 virtual InstructionSemantics::BaseSemantics::SValuePtr
486 subtractCarry(const InstructionSemantics::BaseSemantics::SValuePtr &a,
487 const InstructionSemantics::BaseSemantics::SValuePtr &b,
488 InstructionSemantics::BaseSemantics::SValuePtr &carryOut /*out*/,
489 InstructionSemantics::BaseSemantics::SValuePtr &overflowed /*out*/) override;
490
491 virtual InstructionSemantics::BaseSemantics::SValuePtr
492 addWithCarries(const InstructionSemantics::BaseSemantics::SValuePtr &a,
493 const InstructionSemantics::BaseSemantics::SValuePtr &b,
494 const InstructionSemantics::BaseSemantics::SValuePtr &c,
495 InstructionSemantics::BaseSemantics::SValuePtr &carryOut /*out*/) override;
496
497 virtual InstructionSemantics::BaseSemantics::SValuePtr
498 readRegister(RegisterDescriptor, const InstructionSemantics::BaseSemantics::SValuePtr&) override;
499
500 virtual void
501 writeRegister(RegisterDescriptor, const InstructionSemantics::BaseSemantics::SValuePtr&) override;
502
503 virtual InstructionSemantics::BaseSemantics::SValuePtr
504 readMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr,
505 const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
506 const InstructionSemantics::BaseSemantics::SValuePtr &cond) override;
507
508 virtual void
509 writeMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr,
510 const InstructionSemantics::BaseSemantics::SValuePtr &value,
511 const InstructionSemantics::BaseSemantics::SValuePtr &cond) override;
512};
513
515// High-level semantic operations
517
519class SemanticCallbacks: public Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks {
520public:
521 using Ptr = SemanticCallbacksPtr;
523
524private:
525 Settings settings_; // settings are set by the constructor and not modified thereafter
526 Partitioner2::PartitionerConstPtr partitioner_; // generally shouldn't be changed once model checking starts, non-null
527 SmtSolver::Memoizer::Ptr smtMemoizer_; // memoizer shared among all solvers
528 AddressInterval stackRegion_; // addresses considered to be in the stack's area of memory
529
530 mutable SAWYER_THREAD_TRAITS::Mutex unitsMutex_; // protects only the units_ data member
531 Sawyer::Container::Map<Address, ExecutionUnitPtr> units_; // cached execution units
532
533 mutable SAWYER_THREAD_TRAITS::Mutex mutex_; // protects the following data members
534 std::set<uint64_t> seenStates_; // states we've seen, by hash
535 size_t nDuplicateStates_ = 0; // number of times a previous state is seen again
536 size_t nSolverFailures_ = 0; // number of times the SMT solver failed
537 UnitCounts unitsReached_; // number of times basic blocks were reached
538 Variables::VariableFinderPtr variableFinder_; // also shared by all RiscOperator objects
539 Variables::GlobalVariables gvars_; // all global variables identified by variableFinder_
540
541 // This model is able to follow a single path specified by the user. In order to do that, the user should call
542 // followOnePath to provide the ordered list of execution units. The nextCodeAddresses function is overridden to
543 // return only the address of the next execution unit in this list, or none when the list is empty. The findUnit
544 // function is enhanced to return the next execution unit and remove it from the list.
545 //
546 // These are also protected by mutex_
547 bool followingOnePath_ = false;
548 std::list<ExecutionUnitPtr> onePath_; // execution units yet to be consumed by findUnit
549
550protected:
551 SemanticCallbacks(const ModelChecker::SettingsPtr&, const Settings&, const Partitioner2::PartitionerConstPtr&);
552public:
553 ~SemanticCallbacks();
554
555public:
556 static Ptr instance(const ModelChecker::SettingsPtr&, const Settings&, const Partitioner2::PartitionerConstPtr&);
557
558public:
560 Partitioner2::PartitionerConstPtr partitioner() const;
561
562public:
564 const Settings& p2Settings() const;
565
581 void followOnePath(const std::list<ExecutionUnitPtr>&);
582
594 bool followingOnePath() const;
595 void followingOnePath(bool);
605 SmtSolver::Memoizer::Ptr smtMemoizer() const;
606 void smtMemoizer(const SmtSolver::Memoizer::Ptr&);
612 AddressInterval stackRegion() const;
613
621 size_t nDuplicateStates() const;
622
630 size_t nSolverFailures() const;
631
640 size_t nUnitsReached() const;
641
648 UnitCounts unitsReached() const;
649
657 virtual bool filterNullDeref(const InstructionSemantics::BaseSemantics::SValuePtr &addr, SgAsmInstruction*,
658 TestMode testMode, IoMode ioMode);
659
675 virtual bool filterOobAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
676 const AddressInterval &referencedRegion, const AddressInterval &accessedRegion,
677 SgAsmInstruction *insn, TestMode testMode, IoMode ioMode,
678 const FoundVariable &intendedVariable, const FoundVariable &accessedVariable);
679
680 virtual bool filterUninitVar(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
681 const AddressInterval &referencedREgion, const AddressInterval &accessedRegion,
682 SgAsmInstruction *insn, TestMode testMode, const FoundVariable &accessedVariable);
683
684public:
685 virtual void reset() override;
686
687 virtual InstructionSemantics::BaseSemantics::SValuePtr protoval() override;
688
689 virtual InstructionSemantics::BaseSemantics::RegisterStatePtr createInitialRegisters() override;
690
691 virtual InstructionSemantics::BaseSemantics::MemoryStatePtr createInitialMemory() override;
692
693 virtual InstructionSemantics::BaseSemantics::StatePtr createInitialState() override;
694
695 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr createRiscOperators() override;
696
697 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
698 configureRiscOperators(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
699
700 virtual void
701 initializeState(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
702
703 virtual InstructionSemantics::BaseSemantics::DispatcherPtr
704 createDispatcher(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
705
706 virtual SmtSolver::Ptr createSolver() override;
707
708 virtual void attachModelCheckerSolver(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
709 const SmtSolver::Ptr&) override;
710
711 virtual CodeAddresses
712 nextCodeAddresses(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
713
714 virtual std::vector<TagPtr>
715 preExecute(const PathNodePtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
716
717 virtual std::vector<TagPtr>
718 postExecute(const PathNodePtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
719
720 virtual InstructionSemantics::BaseSemantics::SValuePtr
721 instructionPointer(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
722
723 virtual std::vector<NextUnit>
724 nextUnits(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&) override;
725
726#ifdef ROSE_HAVE_YAMLCPP
727 virtual std::list<ExecutionUnitPtr>
728 parsePath(const YAML::Node&, const std::string &sourceName) override;
729#endif
730
731 virtual std::list<ExecutionUnitPtr>
732 parsePath(const Yaml::Node&, const std::string &sourceName) override;
733
734protected:
735 Variables::VariableFinderPtr variableFinder() const;
736 Variables::GlobalVariables& globalVariables();
737
738private:
739 // Records the state hash and returns true if we've seen it before.
740 bool seenState(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
741
742 // Find and cache the execution unit at the specified address.
743 ExecutionUnitPtr findUnit(Address va, const Progress::Ptr&);
744};
745
746} // namespace
747} // namespace
748} // namespace
749} // namespace
750
751#endif
752#endif
A collection of related switch declarations.
Container associating values with keys.
Definition Sawyer/Map.h:72
Stack-based container.
Definition Stack.h:22
Holds a value or nothing.
Definition Optional.h:54
Base class for machine instructions.
T shiftRightArithmetic(T value, size_t count)
Shifts bits of value right by count bits with sign extension.
Definition integerOps.h:131
T extract(T bits)
Extract bits from a value.
Definition integerOps.h:255
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to concrete RISC operations.
Sawyer::SharedPointer< class SValue > SValuePtr
Smart-ownership pointer to a concrete semantic value.
Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &)
Define command-line switches.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
Hash hash(const std::vector< Ptr > &)
Hash zero or more expressions.
void print(const GlobalVariables &, const Partitioner2::PartitionerConstPtr &, std::ostream &out, const std::string &prefix="")
Print info about multiple global variables.
std::uint64_t Address
Address.
Definition Address.h:11
Sawyer::Container::Interval< Address > AddressInterval
An interval of addresses.
Unsigned shiftRight(Unsigned src, size_t n, bool b=false)
Right shift a value.
Definition BitOps.h:125
Unsigned signExtend(Unsigned src, size_t n)
Sign extend part of a value to the full width of the src type.
Definition BitOps.h:324
Unsigned shiftLeft(Unsigned src, size_t n, bool b=false)
Left shift a value.
Definition BitOps.h:91
void serialize(std::ostream &output, Graph &graph)
Serialize a graph into a stream of bytes.
The ROSE library.
void copy(const Word *src, const BitRange &srcRange, Word *dst, const BitRange &dstRange)
Copy some bits.
const char * MemoryType(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::PartitionerModel::Settings::MemoryType enum constant to a...
const char * TestMode(int64_t)
Convert Rose::BinaryAnalysis::ModelChecker::TestMode enum constant to a string.