aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SymbolicVariables.h
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-10-22 16:29:03 +0800
committerLeonardo Alt <leo@ethereum.org>2018-10-25 15:30:48 +0800
commitd8cbf321dafbe85f6fde07b5dd4ce7a3abffaeb6 (patch)
treee8d160211b6db84307670e86982171e7ac1f8d2d /libsolidity/formal/SymbolicVariables.h
parent01566c2e1af5b7f655fd593e5e1019e103d739a0 (diff)
downloaddexon-solidity-d8cbf321dafbe85f6fde07b5dd4ce7a3abffaeb6.tar.gz
dexon-solidity-d8cbf321dafbe85f6fde07b5dd4ce7a3abffaeb6.tar.zst
dexon-solidity-d8cbf321dafbe85f6fde07b5dd4ce7a3abffaeb6.zip
Grouping of symbolic variables in the same file and support to FixedBytes
Diffstat (limited to 'libsolidity/formal/SymbolicVariables.h')
-rw-r--r--libsolidity/formal/SymbolicVariables.h149
1 files changed, 149 insertions, 0 deletions
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
new file mode 100644
index 00000000..4fd9b245
--- /dev/null
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -0,0 +1,149 @@
+/*
+ This file is part of solidity.
+
+ solidity is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
+
+ solidity 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 General Public License for more details.
+
+ You should have received a copy of the GNU General Public License
+ along with solidity. If not, see <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/formal/SSAVariable.h>
+
+#include <libsolidity/formal/SolverInterface.h>
+
+#include <libsolidity/ast/Types.h>
+
+#include <memory>
+
+namespace dev
+{
+namespace solidity
+{
+
+class Type;
+
+/**
+ * This abstract class represents the symbolic version of a program variable.
+ */
+class SymbolicVariable
+{
+public:
+ SymbolicVariable(
+ TypePointer _type,
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+
+ virtual ~SymbolicVariable() = default;
+
+ smt::Expression currentValue() const
+ {
+ return valueAtIndex(m_ssa->index());
+ }
+
+ virtual smt::Expression valueAtIndex(int _index) const = 0;
+
+ smt::Expression increaseIndex()
+ {
+ ++(*m_ssa);
+ return currentValue();
+ }
+
+ unsigned index() const { return m_ssa->index(); }
+ unsigned& index() { return m_ssa->index(); }
+
+ /// Sets the var to the default value of its type.
+ /// Inherited types must implement.
+ virtual void setZeroValue() = 0;
+ /// The unknown value is the full range of valid values.
+ /// It is sub-type dependent, but not mandatory.
+ virtual void setUnknownValue() {}
+
+protected:
+ std::string uniqueSymbol(unsigned _index) const;
+
+ TypePointer m_type = nullptr;
+ std::string m_uniqueName;
+ smt::SolverInterface& m_interface;
+ std::shared_ptr<SSAVariable> m_ssa = nullptr;
+};
+
+/**
+ * Specialization of SymbolicVariable for Bool
+ */
+class SymbolicBoolVariable: public SymbolicVariable
+{
+public:
+ SymbolicBoolVariable(
+ TypePointer _type,
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+
+ /// Sets the var to false.
+ void setZeroValue();
+ /// Does nothing since the SMT solver already knows the valid values for Bool.
+ void setUnknownValue();
+
+protected:
+ smt::Expression valueAtIndex(int _index) const;
+};
+
+/**
+ * Specialization of SymbolicVariable for Integers
+ */
+class SymbolicIntVariable: public SymbolicVariable
+{
+public:
+ SymbolicIntVariable(
+ TypePointer _type,
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+
+ /// Sets the var to 0.
+ void setZeroValue();
+ /// Sets the variable to the full valid value range.
+ void setUnknownValue();
+
+protected:
+ smt::Expression valueAtIndex(int _index) const;
+};
+
+/**
+ * Specialization of SymbolicVariable for Address
+ */
+class SymbolicAddressVariable: public SymbolicIntVariable
+{
+public:
+ SymbolicAddressVariable(
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+};
+
+/**
+ * Specialization of SymbolicVariable for FixedBytes
+ */
+class SymbolicFixedBytesVariable: public SymbolicIntVariable
+{
+public:
+ SymbolicFixedBytesVariable(
+ unsigned _numBytes,
+ std::string const& _uniqueName,
+ smt::SolverInterface& _interface
+ );
+};
+
+}
+}