Skip to content

introduce goto_instruction_codet #6854

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 13, 2022
Merged

introduce goto_instruction_codet #6854

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
138 changes: 74 additions & 64 deletions src/goto-programs/goto_instruction_code.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,25 +13,30 @@ Author: Daniel Kroening, [email protected]
#include <util/std_code_base.h>
#include <util/std_expr.h>

/// A \ref codet representing an assignment in the program.
using goto_instruction_codet = codet;

/// A \ref goto_instruction_codet representing an assignment in the program.
/// For example, if an expression `e1` is represented as an \ref exprt `expr1`
/// and an expression `e2` is represented as an \ref exprt `expr2`, the
/// assignment `e1 = e2;` can be represented as `code_assignt(expr1, expr2)`.
class code_assignt : public codet
class code_assignt : public goto_instruction_codet
{
public:
code_assignt() : codet(ID_assign)
code_assignt() : goto_instruction_codet(ID_assign)
{
operands().resize(2);
}

code_assignt(exprt lhs, exprt rhs)
: codet(ID_assign, {std::move(lhs), std::move(rhs)})
: goto_instruction_codet(ID_assign, {std::move(lhs), std::move(rhs)})
{
}

code_assignt(exprt lhs, exprt rhs, source_locationt loc)
: codet(ID_assign, {std::move(lhs), std::move(rhs)}, std::move(loc))
: goto_instruction_codet(
ID_assign,
{std::move(lhs), std::move(rhs)},
std::move(loc))
{
}

Expand All @@ -56,15 +61,15 @@ class code_assignt : public codet
}

static void check(
const codet &code,
const goto_instruction_codet &code,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(
vm, code.operands().size() == 2, "assignment must have two operands");
}

static void validate(
const codet &code,
const goto_instruction_codet &code,
const namespacet &,
const validation_modet vm = validation_modet::INVARIANT)
{
Expand All @@ -77,7 +82,7 @@ class code_assignt : public codet
}

static void validate_full(
const codet &code,
const goto_instruction_codet &code,
const namespacet &ns,
const validation_modet vm = validation_modet::INVARIANT)
{
Expand All @@ -90,10 +95,10 @@ class code_assignt : public codet
}

protected:
using codet::op0;
using codet::op1;
using codet::op2;
using codet::op3;
using goto_instruction_codet::op0;
using goto_instruction_codet::op1;
using goto_instruction_codet::op2;
using goto_instruction_codet::op3;
};

template <>
Expand All @@ -107,26 +112,27 @@ inline void validate_expr(const code_assignt &x)
code_assignt::check(x);
}

inline const code_assignt &to_code_assign(const codet &code)
inline const code_assignt &to_code_assign(const goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_assign);
code_assignt::check(code);
return static_cast<const code_assignt &>(code);
}

inline code_assignt &to_code_assign(codet &code)
inline code_assignt &to_code_assign(goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_assign);
code_assignt::check(code);
return static_cast<code_assignt &>(code);
}

/// A \ref codet representing the removal of a local variable going out of
/// scope.
class code_deadt : public codet
/// A \ref goto_instruction_codet representing the removal of
/// a local variable going out of scope.
class code_deadt : public goto_instruction_codet
{
public:
explicit code_deadt(symbol_exprt symbol) : codet(ID_dead, {std::move(symbol)})
explicit code_deadt(symbol_exprt symbol)
: goto_instruction_codet(ID_dead, {std::move(symbol)})
{
}

Expand All @@ -146,7 +152,7 @@ class code_deadt : public codet
}

static void check(
const codet &code,
const goto_instruction_codet &code,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(
Expand All @@ -160,10 +166,10 @@ class code_deadt : public codet
}

protected:
using codet::op0;
using codet::op1;
using codet::op2;
using codet::op3;
using goto_instruction_codet::op0;
using goto_instruction_codet::op1;
using goto_instruction_codet::op2;
using goto_instruction_codet::op3;
};

template <>
Expand All @@ -177,28 +183,29 @@ inline void validate_expr(const code_deadt &x)
code_deadt::check(x);
}

inline const code_deadt &to_code_dead(const codet &code)
inline const code_deadt &to_code_dead(const goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_dead);
code_deadt::check(code);
return static_cast<const code_deadt &>(code);
}

inline code_deadt &to_code_dead(codet &code)
inline code_deadt &to_code_dead(goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_dead);
code_deadt::check(code);
return static_cast<code_deadt &>(code);
}

/// A `codet` representing the declaration of a local variable.
/// A `goto_instruction_codet` representing the declaration of a local variable.
/// For example, if a variable (symbol) `x` is represented as a
/// \ref symbol_exprt `sym`, then the declaration of this variable can be
/// represented as `code_declt(sym)`.
class code_declt : public codet
class code_declt : public goto_instruction_codet
{
public:
explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {std::move(symbol)})
explicit code_declt(symbol_exprt symbol)
: goto_instruction_codet(ID_decl, {std::move(symbol)})
{
}

Expand All @@ -218,7 +225,7 @@ class code_declt : public codet
}

static void check(
const codet &code,
const goto_instruction_codet &code,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(
Expand All @@ -242,30 +249,30 @@ inline void validate_expr(const code_declt &x)
code_declt::check(x);
}

inline const code_declt &to_code_decl(const codet &code)
inline const code_declt &to_code_decl(const goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_decl);
code_declt::check(code);
return static_cast<const code_declt &>(code);
}

inline code_declt &to_code_decl(codet &code)
inline code_declt &to_code_decl(goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_decl);
code_declt::check(code);
return static_cast<code_declt &>(code);
}

/// \ref codet representation of a function call statement.
/// \ref goto_instruction_codet representation of a function call statement.
/// The function call statement has three operands.
/// The first is the expression that is used to store the return value.
/// The second is the function called.
/// The third is a vector of argument values.
class code_function_callt : public codet
class code_function_callt : public goto_instruction_codet
{
public:
explicit code_function_callt(exprt _function)
: codet(
: goto_instruction_codet(
ID_function_call,
{nil_exprt(), std::move(_function), exprt(ID_arguments)})
{
Expand All @@ -274,7 +281,7 @@ class code_function_callt : public codet
typedef exprt::operandst argumentst;

code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
: codet(
: goto_instruction_codet(
ID_function_call,
{std::move(_lhs), std::move(_function), exprt(ID_arguments)})
{
Expand Down Expand Up @@ -318,7 +325,7 @@ class code_function_callt : public codet
}

static void check(
const codet &code,
const goto_instruction_codet &code,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(
Expand All @@ -330,7 +337,7 @@ class code_function_callt : public codet
}

static void validate(
const codet &code,
const goto_instruction_codet &code,
const namespacet &,
const validation_modet vm = validation_modet::INVARIANT)
{
Expand All @@ -344,7 +351,7 @@ class code_function_callt : public codet
}

static void validate_full(
const codet &code,
const goto_instruction_codet &code,
const namespacet &ns,
const validation_modet vm = validation_modet::INVARIANT)
{
Expand All @@ -357,10 +364,10 @@ class code_function_callt : public codet
}

protected:
using codet::op0;
using codet::op1;
using codet::op2;
using codet::op3;
using goto_instruction_codet::op0;
using goto_instruction_codet::op1;
using goto_instruction_codet::op2;
using goto_instruction_codet::op3;
};

template <>
Expand All @@ -374,29 +381,30 @@ inline void validate_expr(const code_function_callt &x)
code_function_callt::check(x);
}

inline const code_function_callt &to_code_function_call(const codet &code)
inline const code_function_callt &
to_code_function_call(const goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_function_call);
code_function_callt::check(code);
return static_cast<const code_function_callt &>(code);
}

inline code_function_callt &to_code_function_call(codet &code)
inline code_function_callt &to_code_function_call(goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_function_call);
code_function_callt::check(code);
return static_cast<code_function_callt &>(code);
}

/// A `codet` representing the declaration that an input of a particular
/// description has a value which corresponds to the value of a given expression
/// (or expressions).
/// A `goto_instruction_codet` representing the declaration that an input of
/// a particular description has a value which corresponds to the value of a
/// given expression (or expressions).
/// When working with the C front end, calls to the `__CPROVER_input` intrinsic
/// can be added to the input code in order add instructions of this type to the
/// goto program.
/// The first argument is expected to be a C string denoting the input
/// identifier. The second argument is the expression for the input value.
class code_inputt : public codet
class code_inputt : public goto_instruction_codet
{
public:
/// This constructor is for support of calls to `__CPROVER_input` in user
Expand All @@ -420,7 +428,7 @@ class code_inputt : public codet
optionalt<source_locationt> location = {});

static void check(
const codet &code,
const goto_instruction_codet &code,
const validation_modet vm = validation_modet::INVARIANT);
};

Expand All @@ -435,15 +443,15 @@ inline void validate_expr(const code_inputt &input)
code_inputt::check(input);
}

/// A `codet` representing the declaration that an output of a particular
/// description has a value which corresponds to the value of a given expression
/// (or expressions).
/// A `goto_instruction_codet` representing the declaration that an output of
/// a particular description has a value which corresponds to the value of a
/// given expression (or expressions).
/// When working with the C front end, calls to the `__CPROVER_output` intrinsic
/// can be added to the input code in order add instructions of this type to the
/// goto program.
/// The first argument is expected to be a C string denoting the output
/// identifier. The second argument is the expression for the output value.
class code_outputt : public codet
class code_outputt : public goto_instruction_codet
{
public:
/// This constructor is for support of calls to `__CPROVER_output` in user
Expand All @@ -466,7 +474,7 @@ class code_outputt : public codet
optionalt<source_locationt> location = {});

static void check(
const codet &code,
const goto_instruction_codet &code,
const validation_modet vm = validation_modet::INVARIANT);
};

Expand All @@ -481,11 +489,13 @@ inline void validate_expr(const code_outputt &output)
code_outputt::check(output);
}

/// \ref codet representation of a "return from a function" statement.
class code_returnt : public codet
/// \ref goto_instruction_codet representation of a "return from a
/// function" statement.
class code_returnt : public goto_instruction_codet
{
public:
explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
explicit code_returnt(exprt _op)
: goto_instruction_codet(ID_return, {std::move(_op)})
{
}

Expand All @@ -500,17 +510,17 @@ class code_returnt : public codet
}

static void check(
const codet &code,
const goto_instruction_codet &code,
const validation_modet vm = validation_modet::INVARIANT)
{
DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
}

protected:
using codet::op0;
using codet::op1;
using codet::op2;
using codet::op3;
using goto_instruction_codet::op0;
using goto_instruction_codet::op1;
using goto_instruction_codet::op2;
using goto_instruction_codet::op3;
};

template <>
Expand All @@ -524,14 +534,14 @@ inline void validate_expr(const code_returnt &x)
code_returnt::check(x);
}

inline const code_returnt &to_code_return(const codet &code)
inline const code_returnt &to_code_return(const goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_return);
code_returnt::check(code);
return static_cast<const code_returnt &>(code);
}

inline code_returnt &to_code_return(codet &code)
inline code_returnt &to_code_return(goto_instruction_codet &code)
{
PRECONDITION(code.get_statement() == ID_return);
code_returnt::check(code);
Expand Down
Loading