From f36317806135e04f69eaf35f4854e5e5d764ab78 Mon Sep 17 00:00:00 2001 From: Elazar Gershuni Date: Tue, 17 Dec 2024 00:48:06 +0200 Subject: [PATCH] get rid of GuardedInstructions Signed-off-by: Elazar Gershuni --- src/asm_cfg.cpp | 25 +++++++++++-------------- src/asm_syntax.hpp | 6 ------ src/program.hpp | 12 +++++++----- 3 files changed, 18 insertions(+), 25 deletions(-) diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp index a3b4cad8..acaf689f 100644 --- a/src/asm_cfg.cpp +++ b/src/asm_cfg.cpp @@ -24,7 +24,7 @@ struct cfg_builder_t final { Program prog; // TODO: ins should be inserted elsewhere - void insert_after(const label_t& prev_label, const label_t& new_label, const GuardedInstruction& ins) { + void insert_after(const label_t& prev_label, const label_t& new_label, const Instruction& ins) { if (prev_label == new_label) { CRAB_ERROR("Cannot insert after the same label ", to_string(new_label)); } @@ -43,7 +43,7 @@ struct cfg_builder_t final { } // TODO: ins should be inserted elsewhere - void insert(const label_t& _label, const GuardedInstruction& ins) { + void insert(const label_t& _label, const Instruction& ins) { if (const auto it = prog.m_cfg.neighbours.find(_label); it != prog.m_cfg.neighbours.end()) { CRAB_ERROR("Label ", to_string(_label), " already exists"); } @@ -52,7 +52,7 @@ struct cfg_builder_t final { } // TODO: ins should be inserted elsewhere - label_t insert_jump(const label_t& from, const label_t& to, const GuardedInstruction& ins) { + label_t insert_jump(const label_t& from, const label_t& to, const Instruction& ins) { const label_t jump_label = label_t::make_jump(from, to); if (prog.m_cfg.contains(jump_label)) { CRAB_ERROR("Jump label ", to_string(jump_label), " already exists"); @@ -76,10 +76,10 @@ struct cfg_builder_t final { } void set_assertions(const label_t& label, const std::vector& assertions) { - if (!prog.m_instructions.contains(label)) { + if (!prog.m_cfg.contains(label)) { CRAB_ERROR("Label ", to_string(label), " not found in the CFG: "); } - prog.m_instructions.at(label).preconditions = assertions; + prog.m_assertions.insert_or_assign(label, assertions); } }; @@ -164,7 +164,7 @@ static void add_cfg_nodes(cfg_builder_t& builder, const label_t& caller_label, c } else if (const auto pcall = std::get_if(&inst)) { pcall->stack_frame_prefix = label.stack_frame_prefix; } - builder.insert(label, {.cmd = inst}); + builder.insert(label, inst); if (first) { // Add an edge from the caller to the new block. @@ -226,7 +226,7 @@ static cfg_builder_t instruction_seq_to_cfg(const InstructionSeq& insts, const b if (std::holds_alternative(inst)) { continue; } - builder.insert(label, GuardedInstruction{.cmd = inst}); + builder.insert(label, inst); } if (insts.size() == 0) { @@ -262,10 +262,8 @@ static cfg_builder_t instruction_seq_to_cfg(const InstructionSeq& insts, const b if (!builder.prog.cfg().contains(target_label)) { throw InvalidControlFlow{"jump to undefined label " + to_string(target_label)}; } - builder.insert_jump(label, target_label, - GuardedInstruction{.cmd = Assume{.cond = *cond, .is_implicit = true}}); - builder.insert_jump(label, fallthrough, - GuardedInstruction{.cmd = Assume{.cond = reverse(*cond), .is_implicit = true}}); + builder.insert_jump(label, target_label, Assume{.cond = *cond, .is_implicit = true}); + builder.insert_jump(label, fallthrough, Assume{.cond = reverse(*cond), .is_implicit = true}); } else { builder.add_child(label, jmp->target); } @@ -304,8 +302,7 @@ Program Program::from_sequence(const InstructionSeq& inst_seq, const program_inf if (options.check_for_termination) { const crab::wto_t wto{builder.prog.cfg()}; wto.for_each_loop_head([&](const label_t& label) -> void { - builder.insert_after(label, label_t::make_increment_counter(label), - GuardedInstruction{.cmd = IncrementLoopCounter{label}}); + builder.insert_after(label, label_t::make_increment_counter(label), IncrementLoopCounter{label}); }); } @@ -455,7 +452,7 @@ crab::cfg_t crab::cfg_from_adjacency_list(const std::map; -struct GuardedInstruction { - Instruction cmd; - std::vector preconditions; - bool operator==(const GuardedInstruction&) const = default; -}; - std::ostream& operator<<(std::ostream& os, Instruction const& ins); std::string to_string(Instruction const& ins); diff --git a/src/program.hpp b/src/program.hpp index a26700a1..ec721ff1 100644 --- a/src/program.hpp +++ b/src/program.hpp @@ -14,8 +14,10 @@ class Program { friend struct cfg_builder_t; - std::map m_instructions{{label_t::entry, {.cmd = Undefined{}}}, - {label_t::exit, {.cmd = Undefined{}}}}; + std::map m_instructions{{label_t::entry, Undefined{}}, {label_t::exit, Undefined{}}}; + + // This is a cache. The assertions can also be computed on the fly. + std::map> m_assertions{{label_t::entry, {}}, {label_t::exit, {}}}; crab::cfg_t m_cfg; // TODO: add program_info field @@ -33,21 +35,21 @@ class Program { if (!m_instructions.contains(label)) { CRAB_ERROR("Label ", to_string(label), " not found in the CFG: "); } - return m_instructions.at(label).cmd; + return m_instructions.at(label); } Instruction& instruction_at(const label_t& label) { if (!m_instructions.contains(label)) { CRAB_ERROR("Label ", to_string(label), " not found in the CFG: "); } - return m_instructions.at(label).cmd; + return m_instructions.at(label); } std::vector assertions_at(const label_t& label) const { if (!m_instructions.contains(label)) { CRAB_ERROR("Label ", to_string(label), " not found in the CFG: "); } - return m_instructions.at(label).preconditions; + return m_assertions.at(label); } static Program from_sequence(const InstructionSeq& inst_seq, const program_info& info,