Bob Simulator

The Bob simulator is as found here. In shorts we have a limited amount of memory and an unlimited amount of registers. Each slot has integer size (The simulator is written in JavaScript, so we use JS integers). After each execution the values of all registers prefixed with res. are stored internally (they are compared to a set of expected values) after which these registers are zero-cleared. All other registers and the memory is left as is.

Memory Handling

As stated Janus has a pass by reference policy. We implement this by solely using the stack part of memory. Our Bob model has a stack that grows bottom up as opposed to a normal x86 stack. This we have to take into account when translating: if we want to index into some array like so a[21] we add 21 to the address of the head of the array.

Resetting Branch Register

If a given jump is taken, we need to reset the branch register. Or else we keep on jumping ahead into undefined behavior. This is often done using a BRA instruction, as thus

l1: BNEQ $reg1 $reg2 some_label # code some_label: BRA l1 # continue

Zero Clearing Values

Before we dive into the translation, we need to discuss the need for zero clearing used registers and memory slots. The Bob simulator being reversible do not have any way move or overwrite registers or memory locations (described here). Thus the only way to store a value in a register is to either add, subtract or exclusive or the value into the register. Say we have the following Bob code within some loop (the condition could be 4 != x)

XORI $reg_1 4 l1: BNEQ $reg_1 $reg_x some_label

Now if we take the branch and do not zero-clear $reg_1, during next iteration of the same code we store the value 4 ^ 4 = 0 in $reg_1. If we expect $reg_1 to be 4, this behavior is undefined: we can't predict what will happen. To properly stay clear of this situation, we must clean up both if the branch is taken, and if it isn't. So we get

XORI $reg_1 4 l1: BNEQ $reg_1 $reg_x some_label XORI $reg_1 4 # clean up right away # code some_label: BRA l1 XORI $reg_1 4 #clean up if

This also applies on a global scale: if some Bob program does not clean up after execution, we might end up with undefined behavior if registers are reused. As stated above the simulator only zero-clears res. registers.

Zero-clearing has some interesting properties:

Tranlating Using Templates

We translate using a set of templates. Each Janus construct is made in order to conform to its syntax. So we translate each syntactic construct into predefined Bob code. Some of these translations are here illustrated with flow charts.


Figure 1: Flowchart of a reversible assembly procedure.

Translates into

# template for procedure l_top: BRA proc_bot POP $raddr l: SWRET $raddr NEG $raddr PUSH $raddr # procedure code l_bot: BRA proc_top

Conditional Statements

Figure 2: Flowchart of reversible if-fi conditions

Translates into

if_top: BGEZ $if if_else #code for then if_then: BRA if_bot if_else: BRA if_top # code for else if_bot: BGEZ $fi if_then


Figure 3: Flowchart of reversible for-loop

Translates into

loop_top: BGEZ $entry loop # code for do loop_do: BLZ $exit loop_bot # code for loop loop: BRA loop_top loop_bot: BRA loop_do

Compare Operators

Figure 4: Flowchart of reversible compare operators in assembly, ⊕

If we need to evaluate a compare operator (⊕ = [ >,<,≥≤,=,≠ ]), we can do so as illustrated in Figure 4. This results in the following code where we need to zero-clear the registers we have used.

c_top_pre: BGT $r1 $r2 c_true_pre c_false_pre: BRA c_bot_pre c_true_pre: BRA c_top_pre XORI $res 1 c_bot_pre: BLE $r1 $r2 c_false_pre # Code that can use $res in condition c_bot_post: BLE $r1 $r2 c_false_pre c_true_post: BRA c_top_pre XORI $res 1 c_false_post: BRA c_bot_pre c_top_post: BGT $r1 $r2 c_true_pre


A local-delocal statement has the form

local int a = 200 + b ... code that has a in scope ... delocal int a = 20

Where local is translated into

... expr result into $e_res_pre ... XOR $temp1 $e_res_pre ; use temp to store res PUSH $temp1 ; push sets $temp1 to 0 XOR $f.a.0 $spointer ; store address ... expr clean up ...

And delocal into

... expr result into $e_res_post ... XOR $f.a.0 $spointer ; unstore address POP $temp1 ; pop resets $temp1 XOR $temp1 $e_res_post ; clean up temp1 ... expr clean up ...

In forward execution if the delocal check does not match, we will not clean the register $temp1 up properly in the resulting Bob code. Thus we end up with undefined behavior.