diff --git a/FactGenerator/include/predicates.inc b/FactGenerator/include/predicates.inc index f4d2e23..6d6eb2e 100644 --- a/FactGenerator/include/predicates.inc +++ b/FactGenerator/include/predicates.inc @@ -64,15 +64,18 @@ PREDICATE2(func, param_attr) GROUP_END(function) GROUP_BEGIN(instr) -PREDICATE(instr, to, instr_assigns_to) -PREDICATE(instr, flag, instr_flag) -PREDICATE(instr, next, next_instr) -PREDICATE(instr, bb_entry, instr_bb_entry) -PREDICATE(instr, func, instr_func) -PREDICATE(instr, pos, instr_pos) -PREDICATE(instr, unreachable, unreachable_instr) +PREDICATE2(instr, assigns_to) +PREDICATE2(instr, flag) +PREDICATE2(instr, successor) +PREDICATE2(instr, bb_entry) +PREDICATE2(instr, func) +PREDICATE2(instr, pos) GROUP_END(instr) +GROUP_BEGIN(unreachable) +PREDICATE2(unreachable, instr) +GROUP_END(unreachable) + GROUP_BEGIN(add) PREDICATE2(add, instr) PREDICATEI(add, first_operand) @@ -187,20 +190,19 @@ GROUP_END(xor_) GROUP_BEGIN(ret) PREDICATE2(ret, instr) -// TODO(#42): -PREDICATE(ret, instr_void, void_ret_instr) -// TODO(#42): -PREDICATE(ret, operand, ret_instr_value) +// Can't be named 'void', as that's a C++ keyword. +PREDICATEI(ret, void_) +PREDICATEI(ret, operand) GROUP_END(ret) GROUP_BEGIN(br) PREDICATE2(br, instr) -PREDICATE(br, instr_cond, br_cond_instr) -PREDICATE(br, condition, br_cond_instr_condition) -PREDICATE(br, cond_iftrue, br_cond_instr_iftrue_label) -PREDICATE(br, cond_iffalse, br_cond_instr_iffalse_label) -PREDICATE(br, instr_uncond, br_uncond_instr) -PREDICATE(br, uncond_dest, br_uncond_instr_dest_label) +PREDICATEI(br, cond) +PREDICATEI(br, condition) +PREDICATEI(br, true_label) +PREDICATEI(br, false_label) +PREDICATEI(br, uncond) +PREDICATEI(br, uncond_label) GROUP_END(br) GROUP_BEGIN(switch_) diff --git a/FactGenerator/src/FactGenerator.cpp b/FactGenerator/src/FactGenerator.cpp index 6814cc3..7a5e48b 100644 --- a/FactGenerator/src/FactGenerator.cpp +++ b/FactGenerator/src/FactGenerator.cpp @@ -157,7 +157,7 @@ auto FactGenerator::processModule( if (!instr.getType()->isVoidTy()) { refmode_t targetVar = refmode(instr); - writeFact(pred::instr::to, iref, targetVar); + writeFact(pred::instr::assigns_to, iref, targetVar); recordVariable(targetVar, instr.getType()); // Save variables for the CPG @@ -166,7 +166,7 @@ auto FactGenerator::processModule( } // Record successor instruction - if (prev_instr) writeFact(pred::instr::next, prev_iref, iref); + if (prev_instr) writeFact(pred::instr::successor, prev_iref, iref); // Store the refmode of this instruction for next iteration prev_iref = iref; diff --git a/FactGenerator/src/InstructionVisitor.cpp b/FactGenerator/src/InstructionVisitor.cpp index 2c1f459..9d2d9c5 100644 --- a/FactGenerator/src/InstructionVisitor.cpp +++ b/FactGenerator/src/InstructionVisitor.cpp @@ -215,7 +215,7 @@ void InstructionVisitor::visitReturnInst(const llvm::ReturnInst &RI) { if (RI.getReturnValue()) { // with returned value writeInstrOperand(pred::ret::operand, iref, RI.getReturnValue()); } else { // w/o returned value - gen.writeFact(pred::ret::instr_void, iref); + gen.writeFact(pred::ret::void_, iref); } } @@ -224,18 +224,18 @@ void InstructionVisitor::visitBranchInst(const llvm::BranchInst &BI) { if (BI.isConditional()) { // conditional branch // br i1 , label , label - gen.writeFact(pred::br::instr_cond, iref); + gen.writeFact(pred::br::cond, iref); // Condition Operand writeInstrOperand(pred::br::condition, iref, BI.getCondition()); // 'iftrue' and 'iffalse' labels - writeInstrOperand(pred::br::cond_iftrue, iref, BI.getOperand(1)); - writeInstrOperand(pred::br::cond_iffalse, iref, BI.getOperand(2)); + writeInstrOperand(pred::br::true_label, iref, BI.getOperand(1)); + writeInstrOperand(pred::br::false_label, iref, BI.getOperand(2)); } else { // unconditional branch // br label - gen.writeFact(pred::br::instr_uncond, iref); - writeInstrOperand(pred::br::uncond_dest, iref, BI.getOperand(0)); + gen.writeFact(pred::br::uncond, iref); + writeInstrOperand(pred::br::uncond_label, iref, BI.getOperand(0)); } } @@ -320,7 +320,7 @@ void InstructionVisitor::visitResumeInst(const llvm::ResumeInst &RI) { } void InstructionVisitor::visitUnreachableInst(const llvm::UnreachableInst &I) { - recordInstruction(pred::instr::unreachable, I); + recordInstruction(pred::unreachable::instr, I); } void InstructionVisitor::visitAllocaInst(const llvm::AllocaInst &AI) { diff --git a/datalog/export/debug-output-extended.dl b/datalog/export/debug-output-extended.dl index e11e6fd..e945d9a 100644 --- a/datalog/export/debug-output-extended.dl +++ b/datalog/export/debug-output-extended.dl @@ -143,13 +143,13 @@ .output block_predecessors (compress=true) .output boolean_type (compress=true) .output boolean_vector_type (compress=true) -.output br_cond_instr (compress=true) -.output br_cond_instr_condition (compress=true) -.output br_cond_instr_iffalse_label (compress=true) -.output br_cond_instr_iftrue_label (compress=true) +.output br_instr_cond (compress=true) +.output br_instr_condition (compress=true) +.output br_instr_false_label (compress=true) +.output br_instr_true_label (compress=true) .output br_instr (compress=true) -.output br_uncond_instr (compress=true) -.output br_uncond_instr_dest_label (compress=true) +.output br_instr_uncond (compress=true) +.output br_instr_uncond_label (compress=true) .output call_instr (compress=true) .output call_instr_arg (compress=true) .output call_instr_fn_operand (compress=true) @@ -575,8 +575,8 @@ .output mul_instr_first_operand (compress=true) .output mul_instr_second_operand (compress=true) .output nallocs_by_pt_size (compress=true) -.output next_instr (compress=true) -.output next_instr_index (compress=true) +.output instr_successor (compress=true) +.output instr_successor_index (compress=true) .output non_allocation (compress=true) .output nonempty_ptr (compress=true) .output nonempty_ptrs (compress=true) @@ -673,7 +673,7 @@ .output resume_instr (compress=true) .output resume_instr_operand (compress=true) .output ret_instr (compress=true) -.output ret_instr_value (compress=true) +.output ret_instr_operand (compress=true) .output schema_invalid_alias (compress=true) .output schema_invalid_constant (compress=true) .output schema_invalid_func (compress=true) @@ -826,7 +826,7 @@ .output vector_type_has_component (compress=true) .output vector_type_has_size (compress=true) .output visibility (compress=true) -.output void_ret_instr (compress=true) +.output ret_instr_void_ (compress=true) .output void_type (compress=true) .output vtable (compress=true) .output vtable_func (compress=true) diff --git a/datalog/export/debug-output.dl b/datalog/export/debug-output.dl index e11e6fd..e945d9a 100644 --- a/datalog/export/debug-output.dl +++ b/datalog/export/debug-output.dl @@ -143,13 +143,13 @@ .output block_predecessors (compress=true) .output boolean_type (compress=true) .output boolean_vector_type (compress=true) -.output br_cond_instr (compress=true) -.output br_cond_instr_condition (compress=true) -.output br_cond_instr_iffalse_label (compress=true) -.output br_cond_instr_iftrue_label (compress=true) +.output br_instr_cond (compress=true) +.output br_instr_condition (compress=true) +.output br_instr_false_label (compress=true) +.output br_instr_true_label (compress=true) .output br_instr (compress=true) -.output br_uncond_instr (compress=true) -.output br_uncond_instr_dest_label (compress=true) +.output br_instr_uncond (compress=true) +.output br_instr_uncond_label (compress=true) .output call_instr (compress=true) .output call_instr_arg (compress=true) .output call_instr_fn_operand (compress=true) @@ -575,8 +575,8 @@ .output mul_instr_first_operand (compress=true) .output mul_instr_second_operand (compress=true) .output nallocs_by_pt_size (compress=true) -.output next_instr (compress=true) -.output next_instr_index (compress=true) +.output instr_successor (compress=true) +.output instr_successor_index (compress=true) .output non_allocation (compress=true) .output nonempty_ptr (compress=true) .output nonempty_ptrs (compress=true) @@ -673,7 +673,7 @@ .output resume_instr (compress=true) .output resume_instr_operand (compress=true) .output ret_instr (compress=true) -.output ret_instr_value (compress=true) +.output ret_instr_operand (compress=true) .output schema_invalid_alias (compress=true) .output schema_invalid_constant (compress=true) .output schema_invalid_func (compress=true) @@ -826,7 +826,7 @@ .output vector_type_has_component (compress=true) .output vector_type_has_size (compress=true) .output visibility (compress=true) -.output void_ret_instr (compress=true) +.output ret_instr_void_ (compress=true) .output void_type (compress=true) .output vtable (compress=true) .output vtable_func (compress=true) diff --git a/datalog/points-to/interprocedural.dl b/datalog/points-to/interprocedural.dl index 93b8105..759a404 100644 --- a/datalog/points-to/interprocedural.dl +++ b/datalog/points-to/interprocedural.dl @@ -179,7 +179,7 @@ func_param_not_by_value(?callee, ?index, ?param) :- .decl func_returns_value(?retValue: Operand, ?inFunction: Function) func_returns_value(?retValue, ?inFunction) :- - ret_instr_value(?retInsn, ?retValue), + ret_instr_operand(?retInsn, ?retValue), instr_func(?retInsn, ?inFunction). .comp InterpAssignment { diff --git a/datalog/schema/basic-block.dl b/datalog/schema/basic-block.dl index c0f4692..1b58f5c 100644 --- a/datalog/schema/basic-block.dl +++ b/datalog/schema/basic-block.dl @@ -40,23 +40,23 @@ block_of_label(cat("block:", Label), Label) :- block_first_instr(BB, First) :- instr_block(First, BB), - !next_instr(_, First). + !instr_successor(_, First). block_first_instr(BB2, First) :- - next_instr(Last, First), + instr_successor(Last, First), instr_block(Last, BB1), instr_block(First, BB2), BB1 != BB2. block_last_instr(BB1, Last) :- - next_instr(Last, First), + instr_successor(Last, First), instr_block(Last, BB1), instr_block(First, BB2), BB1 != BB2. block_last_instr(BB, Last) :- instr_block(Last, BB), - !next_instr(Last, _). + !instr_successor(Last, _). //------------------------------------------------------------------------------ @@ -69,7 +69,7 @@ block_last_instr(BB, Last) :- schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - next_instr(Instr, NextInstr), + instr_successor(Instr, NextInstr), instr_block(Instr, BB1), instr_block(NextInstr, BB2), !terminator_instr(Instr), diff --git a/datalog/schema/br-instr.dl b/datalog/schema/br-instr.dl index af5cfc3..3d9b973 100644 --- a/datalog/schema/br-instr.dl +++ b/datalog/schema/br-instr.dl @@ -6,30 +6,30 @@ .type BrUncondInstruction = BrInstruction .decl br_instr(instr:BrInstruction) -.decl br_cond_instr(instr:BrCondInstruction) -.decl br_uncond_instr(instr:BrUncondInstruction) +.decl br_instr_cond(instr:BrCondInstruction) +.decl br_instr_uncond(instr:BrUncondInstruction) instr(v) :- br_instr(v). terminator_instr(v) :- br_instr(v). -br_instr(v) :- br_cond_instr(v). -br_instr(v) :- br_uncond_instr(v). +br_instr(v) :- br_instr_cond(v). +br_instr(v) :- br_instr_uncond(v). //----------------------------- // Conditional branch //----------------------------- -.decl br_cond_instr_condition(instr:Instruction, cond:Operand) -.decl br_cond_instr_iftrue_label(instr:Instruction, label:Variable) -.decl br_cond_instr_iffalse_label(instr:Instruction, label:Variable) +.decl br_instr_condition(instr:Instruction, cond:Operand) +.decl br_instr_true_label(instr:Instruction, label:Variable) +.decl br_instr_false_label(instr:Instruction, label:Variable) //----------------------------- // Unconditional branch //----------------------------- -.decl br_uncond_instr_dest_label(instr:Instruction, label:Variable) +.decl br_instr_uncond_label(instr:Instruction, label:Variable) //------------------------------------------------------------------------------ @@ -45,45 +45,45 @@ br_instr(v) :- br_uncond_instr(v). schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - br_cond_instr(Instr), - !br_cond_instr_condition(Instr, _). + br_instr_cond(Instr), + !br_instr_condition(Instr, _). schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - br_cond_instr(Instr), - br_cond_instr_condition(Instr, Cond), + br_instr_cond(Instr), + br_instr_condition(Instr, Cond), operand_has_type(Cond, CondType), !int1_type(CondType). schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - br_cond_instr(Instr), - !br_cond_instr_iftrue_label(Instr, _). + br_instr_cond(Instr), + !br_instr_true_label(Instr, _). schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - br_cond_instr(Instr), - !br_cond_instr_iffalse_label(Instr, _). + br_instr_cond(Instr), + !br_instr_false_label(Instr, _). schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - br_cond_instr(Instr), - br_cond_instr_iftrue_label(Instr, Label), + br_instr_cond(Instr), + br_instr_true_label(Instr, Label), !variable_is_label(Label). schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - br_cond_instr(Instr), - br_cond_instr_iffalse_label(Instr, Label), + br_instr_cond(Instr), + br_instr_false_label(Instr, Label), !variable_is_label(Label). schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - br_uncond_instr(Instr), - !br_uncond_instr_dest_label(Instr, _). + br_instr_uncond(Instr), + !br_instr_uncond_label(Instr, _). schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - br_uncond_instr(Instr), - br_uncond_instr_dest_label(Instr, Label), + br_instr_uncond(Instr), + br_instr_uncond_label(Instr, Label), !variable_is_label(Label). diff --git a/datalog/schema/extractvalue-instr.dl b/datalog/schema/extractvalue-instr.dl index d36a7db..579d14d 100644 --- a/datalog/schema/extractvalue-instr.dl +++ b/datalog/schema/extractvalue-instr.dl @@ -15,7 +15,7 @@ instr(v) :- extractvalue_instr(v). .decl extractvalue_instr_nindices(instr:ExtractValueInstruction, total:number) .decl extractvalue_instr_index(instr:ExtractValueInstruction, i:number, idx:number) -next_instr_index(Instr, Index, Index + 1) :- +instr_successor_index(Instr, Index, Index + 1) :- extractvalue_instr_index(Instr, Index, _). @@ -35,12 +35,12 @@ extractvalue_instrterm_type(Instr, NextIndex, Type) :- extractvalue_instrterm_type(Instr, Index, StructType), extractvalue_instr_index(Instr, Index, IdxValue), struct_type_field(StructType, IdxValue, Type), - next_instr_index(Instr, Index, NextIndex). + instr_successor_index(Instr, Index, NextIndex). extractvalue_instrterm_type(Instr, NextIndex, Type) :- extractvalue_instrterm_type(Instr, Index, ArrayType), array_type_has_component(ArrayType, Type), - next_instr_index(Instr, Index, NextIndex). + instr_successor_index(Instr, Index, NextIndex). extractvalue_instr_value_type(Instr, Type) :- extractvalue_instr_nindices(Instr, Total), diff --git a/datalog/schema/getelementptr-instr.dl b/datalog/schema/getelementptr-instr.dl index fef6c19..844710b 100644 --- a/datalog/schema/getelementptr-instr.dl +++ b/datalog/schema/getelementptr-instr.dl @@ -72,7 +72,7 @@ gep_is_vector_based(Instr) :- .decl getelementptr_instr_value_type(instr:GetElementPtrInstruction, type:Type) -next_instr_index(Instr, Index, Index + 1) :- +instr_successor_index(Instr, Index, Index + 1) :- getelementptr_instr_index(Instr, Index, _). getelementptr_instrterm_type(Instr, 1, Type) :- @@ -87,12 +87,12 @@ getelementptr_instrterm_type(Instr, 1, Type) :- getelementptr_instrterm_type(Instr, NextIndex, Type) :- getelementptr_instrterm_type(Instr, Index, ArrayType), array_type_has_component(ArrayType, Type), - next_instr_index(Instr, Index, NextIndex). + instr_successor_index(Instr, Index, NextIndex). getelementptr_instrterm_type(Instr, NextIndex, Type) :- getelementptr_instrterm_type(Instr, Index, VectorType), vector_type_has_component(VectorType, Type), - next_instr_index(Instr, Index, NextIndex). + instr_successor_index(Instr, Index, NextIndex). getelementptr_instrterm_type(Instr, NextIndex, Type) :- getelementptr_instrterm_type(Instr, Index, StructType), @@ -101,7 +101,7 @@ getelementptr_instrterm_type(Instr, NextIndex, Type) :- constant_to_int(FieldIdx, FieldIdxValue), int32_type(FieldIdxType), // c3 struct_type_field(StructType, FieldIdxValue, Type), - next_instr_index(Instr, Index, NextIndex). + instr_successor_index(Instr, Index, NextIndex). getelementptr_instr_value_type(Instr, Type) :- getelementptr_instr_nindices(Instr, Total), diff --git a/datalog/schema/insertvalue-instr.dl b/datalog/schema/insertvalue-instr.dl index b9ce2be..cbb48b4 100644 --- a/datalog/schema/insertvalue-instr.dl +++ b/datalog/schema/insertvalue-instr.dl @@ -16,7 +16,7 @@ instr(v) :- insertvalue_instr(v). .decl insertvalue_instr_nindices(instr:InsertValueInstruction, total:number) .decl insertvalue_instr_index(instr:InsertValueInstruction, i:number, idx:number) -next_instr_index(Instr, Index, Index + 1) :- +instr_successor_index(Instr, Index, Index + 1) :- insertvalue_instr_index(Instr, Index, _). @@ -36,12 +36,12 @@ insertvalue_instrterm_type(Instr, NextIndex, Type) :- insertvalue_instrterm_type(Instr, Index, StructType), insertvalue_instr_index(Instr, Index, IdxValue), struct_type_field(StructType, IdxValue, Type), - next_instr_index(Instr, Index, NextIndex). + instr_successor_index(Instr, Index, NextIndex). insertvalue_instrterm_type(Instr, NextIndex, Type) :- insertvalue_instrterm_type(Instr, Index, ArrayType), array_type_has_component(ArrayType, Type), - next_instr_index(Instr, Index, NextIndex). + instr_successor_index(Instr, Index, NextIndex). insertvalue_instr_value_type(Instr, Type) :- insertvalue_instr_nindices(Instr, Total), diff --git a/datalog/schema/instr.dl b/datalog/schema/instr.dl index 2470c06..6bd5511 100644 --- a/datalog/schema/instr.dl +++ b/datalog/schema/instr.dl @@ -33,7 +33,7 @@ flag(Flag) :- instr_flag(_, Flag). // helpful in avoiding non-termination warnings -.decl next_instr_index(instr:Instruction, index:number, next_index:number) +.decl instr_successor_index(instr:Instruction, index:number, next_index:number) // Position of instr on source code (if debug info is available) .decl instr_pos(instr:Instruction, line:LineNumber, column:ColumnNumber) @@ -44,7 +44,7 @@ flag(Flag) :- instr_flag(_, Flag). //------------------------------------ // The next instr in the source file. -.decl next_instr(instr:Instruction, next:Instruction) +.decl instr_successor(instr:Instruction, next:Instruction) // The func that contains the instr .decl instr_func(instr:Instruction, func:Function) diff --git a/datalog/schema/landingpad-instr.dl b/datalog/schema/landingpad-instr.dl index 23cde7e..a7d6b77 100644 --- a/datalog/schema/landingpad-instr.dl +++ b/datalog/schema/landingpad-instr.dl @@ -73,7 +73,7 @@ _landingpad_starting_phi(BB, Instr) :- _landingpad_starting_phi(BB, NextInstr) :- _landingpad_starting_phi(BB, Instr), - next_instr(Instr, NextInstr), + instr_successor(Instr, NextInstr), phi_instr(NextInstr), instr_block(NextInstr, BB). @@ -89,7 +89,7 @@ _landingpad_first_nonphi(BB, Instr) :- _landingpad_first_nonphi(BB, NextInstr) :- _landingpad_starting_phi(BB, Instr), - next_instr(Instr, NextInstr), + instr_successor(Instr, NextInstr), !phi_instr(NextInstr), instr_block(NextInstr, BB). diff --git a/datalog/schema/ret-instr.dl b/datalog/schema/ret-instr.dl index f722044..2e95b93 100644 --- a/datalog/schema/ret-instr.dl +++ b/datalog/schema/ret-instr.dl @@ -10,13 +10,13 @@ terminator_instr(v) :- ret_instr(v). // The ‘ret‘ instr optionally accepts a single // argument, the return value. -.decl ret_instr_value(instr:RetInstruction, val:Operand) -.decl void_ret_instr(instr:RetInstruction) +.decl ret_instr_operand(instr:RetInstruction, val:Operand) +.decl ret_instr_void_(instr:RetInstruction) schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - void_ret_instr(Instr), - ret_instr_value(Instr, _). + ret_instr_void_(Instr), + ret_instr_operand(Instr, _). //------------------------------------------------------------------------------ @@ -40,14 +40,14 @@ func_is_wellformed(Func):- !func_is_illformed(Func). func_is_illformed(Func) :- - void_ret_instr(Instr), + ret_instr_void_(Instr), instr_func(Instr, Func), func_ty(Func, FuncType), func_type_return(FuncType, RetType), !void_type(RetType). func_is_illformed(Func) :- - ret_instr_value(Instr, Value), + ret_instr_operand(Instr, Value), instr_func(Instr, Func), func_ty(Func, FuncType), func_type_return(FuncType, RetType), @@ -56,7 +56,7 @@ func_is_illformed(Func) :- func_is_illformed(Func) :- ret_instr(Instr), - !void_ret_instr(Instr), + !ret_instr_void_(Instr), instr_func(Instr, Func), func_ty(Func, FuncType), func_type_return(FuncType, RetType), @@ -71,5 +71,5 @@ func_is_illformed(Func) :- schema_invalid_instr(Instr, __FILE__, __LINE__) :- schema_sanity(), - ret_instr_value(Instr, Value), + ret_instr_operand(Instr, Value), !operand_is_firstclass(Value).