@@ -467,8 +467,6 @@ def __init__(self, pag: pysvf.SVFIR):
467467 self .flippedAddressMask = (self .addressMask ^ 0xffffffff )
468468
469469
470-
471- #==============Don't modify the code below==============
472470 """
473471 Initialize the WTO (Weak topological order) for each function.
474472 """
@@ -796,6 +794,7 @@ def analyse(self):
796794
797795 wto = self .func_to_wto [main_fun ]
798796 self .handle_wto_components (wto .components )
797+ self .ensure_all_asserts_validated ()
799798
800799
801800 """
@@ -999,55 +998,6 @@ def update_state_on_ret(self, ret: pysvf.RetPE):
999998
1000999
10011000
1002-
1003- """
1004- Find the comparison predicates in "class BinaryOPStmt:OpCode" under SVF/svf/include/SVFIR/SVFStatements.h
1005- You are required to handle predicates (The program is assumed to have signed ints and also interger-overflow-free),
1006- including Add, FAdd, Sub, FSub, Mul, FMul, SDiv, FDiv, UDiv, SRem, FRem, URem, Xor, And, Or, AShr, Shl, LShr
1007- """
1008- def update_state_on_binary (self , binary : pysvf .BinaryOPStmt ):
1009- node = binary .get_icfg_node ()
1010- abstract_state = self .post_abs_trace [node ]
1011- lhs = binary .get_res_id ()
1012- op1 = binary .get_op_var (0 )
1013- op2 = binary .get_op_var (1 )
1014- assert abstract_state .is_interval (op1 .get_id ()) and abstract_state .is_interval (op2 .get_id ())
1015- result = IntervalValue (0 )
1016- val1 = abstract_state [op1 .get_id ()].get_interval ()
1017- val2 = abstract_state [op2 .get_id ()].get_interval ()
1018- assert (isinstance (val1 , IntervalValue ) and isinstance (val2 , IntervalValue ))
1019- if binary .get_op () == OpCode .Add or binary .get_op () == OpCode .FAdd :
1020- result = val1 + val2
1021- elif binary .get_op () == OpCode .Sub or binary .get_op () == OpCode .FSub :
1022- result = val1 - val2
1023- elif binary .get_op () == OpCode .Mul or binary .get_op () == OpCode .FMul :
1024- result = val1 * val2
1025- elif binary .get_op () == OpCode .UDiv or binary .get_op () == OpCode .SDiv or binary .get_op () == OpCode .FDiv :
1026- if int (val2 .ub ())>= 0 and int (val2 .lb ()) <= 0 :
1027- result = IntervalValue .top ()
1028- else :
1029- result = val1 / val2
1030- elif binary .get_op () == OpCode .SRem or binary .get_op () == OpCode .FRem or binary .get_op () == OpCode .URem :
1031- if int (val2 .ub ())>= 0 and int (val2 .lb ()) <= 0 :
1032- result = IntervalValue .top ()
1033- else :
1034- result = val1 % val2
1035- elif binary .get_op () == OpCode .Xor :
1036- result = val1 ^ val2
1037- elif binary .get_op () == OpCode .Or :
1038- result = val1 | val2
1039- elif binary .get_op () == OpCode .And :
1040- result = val1 & val2
1041- elif binary .get_op () == OpCode .Shl :
1042- result = val1 << val2
1043- elif binary .get_op () == OpCode .LShr or binary .get_op () == OpCode .AShr :
1044- result = val1 >> val2
1045- else :
1046- result = IntervalValue .top ()
1047- abstract_state [lhs ] = AbstractValue (result )
1048-
1049-
1050-
10511001 def update_state_on_select (self , select : pysvf .SelectStmt ):
10521002 node = select .get_icfg_node ()
10531003 abstract_state = self .post_abs_trace [node ]
0 commit comments