fact-gen: support freeze instruction

GaloisInc · Apr 7, 2023 · 1a64af9 · 1a64af9
1 parent 79e8394
commit 1a64af9
Show file tree

Hide file tree

Showing 9 changed files with 47 additions and 0 deletions.
diff --git a/FactGenerator/include/InstructionVisitor.hpp b/FactGenerator/include/InstructionVisitor.hpp
@@ -100,6 +100,7 @@ class cclyzer::InstructionVisitor
   void visitCallInst(const llvm::CallInst &);
   void visitDbgDeclareInst(const llvm::DbgDeclareInst &);
   void visitVAArgInst(const llvm::VAArgInst &);
+  void visitFreezeInst(const llvm::FreezeInst &);
 
   // Vector Operations
 

diff --git a/FactGenerator/include/predicates.inc b/FactGenerator/include/predicates.inc
@@ -463,6 +463,11 @@ PREDICATE2(fneg, instr)
 PREDICATEI(fneg, operand)
 GROUP_END(fneg)
 
+GROUP_BEGIN(freeze)
+PREDICATE2(freeze, instr)
+PREDICATEI(freeze, operand)
+GROUP_END(freeze)
+
 // Types
 
 GROUP_BEGIN(primitive_type)

diff --git a/FactGenerator/src/InstructionVisitor.cpp b/FactGenerator/src/InstructionVisitor.cpp
@@ -701,6 +701,12 @@ void InstructionVisitor::visitUnaryInstruction(
   }
 }
 
+void InstructionVisitor::visitFreezeInst(const llvm::FreezeInst &FI) {
+  refmode_t iref = recordInstruction(pred::freeze::instr, FI);
+
+  writeInstrOperand(pred::freeze::operand, iref, FI.getOperand(0));
+}
+
 void InstructionVisitor::visitInstruction(const llvm::Instruction &I) {
   unknown("instruction", I.getOpcodeName());
 }

diff --git a/datalog/CMakeLists.txt b/datalog/CMakeLists.txt
@@ -86,6 +86,7 @@ set(DL_SOURCES
     ${CMAKE_CURRENT_LIST_DIR}/schema/phi-instr.dl
     ${CMAKE_CURRENT_LIST_DIR}/schema/fmul-instr.dl
     ${CMAKE_CURRENT_LIST_DIR}/schema/fneg-instr.dl
+    ${CMAKE_CURRENT_LIST_DIR}/schema/freeze-instr.dl
     ${CMAKE_CURRENT_LIST_DIR}/schema/basic-block.dl
     ${CMAKE_CURRENT_LIST_DIR}/schema/global.dl
     ${CMAKE_CURRENT_LIST_DIR}/schema/call-instr.dl

diff --git a/datalog/export/debug-output-extended.dl b/datalog/export/debug-output-extended.dl
@@ -310,6 +310,8 @@
 .output fptrunc_instr_from_operand (compress=true)
 .output fptrunc_instr_from_type (compress=true)
 .output fptrunc_instr_to_type (compress=true)
+.output freeze_instr (compress=true)
+.output freeze_instr_operand (compress=true)
 .output frem_instr (compress=true)
 .output frem_instr_first_operand (compress=true)
 .output frem_instr_second_operand (compress=true)

diff --git a/datalog/export/debug-output.dl b/datalog/export/debug-output.dl
@@ -310,6 +310,8 @@
 .output fptrunc_instr_from_operand (compress=true)
 .output fptrunc_instr_from_type (compress=true)
 .output fptrunc_instr_to_type (compress=true)
+.output freeze_instr (compress=true)
+.output freeze_instr_operand (compress=true)
 .output frem_instr (compress=true)
 .output frem_instr_first_operand (compress=true)
 .output frem_instr_second_operand (compress=true)

diff --git a/datalog/schema/freeze-instr.dl b/datalog/schema/freeze-instr.dl
@@ -0,0 +1,28 @@
+// http://llvm.org/docs/LangRef.html#freeze-instr
+// keywords: instr
+
+.type FreezeInstruction <: symbol
+.decl freeze_instr(instr:FreezeInstruction)
+
+instr(v) :- freeze_instr(v).
+
+.decl freeze_instr_operand(instr:FreezeInstruction, val:Operand)
+
+
+//------------------------------------------------------------------------------
+// [Constraints]
+//
+// The ‘freeze‘ instr requires that the resulting value is the same type as its
+// operand.
+//------------------------------------------------------------------------------
+
+schema_invalid_instr(Instr, __FILE__, __LINE__) :-
+    schema_sanity(),
+    freeze_instr(Instr),
+    !freeze_instr_operand(Instr, _).
+
+schema_invalid_instr(Instr, __FILE__, __LINE__) :-
+    schema_sanity(),
+    instr_returns_type(Instr, Type),
+    freeze_instr_operand(Instr, Op),
+    !operand_has_type(Op, Type).
diff --git a/datalog/schema/instr.dl b/datalog/schema/instr.dl
@@ -27,6 +27,7 @@
   | FRemInstruction
   | FSubInstruction
   | FenceInstruction
+  | FreezeInstruction
   | GetElementPtrInstruction
   | ICmpInstruction
   | IndirectBrInstruction

diff --git a/datalog/schema/schema.project b/datalog/schema/schema.project
@@ -22,6 +22,7 @@
 #include "fmul-instr.dl"
 #include "fneg-instr.dl"
 #include "fdiv-instr.dl"
+#include "freeze-instr.dl"
 #include "frem-instr.dl"
 #include "and-instr.dl"
 #include "or-instr.dl"