Refactored CEGIS processor body generation.

Author: pkesseli

src/cegis/Makefile

@@ -56,6 +56,8 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       refactor/environment/instrument_state_vars.cpp \
       refactor/instructionset/create_cegis_processor.cpp refactor/instructionset/execute_cegis_program.cpp \
       refactor/instructionset/processor_types.cpp refactor/instructionset/cegis_processor_body_factory.cpp \
+      refactor/instructionset/instruction_description.cpp refactor/instructionset/cegis_instruction_factory.cpp \
+      refactor/instructionset/processor_symbols.cpp \
       refactor/preprocessing/refactor_preprocessing.cpp \
       refactor/learn/refactor_symex_learn.cpp \
       refactor/verify/refactor_symex_verify.cpp \

src/cegis/refactor/instructionset/cegis_instruction_factory.cpp

@@ -0,0 +1,97 @@
+#include <algorithm>
+
+#include <cegis/instrument/instrument_var_ops.h>
+#include <cegis/refactor/instructionset/processor_types.h>
+#include <cegis/refactor/instructionset/processor_symbols.h>
+#include <cegis/refactor/instructionset/cegis_instruction_factory.h>
+
+namespace
+{
+class arithmetic_assignt
+{
+  const irep_idt id;
+  const typet type;
+public:
+  arithmetic_assignt(const irep_idt &id, const typet &type) :
+      id(id), type(type)
+  {
+  }
+
+  goto_programt::targett operator()(const symbol_tablet &st,
+      const std::string &func_name, goto_programt &body,
+      goto_programt::targett pos) const
+  {
+    pos->type=goto_program_instruction_typet::ASSIGN;
+    pos->source_location=default_cegis_source_location();
+    const dereference_exprt lhs(cegis_operand(st, func_name, type, 1));
+    const dereference_exprt rhs(cegis_operand(st, func_name, type, 2));
+    const binary_exprt result(lhs, id, rhs);
+    pos->code=code_assignt(cegis_operand(st, func_name, type, 0), result);
+    return pos;
+  }
+};
+
+class arithmetic_instructionst
+{
+  const typet &type;
+  const instruction_descriptiont::typest sig;
+public:
+  arithmetic_instructionst(const typet &type) :
+      type(type), sig( { type, type, type })
+  {
+  }
+
+  instruction_descriptiont plus() const
+  {
+    return instruction_descriptiont(sig, arithmetic_assignt(ID_plus, type));
+  }
+
+  instruction_descriptiont minus() const
+  {
+    return instruction_descriptiont(sig, arithmetic_assignt(ID_minus, type));
+  }
+
+  instruction_descriptiont mult() const
+  {
+    return instruction_descriptiont(sig, arithmetic_assignt(ID_mult, type));
+  }
+
+  instruction_descriptiont div() const
+  {
+    return instruction_descriptiont(sig, arithmetic_assignt(ID_div, type));
+  }
+};
+
+void insert(
+    std::map<instruction_descriptiont::typest, instruction_descriptionst> &result,
+    const instruction_descriptiont &instr)
+{
+  result[instr.signature].push_back(instr);
+}
+}
+
+ordered_instructionst get_instructions_for_types(
+    const cegis_operand_datat &signature)
+{
+  ordered_instructionst result;
+  for (const cegis_operand_datat::value_type &typeWithSlots : signature)
+  {
+    const typet &type=typeWithSlots.first;
+    if (!is_cegis_primitive(type))
+    assert(!"Class type operand generation not supported.");
+    const arithmetic_instructionst arith(type);
+    insert(result, arith.plus());
+    insert(result, arith.minus());
+    insert(result, arith.mult());
+    insert(result, arith.div());
+  }
+  return result;
+}
+
+instruction_descriptionst::size_type num_instrs(
+    const ordered_instructionst &instrs)
+{
+  return std::accumulate(instrs.begin(), instrs.end(), 0,
+      [](const size_t count, const ordered_instructionst::value_type &instrs)
+      { return count + instrs.second.size();});
+}

src/cegis/refactor/instructionset/cegis_instruction_factory.h

@@ -0,0 +1,42 @@
+/*******************************************************************
+
+Module: Counterexample-Guided Inductive Synthesis
+
+Author: Daniel Kroening, kroening@kroening.com
+        Pascal Kesseli, pascal.kesseli@cs.ox.ac.uk
+
+\*******************************************************************/
+
+#ifndef CEGIS_REFACTOR_INSTRUCTIONSET_CEGIS_INSTRUCTION_FACTORY_H_
+#define CEGIS_REFACTOR_INSTRUCTIONSET_CEGIS_INSTRUCTION_FACTORY_H_
+
+#include <cegis/refactor/instructionset/operand_data.h>
+#include <cegis/refactor/instructionset/instruction_description.h>
+
+typedef std::map<instruction_descriptiont::typest, instruction_descriptionst> ordered_instructionst;
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param signature
+ *
+ * @return
+ */
+ordered_instructionst get_instructions_for_types(
+    const cegis_operand_datat &signature);
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param instrs
+ *
+ * @result
+ */
+instruction_descriptionst::size_type num_instrs(
+    const ordered_instructionst &instrs);
+
+#endif /* CEGIS_REFACTOR_INSTRUCTIONSET_CEGIS_INSTRUCTION_FACTORY_H_ */