@@ -31,20 +31,44 @@ public class AbstractMemory implements ValueDomain<AbstractMemory>, BaseLattice<
3131 public static final AbstractMemory BOTTOM = new AbstractMemory (null );
3232 public static final AbstractMemory TOP = new AbstractMemory (null , true );
3333
34+ /**
35+ * Constructs an empty Abstract Memory.
36+ */
3437 public AbstractMemory () {
3538 this (new AbstractByte [0 ]);
3639 }
3740
41+ /**
42+ * Constructs an Abstract Memory with the given memory array.
43+ *
44+ * @param memory the array of abstract bytes representing the memory
45+ */
3846 public AbstractMemory (AbstractByte [] memory ) {
3947 this .memory = memory ;
4048 this .isTop = false ;
4149 }
4250
51+ /**
52+ * Constructs an Abstract Memory with the given memory array and Top flag.
53+ *
54+ * @param memory the array of abstract bytes representing the memory
55+ * @param isTop if true, this instance represents the Top element
56+ */
4357 public AbstractMemory (AbstractByte [] memory , boolean isTop ) {
4458 this .memory = memory ;
4559 this .isTop = isTop ;
4660 }
4761
62+ /**
63+ * Stores a 32-byte word in memory at the specified offset (MSTORE
64+ * operation).
65+ *
66+ * @param offset the memory offset where the value should be stored
67+ * @param e the stack element to store
68+ *
69+ * @return a new Abstract Memory with the stored value, or TOP/BOTTOM if the
70+ * operation cannot be performed
71+ */
4872 public AbstractMemory mstore (StackElement offset , StackElement e ) {
4973 if (offset .isTop () || offset .isTopNotJumpdest ()) {
5074 log .warn ("Offset is TOP, ignoring mstore with offset {}, value {}." , offset , e );
@@ -80,6 +104,16 @@ public AbstractMemory mstore(StackElement offset, StackElement e) {
80104 }
81105 }
82106
107+ /**
108+ * Stores a single byte in memory at the specified offset (MSTORE8
109+ * operation).
110+ *
111+ * @param offset the memory offset where the byte should be stored
112+ * @param value the stack element containing the byte value to store
113+ *
114+ * @return a new Abstract Memory with the stored byte, or TOP/BOTTOM if the
115+ * operation cannot be performed
116+ */
83117 public AbstractMemory mstore8 (StackElement offset , StackElement value ) {
84118 if (offset .isTop () || offset .isTopNotJumpdest ()) {
85119 log .warn ("Offset is TOP, ignoring mstore8 with offset {}, value {}." , offset , value );
@@ -109,6 +143,15 @@ public AbstractMemory mstore8(StackElement offset, StackElement value) {
109143 return new AbstractMemory (newMemory );
110144 }
111145
146+ /**
147+ * Loads a 32-byte word from memory at the specified offset (MLOAD
148+ * operation).
149+ *
150+ * @param offset the memory offset from which to load the value
151+ *
152+ * @return a stack element containing the loaded value, or TOP/BOTTOM if the
153+ * operation cannot be performed
154+ */
112155 public StackElement mload (StackElement offset ) {
113156 if (offset .compareTo (new StackElement (MAX_MEMORY_SIZE )) >= 0 ) {
114157 log .warn ("Offset is greater than max memory size, ignoring mload with offset {}." , offset );
@@ -131,6 +174,16 @@ public StackElement mload(StackElement offset) {
131174 return StackElement .fromBytes (result );
132175 }
133176
177+ /**
178+ * Copies memory from one location to another (MCOPY operation).
179+ *
180+ * @param destOffset the destination offset in memory
181+ * @param srcOffset the source offset in memory
182+ * @param length the number of bytes to copy
183+ *
184+ * @return a new Abstract Memory with the copied data, or TOP/BOTTOM if the
185+ * operation cannot be performed
186+ */
134187 public AbstractMemory mcopy (StackElement destOffset , StackElement srcOffset , StackElement length ) {
135188 if (length .compareTo (new StackElement (MAX_MEMORY_SIZE )) >= 0 ) {
136189 log .warn (
@@ -180,6 +233,14 @@ public AbstractMemory mcopy(StackElement destOffset, StackElement srcOffset, Sta
180233 return new AbstractMemory (newMemory );
181234 }
182235
236+ /**
237+ * Ensures that the memory array has at least the specified capacity,
238+ * aligned to 32-byte boundaries.
239+ *
240+ * @param size the minimum required size
241+ *
242+ * @return an array of abstract bytes with at least the specified capacity
243+ */
183244 private AbstractByte [] ensureCapacity (int size ) {
184245 int alignedSize = ((size + 31 ) / 32 ) * 32 ;
185246 if (alignedSize <= memory .length )
@@ -359,6 +420,14 @@ else if (isBottom())
359420 return new StringRepresentation (hexString .toString ());
360421 }
361422
423+ /**
424+ * Converts an array of abstract bytes to its hexadecimal string
425+ * representation.
426+ *
427+ * @param bytes the array of abstract bytes to print
428+ *
429+ * @return the hexadecimal string representation of the bytes
430+ */
362431 static public String printBytes (AbstractByte [] bytes ) {
363432 StringBuilder hexString = new StringBuilder ();
364433 for (AbstractByte b : bytes )
@@ -368,6 +437,13 @@ static public String printBytes(AbstractByte[] bytes) {
368437 return hexString .toString ();
369438 }
370439
440+ /**
441+ * Converts a stack element to a 32-byte array representation.
442+ *
443+ * @param element the stack element to convert
444+ *
445+ * @return an array of 32 abstract bytes representing the element
446+ */
371447 private AbstractByte [] convertStackElementToBytes (StackElement element ) {
372448 AbstractByte [] bytes = new AbstractByte [32 ];
373449 BigInteger bigIntValue = Number .toBigInteger (element .getNumber ());
@@ -377,26 +453,56 @@ private AbstractByte[] convertStackElementToBytes(StackElement element) {
377453 return bytes ;
378454 }
379455
456+ /**
457+ * Creates a 32-byte array filled with unknown (TOP) bytes.
458+ *
459+ * @return an array of 32 abstract bytes all set to UNKNOWN
460+ */
380461 private AbstractByte [] unknownBytes () {
381462 AbstractByte [] bytes = new AbstractByte [32 ];
382463 for (int i = 0 ; i < 32 ; i ++)
383464 bytes [i ] = AbstractByte .UNKNOWN ;
384465 return bytes ;
385466 }
386467
468+ /**
469+ * Fills an array of abstract bytes with a specific byte value.
470+ *
471+ * @param bytes the array to fill
472+ * @param value the byte value to fill the array with
473+ */
387474 public static void fill (AbstractByte [] bytes , byte value ) {
388475 for (int i = 0 ; i < bytes .length ; i ++) {
389476 bytes [i ] = new AbstractByte (value );
390477 }
391478 }
392479
480+ /**
481+ * Checks if any byte in the array is unknown (TOP).
482+ *
483+ * @param bytes the array of abstract bytes to check
484+ *
485+ * @return true if any byte is TOP, false otherwise
486+ */
393487 public static boolean isUnknown (AbstractByte [] bytes ) {
394488 for (int i = 0 ; i < 32 ; i ++)
395489 if (bytes [i ].isTop ())
396490 return true ;
397491 return false ;
398492 }
399493
494+ /**
495+ * Reads a sequence of bytes from memory at the specified offset.
496+ *
497+ * @param offset the starting offset in memory
498+ * @param length the number of bytes to read
499+ *
500+ * @return an array of bytes read from memory, or null if any byte is
501+ * unknown (TOP)
502+ *
503+ * @throws IllegalArgumentException if offset or length is negative, or if
504+ * the read exceeds maximum memory size
505+ */
400506 public byte [] readBytes (int offset , int length ) {
401507 if (offset < 0 || length < 0 )
402508 throw new IllegalArgumentException ("Negative offset or length" );
0 commit comments