@@ -129,8 +129,10 @@ public RelationalTaintAbstractDomain smallStepSemantics(ValueExpression expressi
129129 case "PushOperator" :
130130 case "Push0Operator" : {
131131 RelationalTaintAbstractDomain resultStack = clone ();
132- if (this .isTainted ((Statement ) pp ))
133- resultStack .push (RelationalTaintElement .TAINT );
132+ Statement stmt = (Statement ) pp ;
133+ if (this .isTainted (stmt ))
134+ resultStack .push (RelationalTaintElement
135+ .newRelationalTaintedElement (((ProgramCounterLocation ) stmt .getLocation ()).getPc ()));
134136 else
135137 resultStack .push (RelationalTaintElement .CLEAN );
136138 return resultStack ;
@@ -181,8 +183,10 @@ public RelationalTaintAbstractDomain smallStepSemantics(ValueExpression expressi
181183 RelationalTaintAbstractDomain resultStack = clone ();
182184 resultStack .popX (3 );
183185
184- if (this .isTainted ((Statement ) pp ))
185- return mk (resultStack .stack , RelationalTaintElement .TAINT );
186+ Statement stmt = (Statement ) pp ;
187+ if (this .isTainted (stmt ))
188+ return mk (resultStack .stack , RelationalTaintElement
189+ .newRelationalTaintedElement (((ProgramCounterLocation ) stmt .getLocation ()).getPc ()));
186190
187191 return resultStack ;
188192 }
@@ -192,19 +196,7 @@ public RelationalTaintAbstractDomain smallStepSemantics(ValueExpression expressi
192196 case "BlockhashOperator" :
193197 case "NotOperator" :
194198 case "SloadOperator" :
195- case "IszeroOperator" : { // pop 1, push 1
196- if (hasBottomUntil (1 ))
197- return bottom ();
198-
199- RelationalTaintAbstractDomain resultStack = clone ();
200- RelationalTaintElement opnd1 = resultStack .pop ();
201- if (this .isTainted ((Statement ) pp ))
202- resultStack .push (RelationalTaintElement .TAINT );
203- else
204- resultStack .push (RelationalTaintElement .semantics (opnd1 ));
205- return resultStack ;
206- }
207-
199+ case "IszeroOperator" :
208200 case "CalldataloadOperator" : { // pop 1, push 1
209201 if (hasBottomUntil (1 ))
210202 return bottom ();
@@ -227,7 +219,7 @@ public RelationalTaintAbstractDomain smallStepSemantics(ValueExpression expressi
227219 RelationalTaintAbstractDomain resultStack = clone ();
228220 resultStack .pop ();
229221 if (memory .isTaint ())
230- resultStack .push (RelationalTaintElement .TAINT );
222+ resultStack .push (RelationalTaintElement .newRelationalTaintedElement ( memory . getProgramPoints ()) );
231223 else if (memory .isClean ())
232224 resultStack .push (RelationalTaintElement .CLEAN );
233225
@@ -243,7 +235,8 @@ else if (memory.isClean())
243235 RelationalTaintElement value = resultStack .pop ();
244236
245237 if (value .isTaint ())
246- return mk (resultStack .stack , RelationalTaintElement .TAINT );
238+ return mk (resultStack .stack ,
239+ RelationalTaintElement .newRelationalTaintedElement (value .getProgramPoints ()));
247240 else if (value .isClean ())
248241 return resultStack ;
249242 }
@@ -464,8 +457,10 @@ else if (value.isClean())
464457 RelationalTaintElement offset = resultStack .pop ();
465458 RelationalTaintElement length = resultStack .pop ();
466459
467- if (this .isTainted ((Statement ) pp ))
468- resultStack .push (RelationalTaintElement .TAINT );
460+ Statement stmt = (Statement ) pp ;
461+ if (this .isTainted (stmt ))
462+ resultStack .push (RelationalTaintElement
463+ .newRelationalTaintedElement (((ProgramCounterLocation ) stmt .getLocation ()).getPc ()));
469464 else
470465 resultStack .push (RelationalTaintElement .semantics (value , offset , length ));
471466 return resultStack ;
@@ -479,8 +474,10 @@ else if (value.isClean())
479474 RelationalTaintElement length = resultStack .pop ();
480475 RelationalTaintElement salt = resultStack .pop ();
481476
482- if (this .isTainted ((Statement ) pp ))
483- resultStack .push (RelationalTaintElement .TAINT );
477+ Statement stmt = (Statement ) pp ;
478+ if (this .isTainted (stmt ))
479+ resultStack .push (RelationalTaintElement
480+ .newRelationalTaintedElement (((ProgramCounterLocation ) stmt .getLocation ()).getPc ()));
484481 else
485482 resultStack .push (RelationalTaintElement .semantics (value , offset , length , salt ));
486483 return resultStack ;
@@ -498,8 +495,10 @@ else if (value.isClean())
498495 RelationalTaintElement outOffset = resultStack .pop ();
499496 RelationalTaintElement outLength = resultStack .pop ();
500497
501- if (this .isTainted ((Statement ) pp ))
502- resultStack .push (RelationalTaintElement .TAINT );
498+ Statement stmt = (Statement ) pp ;
499+ if (this .isTainted (stmt ))
500+ resultStack .push (RelationalTaintElement
501+ .newRelationalTaintedElement (((ProgramCounterLocation ) stmt .getLocation ()).getPc ()));
503502 else
504503 resultStack
505504 .push (RelationalTaintElement .semantics (gas , to , value , inOffset , inLength , outOffset ,
@@ -527,8 +526,10 @@ else if (value.isClean())
527526 RelationalTaintElement outOffset = resultStack .pop ();
528527 RelationalTaintElement outLength = resultStack .pop ();
529528
530- if (this .isTainted ((Statement ) pp ))
531- resultStack .push (RelationalTaintElement .TAINT );
529+ Statement stmt = (Statement ) pp ;
530+ if (this .isTainted (stmt ))
531+ resultStack .push (RelationalTaintElement
532+ .newRelationalTaintedElement (((ProgramCounterLocation ) stmt .getLocation ()).getPc ()));
532533 else
533534 resultStack .push (
534535 RelationalTaintElement .semantics (gas , to , inOffset , inLength , outOffset , outLength ));
@@ -567,8 +568,10 @@ else if (value.isClean())
567568 RelationalTaintAbstractDomain resultStack = clone ();
568569 RelationalTaintElement address = resultStack .pop ();
569570
570- if (this .isTainted ((Statement ) pp ))
571- resultStack .push (RelationalTaintElement .TAINT );
571+ Statement stmt = (Statement ) pp ;
572+ if (this .isTainted (stmt ))
573+ resultStack .push (RelationalTaintElement
574+ .newRelationalTaintedElement (((ProgramCounterLocation ) stmt .getLocation ()).getPc ()));
572575 else
573576 resultStack .push (RelationalTaintElement .semantics (address ));
574577 return resultStack ;
@@ -595,8 +598,10 @@ else if (value.isClean())
595598 RelationalTaintAbstractDomain resultStack = clone ();
596599 RelationalTaintElement address = resultStack .pop ();
597600
598- if (this .isTainted ((Statement ) pp ))
599- resultStack .push (RelationalTaintElement .TAINT );
601+ Statement stmt = (Statement ) pp ;
602+ if (this .isTainted (stmt ))
603+ resultStack .push (RelationalTaintElement
604+ .newRelationalTaintedElement (((ProgramCounterLocation ) stmt .getLocation ()).getPc ()));
600605 else
601606 resultStack .push (RelationalTaintElement .semantics (address ));
602607 return resultStack ;
0 commit comments