[Question][Hw2] Clarifications needed on `semantics.ml` codes

[yusungsim]

I have several questions to clarify my understanding on semantics.ml codes.

1. Types of functions

Because there were no type annotations on the skeleton code, I want to check types of functions in the code.

eval: llvalue -> Memory -> Value
execute_block: (llbasicblock * llvalue) option -> llbasicblock -> Memory -> Memory
execute_instr: (llbasicblock * llvalue) option -> (llbasicblock  * llvalue) llpos -> Memory -> Memory
transfer: (llbasicblock * llvalue) option -> llvalue -> Memory -> Memory

Although it is not explicitly shown in the code or document, I think execute_block, execute_instr, transfer functions should have Memory return types, because it is implementing transitional semantics.
Are these correct types?

2. Iterating through instructions in block

In execute_block function, execute_instr function is only once on the first instructions. This means that in order to compute total result of a block, there should be some kind of iteration through instructions in the block in execute_instr or transfer function. However we only have rooms to implement in transfer function, at each pattern cases. Does this mean that we need some recursion to iterate through the block? In addition, can we change the parts of codes other than failwith "Not implemented" so that this iteration can be efficiently implemented?

3. Distinguishing Int (Int32) and Bool (Int 1) in eval function

Readme mentions that Int32 should be interpreted as Integer constant and Int1 should be interpreted as Bool. This should happen when matching ValueKind of expression in eval function. Given only e: llvalue which is matched to ValueKind.ConstantInt, how can we known that it's Int32 or Int1?

[yusungsim]

I just found out that (llbasicblock * llvalue) option types should be fixed to (llbasicblock * Memory) option types in the original question, but don't understand why Memory type is needed there.

[Maokami]

1. I think you are right about the types of the functions (with the correction). The reason why there is a memory type is because of the evaluation of the PHI Node .
2. The following may be not the exact answer to your question, but I will just share my interpretation of these functions:
   I think the skeleton codes totally follows the given operational semantics. (See 4. Semantics)
   The execute_instr function checks what the command of the given label is and passes it over to the transfer function.
   The transfer function interprets given commend, and *execute the next label.
   If the * part is implemented properly, I think there will be no need to fix the skeleton code. (I wonder if this is the answer related to your question...)
3. I want to know this, too!

[kangwoosukeq]

1. In our final implementation, the types of functions are

eval : Llvm.llvalue -> Memory.t -> Value.t
execute_block : (Llvm.llbasicblock * Memory.t) option -> Llvm.llbasicblock -> Memory.t -> Memory.t
execute_instr : (Llvm.llbasicblock * Memory.t) option -> (Llvm.llbasicblock, Llvm.llvalue) Llvm.llpos -> Memory.t -> Memory.t
transfer : (Llvm.llbasicblock * Memory.t) option -> Llvm.llvalue -> Memory.t -> Memory.t

So I think your type inference is almost correct, and the Memory type in prev will be used for PHI Node evaluation as @workstudy-zero said.

2. Actually, you don't have to change the structure of the skeleton code. Basically, the transfer function takes instruction and memory, then interprets the instruction to calculate new memory. This memory will be passed to the next instruction (or block). Since the execute_block, execute_instr, and transfer functions are defined mutually recursive, you can call them in each other.

3. You can assume Valuekind.ConstantInt only accepts Int, so you don't have to distinguish them in the source code. The Bool value can be generated by comparison operators only.