From 821eb1dbb6decbcb07afc2ded9b6f1d4c613c404 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 19 May 2018 14:00:38 +0100 Subject: [PATCH] remove basic_blocks and goto_program_irep --- src/goto-programs/Makefile | 2 - src/goto-programs/basic_blocks.cpp | 94 ---------------- src/goto-programs/basic_blocks.h | 20 ---- src/goto-programs/goto_program_irep.cpp | 144 ------------------------ src/goto-programs/goto_program_irep.h | 25 ---- src/util/irep_ids.def | 4 - 6 files changed, 289 deletions(-) delete mode 100644 src/goto-programs/basic_blocks.cpp delete mode 100644 src/goto-programs/basic_blocks.h delete mode 100644 src/goto-programs/goto_program_irep.cpp delete mode 100644 src/goto-programs/goto_program_irep.h diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 98d2cc2a47f..19e5878ca41 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -1,5 +1,4 @@ SRC = adjust_float_expressions.cpp \ - basic_blocks.cpp \ builtin_functions.cpp \ class_hierarchy.cpp \ class_identifier.cpp \ @@ -20,7 +19,6 @@ SRC = adjust_float_expressions.cpp \ goto_inline.cpp \ goto_inline_class.cpp \ goto_program.cpp \ - goto_program_irep.cpp \ goto_program_template.cpp \ goto_trace.cpp \ graphml_witness.cpp \ diff --git a/src/goto-programs/basic_blocks.cpp b/src/goto-programs/basic_blocks.cpp deleted file mode 100644 index 75b91b82bd6..00000000000 --- a/src/goto-programs/basic_blocks.cpp +++ /dev/null @@ -1,94 +0,0 @@ -/*******************************************************************\ - -Module: Group Basic Blocks in Goto Program - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Group Basic Blocks in Goto Program - -#include "basic_blocks.h" - -/// convert basic blocks into single expressions of type "block" -void basic_blocks(goto_programt &goto_program, - unsigned max_block_size) -{ - // get the targets - typedef std::set targetst; - - targetst targets; - - for(goto_programt::instructionst::iterator - i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); - i_it++) - if(i_it->is_goto()) - for(const auto &target : i_it->targets) - targets.insert(target); - - // Scan program - for(goto_programt::instructionst::iterator - it=goto_program.instructions.begin(); - it!=goto_program.instructions.end(); - ) // intentionally no it++ - { - // gotos and empty code are left unchanged - if(it->is_goto() || it->is_dead() || - it->is_assert() || it->is_assume() || - it->is_atomic_begin() || it->is_atomic_end() || - it->is_end_thread() || it->is_start_thread() || - it->is_end_function() || it->is_location() || - it->is_skip() || it->is_function_call() || - it->is_decl()) - it++; - else if(it->is_other() || it->is_assign()) - { - if(it->code.is_nil()) - it++; - else - { - unsigned count=0; - - // this is the start of a new block - targetst::iterator t_it; // iterator for searching targets - - // find the end of the block - goto_programt::instructionst::iterator end_block = it; - do - { - end_block++; - count++; - if(end_block!=goto_program.instructions.end()) - t_it=targets.find(end_block); - - if(max_block_size!=0 && count>=max_block_size) - break; - } - while(end_block!=goto_program.instructions.end() && - (end_block->is_other() || end_block->is_assign()) && - t_it==targets.end()); - - // replace it with the code of the block - - { - code_blockt new_block; - - for(goto_programt::instructionst::iterator stmt = it; - stmt != end_block; - stmt++) - if(!stmt->code.is_nil()) - new_block.move_to_operands(stmt->code); - - it->code.swap(new_block); - it++; - if(it!=goto_program.instructions.end()) - it=goto_program.instructions.erase(it, end_block); - } - } - } - else - UNREACHABLE; - } -} diff --git a/src/goto-programs/basic_blocks.h b/src/goto-programs/basic_blocks.h deleted file mode 100644 index d667c4655d4..00000000000 --- a/src/goto-programs/basic_blocks.h +++ /dev/null @@ -1,20 +0,0 @@ -/*******************************************************************\ - -Module: Group Basic Blocks in Goto Program - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Group Basic Blocks in Goto Program - -#ifndef CPROVER_GOTO_PROGRAMS_BASIC_BLOCKS_H -#define CPROVER_GOTO_PROGRAMS_BASIC_BLOCKS_H - -#include "goto_program.h" - -void basic_blocks(goto_programt &goto_program, - unsigned max_block_size=0); - -#endif // CPROVER_GOTO_PROGRAMS_BASIC_BLOCKS_H diff --git a/src/goto-programs/goto_program_irep.cpp b/src/goto-programs/goto_program_irep.cpp deleted file mode 100644 index 91ffd45065b..00000000000 --- a/src/goto-programs/goto_program_irep.cpp +++ /dev/null @@ -1,144 +0,0 @@ -/*******************************************************************\ - -Module: goto_programt -> irep conversion - -Author: CM Wintersteiger - -Date: May 2007 - -\*******************************************************************/ - -/// \file -/// goto_programt -> irep conversion - -#include "goto_program_irep.h" - -#include - -#include - -void convert(const goto_programt::instructiont &instruction, irept &irep) -{ - irep.set(ID_code, instruction.code); - - if(instruction.function!="") - irep.set(ID_function, instruction.function); - - if(instruction.source_location.is_not_nil()) - irep.set(ID_location, instruction.source_location); - - irep.set(ID_type, (long) instruction.type); - - irep.set(ID_guard, instruction.guard); - - if(!instruction.targets.empty()) - { - irept &tgts=irep.add(ID_targets); - for(const auto &target : instruction.targets) - { - irept t(std::to_string(target->location_number)); - tgts.move_to_sub(t); - } - } - - if(!instruction.labels.empty()) - { - irept &lbls = irep.add(ID_labels); - irept::subt &subs = lbls.get_sub(); - subs.reserve(instruction.labels.size()); - for(const auto &label : instruction.labels) - { - subs.push_back(irept(label)); - } - } -} - -void convert( - const irept &irep, - goto_programt::instructiont &instruction) -{ - instruction.code=static_cast(irep.find(ID_code)); - instruction.function = irep.find(ID_function).id(); - instruction.source_location= - static_cast(irep.find(ID_location)); - instruction.type = static_cast( - unsafe_string2unsigned(irep.find(ID_type).id_string())); - instruction.guard = static_cast(irep.find(ID_guard)); - - // don't touch the targets, the goto_programt conversion does that - - const irept &lbls=irep.find(ID_labels); - const irept::subt &lsubs=lbls.get_sub(); - for(const auto &lsub : lsubs) - instruction.labels.push_back(lsub.id()); -} - -void convert(const goto_programt &program, irept &irep) -{ - irep.id("goto-program"); - irep.get_sub().reserve(program.instructions.size()); - forall_goto_program_instructions(it, program) - { - irep.get_sub().push_back(irept()); - convert(*it, irep.get_sub().back()); - } -} - -void convert(const irept &irep, goto_programt &program) -{ - assert(irep.id()=="goto-program"); - - program.instructions.clear(); - - std::list< std::list > number_targets_list; - - // convert instructions back - const irept::subt &subs = irep.get_sub(); - for(irept::subt::const_iterator it=subs.begin(); - it!=subs.end(); - it++) - { - program.instructions.push_back(goto_programt::instructiont()); - convert(*it, program.instructions.back()); - - number_targets_list.push_back(std::list()); - const irept &targets=it->find(ID_targets); - const irept::subt &tsubs=targets.get_sub(); - for(const auto &tsub : tsubs) - number_targets_list.back().push_back( - unsafe_string2unsigned(tsub.id_string())); - } - - program.compute_location_numbers(); - - // resolve targets - std::list< std::list >::iterator nit= - number_targets_list.begin(); - for(goto_programt::instructionst::iterator lit= - program.instructions.begin(); - lit!=program.instructions.end() && nit!=number_targets_list.end(); - lit++, nit++) - { - for(const unsigned t : *nit) - { - goto_programt::targett fit=program.instructions.begin(); - for( ; fit!=program.instructions.end(); fit++) - { - if(fit->location_number==t) - { - lit->targets.push_back(fit); - break; - } - } - - if(fit==program.instructions.end()) - { - std::cout << "Warning: could not resolve target link " - << "during irep->goto_program translation.\n"; - throw 0; - } - } - } - - program.update(); -} diff --git a/src/goto-programs/goto_program_irep.h b/src/goto-programs/goto_program_irep.h deleted file mode 100644 index 4659e62f9d4..00000000000 --- a/src/goto-programs/goto_program_irep.h +++ /dev/null @@ -1,25 +0,0 @@ -/*******************************************************************\ - -Module: goto_programt -> irep conversion - -Author: CM Wintersteiger - -Date: May 2007 - -\*******************************************************************/ - -/// \file -/// goto_programt -> irep conversion - -#ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_IREP_H -#define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_IREP_H - -#include - -void convert(const goto_programt::instructiont &instruction, irept &irep); -void convert(const irept &irep, goto_programt::instructiont &instruction); - -void convert(const goto_programt &program, irept &irep); -void convert(const irept &irep, goto_programt &program); - -#endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_IREP_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 04fcb8df985..134da97b3cd 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -350,11 +350,7 @@ IREP_ID_ONE(factorial_power) IREP_ID_ONE(pretty_name) IREP_ID_TWO(C_class, #class) IREP_ID_TWO(C_interface, #interface) -IREP_ID_ONE(targets) -IREP_ID_ONE(location) -IREP_ID_ONE(labels) IREP_ID_ONE(event) -IREP_ID_ONE(guard) IREP_ID_ONE(designated_initializer) IREP_ID_ONE(designator) IREP_ID_ONE(member_designator)