Skip to content

Cleanup the API of dfcc_loop_nesting_grapht #7693

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 3 commits into from
May 12, 2023
Merged

Cleanup the API of dfcc_loop_nesting_grapht #7693

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
62fbfe8
analyses/loop_analysis.h: fix includes
tautschnig Apr 27, 2023
b96bbeb
build_loop_nesting_graph: remove unused logging parameter
tautschnig Apr 27, 2023
fe428ad
dfcc_loop_nesting_grapht: cleanup loop includes
tautschnig Apr 27, 2023
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
2 changes: 1 addition & 1 deletion src/analyses/loop_analysis.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ Author: Diffblue Ltd
#ifndef CPROVER_ANALYSES_LOOP_ANALYSIS_H
#define CPROVER_ANALYSES_LOOP_ANALYSIS_H

#include <memory>
#include <goto-programs/goto_model.h>

template <class T>
class loop_analysist;
Expand Down
5 changes: 2 additions & 3 deletions src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -522,16 +522,15 @@ dfcc_cfg_infot::dfcc_cfg_infot(
: function_id(function_id),
goto_function(goto_function),
top_level_write_set(top_level_write_set),
log(message_handler),
ns(symbol_table)
{
dfcc_loop_nesting_grapht loop_nesting_graph;
goto_programt &goto_program = goto_function.body;
messaget log(message_handler);
if(loop_contract_mode != dfcc_loop_contract_modet::NONE)
{
messaget log(message_handler);
dfcc_check_loop_normal_form(goto_program, log);
loop_nesting_graph = build_loop_nesting_graph(goto_program, log);
loop_nesting_graph = build_loop_nesting_graph(goto_program);

const auto head = check_inner_loops_have_contracts(loop_nesting_graph);
if(head.has_value())
Expand Down
3 changes: 1 addition & 2 deletions src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@ Date: March 2023
#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H
#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CFG_INFO_H

#include <util/message.h>
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
Expand All @@ -33,6 +32,7 @@ Date: March 2023
class dfcc_utilst;
class dfcc_libraryt;
class goto_functiont;
class message_handlert;

/// \brief Describes a single loop for the purpose of DFCC loop contract
/// instrumentation.
Expand Down Expand Up @@ -297,7 +297,6 @@ class dfcc_cfg_infot
const irep_idt &function_id;
goto_functiont &goto_function;
const exprt &top_level_write_set;
messaget log;
const namespacet ns;

/// True iff \p id is in the valid range for a loop id or is equal to
Expand Down
8 changes: 3 additions & 5 deletions src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,20 +12,18 @@ Date: March 2023

#include "dfcc_loop_nesting_graph.h"

#include <util/invariant.h>
#include <util/message.h>
#include <analyses/natural_loops.h>

dfcc_loop_nesting_graph_nodet::dfcc_loop_nesting_graph_nodet(
const goto_programt::targett &head,
const goto_programt::targett &latch,
const loopt &instructions)
const loop_templatet<goto_programt::targett> &instructions)
: head(head), latch(latch), instructions(instructions)
{
}

/// \pre Loop normal form properties must hold.
dfcc_loop_nesting_grapht
build_loop_nesting_graph(goto_programt &goto_program, messaget &log)
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program)
{
natural_loops_mutablet natural_loops(goto_program);
dfcc_loop_nesting_grapht loop_nesting_graph;
Expand Down
10 changes: 5 additions & 5 deletions src/goto-instrument/contracts/dynamic-frames/dfcc_loop_nesting_graph.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ Date: March 2023

#include <util/graph.h>

#include <goto-instrument/loop_utils.h>
#include <analyses/loop_analysis.h>

class messaget;

Expand All @@ -29,7 +29,7 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
dfcc_loop_nesting_graph_nodet(
const goto_programt::targett &head,
const goto_programt::targett &latch,
const loopt &instructions);
const loop_templatet<goto_programt::targett> &instructions);

/// Loop head instruction
goto_programt::targett head;
Expand All @@ -38,7 +38,7 @@ struct dfcc_loop_nesting_graph_nodet : public graph_nodet<empty_edget>
goto_programt::targett latch;

/// Set of loop instructions
loopt instructions;
loop_templatet<goto_programt::targett> instructions;
};

typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;
Expand All @@ -47,6 +47,6 @@ typedef grapht<dfcc_loop_nesting_graph_nodet> dfcc_loop_nesting_grapht;
/// loops in the given \p goto_program.
/// A loop is considered nested in an outer loop if its head and its latch are
/// both found in the instructions of the outer loop.
dfcc_loop_nesting_grapht
build_loop_nesting_graph(goto_programt &goto_program, messaget &log);
dfcc_loop_nesting_grapht build_loop_nesting_graph(goto_programt &goto_program);

#endif