@@ -245,324 +245,100 @@ public TaintAbstractStack smallStepSemantics(ValueExpression expression, Program
245245 }
246246
247247 case "Dup1Operator" : { // DUP1
248- if (hasBottomUntil (1 ))
249- return BOTTOM ;
250- TaintAbstractStack resultStack = dupX (1 , clone ());
251-
252- if (resultStack .isEmpty ())
253- return BOTTOM ;
254- else
255- return resultStack ;
248+ return dupXoperator (1 , clone ());
256249 }
257250 case "Dup2Operator" : { // DUP2
258- if (hasBottomUntil (2 ))
259- return BOTTOM ;
260- TaintAbstractStack resultStack = dupX (2 , clone ());
261-
262- if (resultStack .isEmpty ())
263- return BOTTOM ;
264- else
265- return resultStack ;
251+ return dupXoperator (2 , clone ());
266252 }
267253 case "Dup3Operator" : { // DUP3
268- if (hasBottomUntil (3 ))
269- return BOTTOM ;
270- TaintAbstractStack resultStack = dupX (3 , clone ());
271-
272- if (resultStack .isEmpty ())
273- return BOTTOM ;
274- else
275- return resultStack ;
254+ return dupXoperator (3 , clone ());
276255 }
277256 case "Dup4Operator" : { // DUP4
278- if (hasBottomUntil (4 ))
279- return BOTTOM ;
280- TaintAbstractStack resultStack = dupX (4 , clone ());
281-
282- if (resultStack .isEmpty ())
283- return BOTTOM ;
284- else
285- return resultStack ;
257+ return dupXoperator (4 , clone ());
286258 }
287259 case "Dup5Operator" : { // DUP5
288- if (hasBottomUntil (5 ))
289- return BOTTOM ;
290- TaintAbstractStack resultStack = dupX (5 , clone ());
291-
292- if (resultStack .isEmpty ())
293- return BOTTOM ;
294- else
295- return resultStack ;
260+ return dupXoperator (5 , clone ());
296261 }
297262 case "Dup6Operator" : { // DUP6
298- if (hasBottomUntil (6 ))
299- return BOTTOM ;
300- TaintAbstractStack resultStack = dupX (6 , clone ());
301-
302- if (resultStack .isEmpty ())
303- return BOTTOM ;
304- else
305- return resultStack ;
263+ return dupXoperator (6 , clone ());
306264 }
307265 case "Dup7Operator" : { // DUP7
308- if (hasBottomUntil (7 ))
309- return BOTTOM ;
310- TaintAbstractStack resultStack = dupX (7 , clone ());
311-
312- if (resultStack .isEmpty ())
313- return BOTTOM ;
314- else
315- return resultStack ;
266+ return dupXoperator (7 , clone ());
316267 }
317268 case "Dup8Operator" : { // DUP8
318- if (hasBottomUntil (8 ))
319- return BOTTOM ;
320- TaintAbstractStack resultStack = dupX (8 , clone ());
321-
322- if (resultStack .isEmpty ())
323- return BOTTOM ;
324- else
325- return resultStack ;
269+ return dupXoperator (8 , clone ());
326270 }
327271 case "Dup9Operator" : { // DUP9
328- if (hasBottomUntil (9 ))
329- return BOTTOM ;
330- TaintAbstractStack resultStack = dupX (9 , clone ());
331-
332- if (resultStack .isEmpty ())
333- return BOTTOM ;
334- else
335- return resultStack ;
272+ return dupXoperator (9 , clone ());
336273 }
337274 case "Dup10Operator" : { // DUP10
338- if (hasBottomUntil (10 ))
339- return BOTTOM ;
340- TaintAbstractStack resultStack = dupX (10 , clone ());
341-
342- if (resultStack .isEmpty ())
343- return BOTTOM ;
344- else
345- return resultStack ;
275+ return dupXoperator (10 , clone ());
346276 }
347277 case "Dup11Operator" : { // DUP11
348- if (hasBottomUntil (11 ))
349- return BOTTOM ;
350- TaintAbstractStack resultStack = dupX (11 , clone ());
351-
352- if (resultStack .isEmpty ())
353- return BOTTOM ;
354- else
355- return resultStack ;
278+ return dupXoperator (11 , clone ());
356279 }
357280 case "Dup12Operator" : { // DUP12
358- if (hasBottomUntil (12 ))
359- return BOTTOM ;
360- TaintAbstractStack resultStack = dupX (12 , clone ());
361-
362- if (resultStack .isEmpty ())
363- return BOTTOM ;
364- else
365- return resultStack ;
281+ return dupXoperator (12 , clone ());
366282 }
367283 case "Dup13Operator" : { // DUP13
368- if (hasBottomUntil (13 ))
369- return BOTTOM ;
370- TaintAbstractStack resultStack = dupX (13 , clone ());
371-
372- if (resultStack .isEmpty ())
373- return BOTTOM ;
374- else
375- return resultStack ;
284+ return dupXoperator (13 , clone ());
376285 }
377286 case "Dup14Operator" : { // DUP14
378- if (hasBottomUntil (14 ))
379- return BOTTOM ;
380- TaintAbstractStack resultStack = dupX (14 , clone ());
381-
382- if (resultStack .isEmpty ())
383- return BOTTOM ;
384- else
385- return resultStack ;
287+ return dupXoperator (14 , clone ());
386288 }
387289 case "Dup15Operator" : { // DUP15
388- if (hasBottomUntil (15 ))
389- return BOTTOM ;
390- TaintAbstractStack resultStack = dupX (15 , clone ());
391-
392- if (resultStack .isEmpty ())
393- return BOTTOM ;
394- else
395- return resultStack ;
290+ return dupXoperator (15 , clone ());
396291 }
397292 case "Dup16Operator" : { // DUP16
398- if (hasBottomUntil (16 ))
399- return BOTTOM ;
400- TaintAbstractStack resultStack = dupX (16 , clone ());
401-
402- if (resultStack .isEmpty ())
403- return BOTTOM ;
404- else
405- return resultStack ;
293+ return dupXoperator (16 , clone ());
406294 }
407295 case "Swap1Operator" : { // SWAP1
408- if (hasBottomUntil (1 ))
409- return BOTTOM ;
410- TaintAbstractStack resultStack = swapX (1 , clone ());
411-
412- if (resultStack .isEmpty ())
413- return BOTTOM ;
414- else
415- return resultStack ;
296+ return swapXoperator (1 , clone ());
416297 }
417298 case "Swap2Operator" : { // SWAP2
418- if (hasBottomUntil (2 ))
419- return BOTTOM ;
420- TaintAbstractStack resultStack = swapX (2 , clone ());
421-
422- if (resultStack .isEmpty ())
423- return BOTTOM ;
424- else
425- return resultStack ;
299+ return swapXoperator (2 , clone ());
426300 }
427301 case "Swap3Operator" : { // SWAP3
428- if (hasBottomUntil (3 ))
429- return BOTTOM ;
430- TaintAbstractStack resultStack = swapX (3 , clone ());
431-
432- if (resultStack .isEmpty ())
433- return BOTTOM ;
434- else
435- return resultStack ;
302+ return swapXoperator (3 , clone ());
436303 }
437304 case "Swap4Operator" : { // SWAP4
438- if (hasBottomUntil (4 ))
439- return BOTTOM ;
440- TaintAbstractStack resultStack = swapX (4 , clone ());
441-
442- if (resultStack .isEmpty ())
443- return BOTTOM ;
444- else
445- return resultStack ;
305+ return swapXoperator (4 , clone ());
446306 }
447307 case "Swap5Operator" : { // SWAP5
448- if (hasBottomUntil (5 ))
449- return BOTTOM ;
450- TaintAbstractStack resultStack = swapX (5 , clone ());
451-
452- if (resultStack .isEmpty ())
453- return BOTTOM ;
454- else
455- return resultStack ;
308+ return swapXoperator (5 , clone ());
456309 }
457310 case "Swap6Operator" : { // SWAP6
458- if (hasBottomUntil (6 ))
459- return BOTTOM ;
460- TaintAbstractStack resultStack = swapX (6 , clone ());
461-
462- if (resultStack .isEmpty ())
463- return BOTTOM ;
464- else
465- return resultStack ;
311+ return swapXoperator (6 , clone ());
466312 }
467313 case "Swap7Operator" : { // SWAP7
468- if (hasBottomUntil (7 ))
469- return BOTTOM ;
470- TaintAbstractStack resultStack = swapX (7 , clone ());
471-
472- if (resultStack .isEmpty ())
473- return BOTTOM ;
474- else
475- return resultStack ;
314+ return swapXoperator (7 , clone ());
476315 }
477316 case "Swap8Operator" : { // SWAP8
478- if (hasBottomUntil (8 ))
479- return BOTTOM ;
480- TaintAbstractStack resultStack = swapX (8 , clone ());
481-
482- if (resultStack .isEmpty ())
483- return BOTTOM ;
484- else
485- return resultStack ;
317+ return swapXoperator (8 , clone ());
486318 }
487319 case "Swap9Operator" : { // SWAP9
488- if (hasBottomUntil (9 ))
489- return BOTTOM ;
490- TaintAbstractStack resultStack = swapX (9 , clone ());
491-
492- if (resultStack .isEmpty ())
493- return BOTTOM ;
494- else
495- return resultStack ;
320+ return swapXoperator (9 , clone ());
496321 }
497322 case "Swap10Operator" : { // SWAP10
498- if (hasBottomUntil (10 ))
499- return BOTTOM ;
500- TaintAbstractStack resultStack = swapX (10 , clone ());
501-
502- if (resultStack .isEmpty ())
503- return BOTTOM ;
504- else
505- return resultStack ;
323+ return swapXoperator (10 , clone ());
506324 }
507325 case "Swap11Operator" : { // SWAP11
508- if (hasBottomUntil (11 ))
509- return BOTTOM ;
510- TaintAbstractStack resultStack = swapX (11 , clone ());
511-
512- if (resultStack .isEmpty ())
513- return BOTTOM ;
514- else
515- return resultStack ;
326+ return swapXoperator (11 , clone ());
516327 }
517328 case "Swap12Operator" : { // SWAP12
518- if (hasBottomUntil (12 ))
519- return BOTTOM ;
520- TaintAbstractStack resultStack = swapX (12 , clone ());
521-
522- if (resultStack .isEmpty ())
523- return BOTTOM ;
524- else
525- return resultStack ;
329+ return swapXoperator (12 , clone ());
526330 }
527331 case "Swap13Operator" : { // SWAP13
528- if (hasBottomUntil (13 ))
529- return BOTTOM ;
530- TaintAbstractStack resultStack = swapX (13 , clone ());
531-
532- if (resultStack .isEmpty ())
533- return BOTTOM ;
534- else
535- return resultStack ;
332+ return swapXoperator (13 , clone ());
536333 }
537334 case "Swap14Operator" : { // SWAP14
538- if (hasBottomUntil (14 ))
539- return BOTTOM ;
540- TaintAbstractStack resultStack = swapX (14 , clone ());
541-
542- if (resultStack .isEmpty ())
543- return BOTTOM ;
544- else
545- return resultStack ;
335+ return swapXoperator (14 , clone ());
546336 }
547337 case "Swap15Operator" : { // SWAP15
548- if (hasBottomUntil (15 ))
549- return BOTTOM ;
550- TaintAbstractStack resultStack = swapX (15 , clone ());
551-
552- if (resultStack .isEmpty ())
553- return BOTTOM ;
554- else
555- return resultStack ;
338+ return swapXoperator (15 , clone ());
556339 }
557340 case "Swap16Operator" : { // SWAP16
558- if (hasBottomUntil (16 ))
559- return BOTTOM ;
560- TaintAbstractStack resultStack = swapX (16 , clone ());
561-
562- if (resultStack .isEmpty ())
563- return BOTTOM ;
564- else
565- return resultStack ;
341+ return swapXoperator (16 , clone ());
566342 }
567343 case "Log0Operator" : { // LOG0
568344 // At the moment, we do not handle LOG0
@@ -894,6 +670,18 @@ public TaintAbstractStack smallStepSemantics(ValueExpression expression, Program
894670 return top ();
895671 }
896672
673+ private TaintAbstractStack dupXoperator (int x , TaintAbstractStack stack ) {
674+ if (stack .isEmpty () || stack .hasBottomUntil (x ))
675+ return BOTTOM ;
676+ return dupX (x , stack .clone ());
677+ }
678+
679+ private TaintAbstractStack swapXoperator (int x , TaintAbstractStack stack ) {
680+ if (stack .isEmpty () || stack .hasBottomUntil (x ))
681+ return BOTTOM ;
682+ return swapX (x , stack .clone ());
683+ }
684+
897685 private TaintAbstractStack swapX (int x , TaintAbstractStack stack ) {
898686 List <TaintElement > clone = stack .clone ().getStack ();
899687
0 commit comments