Skip to content

Commit

Permalink
Fix mutually distrustful example
Browse files Browse the repository at this point in the history
  • Loading branch information
@JuneRousseau
JuneRousseau committed Jun 14, 2024
1 parent f7ba437 commit b3f914f
Show file tree
Hide file tree
Showing 2 changed files with 145 additions and 133 deletions.
2 changes: 1 addition & 1 deletion tests/test_files/case_studies/mutually_distrustful.reg
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
PC := ([R X], Global, 0, 9, 2)
STK := ([R W WL], Local, 0x100, 0x120, 0x11f)
CSP := ([R W WL], Local, 0x100, 0x120, 0x11f)
MTDC := ([R W WL], Local, 0x1000, 0x10000, 0xffff)
276 changes: 144 additions & 132 deletions tests/test_files/case_studies/mutually_distrustful.s
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,12 @@ loader:
#([R W], Global, A_data, A_data_end, A_data) ; CGP_A

loader_main:
mov r0 PC
lea r0 -1
load cgp r0 ; puts CGP_A in CGP
lea r0 -1
load r0 r0
jalr r0 r0 ; jumps to A_main
mov cra PC
lea cra -1
load cgp cra ; puts CGP_A in CGP
lea cra -1
load cra cra
jalr cra cra ; jumps to A_main
fail ; should never been reach, as A_main terminates the program
loader_end:

Expand All @@ -28,41 +28,41 @@ A:
#{9: ([R], Global, C_ext, C_ext_end, C_ext_g)} ; import switcher
A_main:
;; store PCC_A on the stack, will be used to fetch imported entry point
mov r1 PC
lea r1 -3
store stk r1
lea stk -1
mov ct1 PC
lea ct1 -3
store csp ct1
lea csp -1

;; put shared data in argument register r10
load r10 cgp
;; put shared data in argument register ca0
load ca0 cgp

;; fetch switcher entry point in r0
load r0 r1
;; fetch entry point B_f in r1
lea r1 1
load r1 r1
;; jump to B_f with A_data_shared as argument in r10
jalr r0 r0
;; fetch switcher entry point in cra
load cra ct1
;; fetch entry point B_f in ct1
lea ct1 1
load ct1 ct1
;; jump to B_f with A_data_shared as argument in ca0
jalr cra cra

;; write 0x42 in the shared_data
load r1 cgp
store r1 0x42
load ct1 cgp
store ct1 0x42

;; fetch switcher entry point in r0
mov r1 stk
load r1 r1 ; r1 := (RX,Global,A,A_end,A)
load r0 r1
;; fetch entry point C_g in r1
lea r1 2
load r1 r1
;; fetch switcher entry point in cra
mov ct1 csp
load ct1 ct1 ; ct1 := (RX,Global,A,A_end,A)
load cra ct1
;; fetch entry point C_g in ct1
lea ct1 2
load ct1 ct1
;; jump to C_g with no arguments
jalr r0 r0
jalr cra cra

;; assert that shared_data still contains 0x42
load r1 cgp
load r1 r1
sub r1 r1 0x42
jnz r1 2
load ct1 cgp
load ct1 ct1
sub ct1 ct1 0x42
jnz ct1 2
jmp 2
fail
;; assert didn't fail
Expand All @@ -78,10 +78,10 @@ B_h:
#0x00
#0x00
B_f:
store cgp r10
store stk r10 ; tries to use the stack to pass the pointer
mov r22 0xFF
jalr r0 r0
store cgp ca0
store csp ca0 ; tries to use the stack to pass the pointer
mov ca0 0xFF
jalr cra cra
B_end:

C:
Expand All @@ -91,7 +91,7 @@ C_h:
#0x0
C_g:
;; could be any code here
jalr r0 r0
jalr cra cra
C_end:

A_data:
Expand All @@ -118,76 +118,87 @@ A_ext_end:
B_ext:
#([R X], Global, B, B_end, B) ; PCC
#([R W], Global, B_data, B_data_end, B_data) ; CGP
B_ext_f: #(B_f - B) ; offset_f
B_ext_h: #(B_h - B) ; offset_h
B_ext_f: #(10 * (B_f - B) + 1) ; offset_f
B_ext_h: #(10 * (B_f - B) + 0) ; offset_h
B_ext_end:

;; export table compartment C -> exports C_g
C_ext:
#([R X], Global, C, C_end, C) ; PCC
#([R W], Global, C_data, C_data_end, C_data) ; CGP
C_ext_g: #(C_g - C) ; offset_g
C_ext_g: #(10 * (C_g - C) + 0) ; offset_g
C_ext_end:

;;; NOTE The switcher is copy-paste from switcher/switcher.s
;; Concatenate this file at the end of any example that require the switcher
switcher:
#[SU, Global, 9, 10, 9]
switcher_cc:
store stk r20
lea stk -1
store stk r21
lea stk -1
store stk r0
lea stk -1
store stk cgp
getp r20 stk
mov r21 [R W WL]
sub r20 r20 r21
jnz r20 2
store csp cs0
lea csp -1
store csp cs1
lea csp -1
store csp cra
lea csp -1
store csp cgp
getp ct2 csp
mov ctp [R W WL]
sub ct2 ct2 ctp
jnz ct2 2
jmp 2
fail ; r20 :=/= 0, ie. not the right permissions
movsr r21 mtdc
lea r21 -1
store r21 stk
movsr mtdc r21
geta r20 stk ; r20 := a
getb r21 stk ; r21 := b
subseg stk r21 r20 ; stk := (p,g,b,a,a)
zero_stk_init:
sub r20 r21 r20 ; r20 := b-a
mov r21 stk ; r21 := (p,g,b,a,a)
lea r21 r20 ; r21 := (p,g,b,a,b)
zero_stk_loop:
jnz r20 2 ; if (i = 0) then (end of loop), otherwise continue
jmp (zero_stk_end - zero_stk_loop - 1) ;
store r21 0 ; mem[b+i] := 0
lea r21 1 ; r21 := (p,g,b,a,b+i)
add r20 r20 1 ; i := i + 1
zero_stk_loopp:
jmp (zero_stk_loop - zero_stk_loopp)
zero_stk_end:
lea stk -1
getb r21 PC ; b_cc
geta r20 PC ; a_cc
sub r21 r21 r20 ; b_cc - a_cc
mov r20 PC ; r20 := (RX_SR, Global, b_cc, e_cc, a_cc+2)
lea r20 r21 ; r20 := (RX_SR, Global, b_cc, e_cc, b_cc+2)
lea r20 -2 ; r20 := (RX_SR, Global, b_cc, e_cc, b_cc)
load r20 r20 ; r20 := #[SU, Global, 9, 10, 9]
unseal r1 r20 r1 ; r1 := (RO, Global, b_ext, e_ext, a_ext)
load r20 r1 ; r20 := encodeEntry(offset, args)
getb cgp r1 ; cgp := b_ext
geta r21 r1 ; r21 := a_ext
sub r21 cgp r21 ; r21 := b_ext - a_ext
lea r1 r21 ; r1 := (RO, Global, b_ext, e_ext, b_ext)
load r0 r1 ; r0 := PCC
lea r1 1 ; r1 := (RO, Global, b_ext, e_ext, b_ext+1)
load cgp r1 ; cgp := CGP
lea r0 r20 ; r0 := PCC + offset
mov r1 0
mov r2 0
mov r3 0
fail
movsr ct2 mtdc
lea ct2 -1
store ct2 csp
movsr mtdc ct2
geta cs0 csp
getb cs1 csp
subseg csp cs1 cs0
switcher_zero_stk_init_pre:
sub cs0 cs1 cs0
mov cs1 csp
lea cs1 cs0
switcher_zero_stk_loop_pre:
jnz cs0 2
jmp (switcher_zero_stk_end_pre - switcher_zero_stk_loop_pre - 1)
store cs1 0
lea cs1 1
add cs0 cs0 1
switcher_zero_stk_loop_end_pre:
jmp (switcher_zero_stk_loop_pre - switcher_zero_stk_loop_end_pre)
switcher_zero_stk_end_pre:
lea csp -1
getb cs1 PC
geta cs0 PC
sub cs1 cs1 cs0
mov cs0 PC
lea cs0 cs1
lea cs0 -2
load cs0 cs0
unseal ct1 cs0 ct1
load cs0 ct1
rem ct2 cs0 10
sub cs0 cs0 ct2
div cs0 cs0 10
getb cgp ct1
geta cs1 ct1
sub cs1 cgp cs1
lea ct1 cs1
load cra ct1
lea ct1 1
load cgp ct1
lea cra cs0
add ct2 ct2 1
jmp ct2
mov r10 0
mov r11 0
mov r12 0
mov r13 0
mov r14 0
mov r15 0
mov r5 0
mov r0 0
mov r4 0
mov r6 0
mov r7 0
mov r8 0
mov r9 0
Expand All @@ -205,45 +216,41 @@ zero_stk_end:
mov r27 0
mov r28 0
mov r29 0
jalr r0 r0
movsr r21 mtdc
load stk r21
lea r21 1
movsr mtdc r21
load cgp stk
lea stk 1
load r24 stk
lea stk 1
load r21 stk
lea stk 1
load r20 stk
lea stk 1
zero_stk_init2:
geta r25 stk ; r20 := a
getb r26 stk ; r21 := b
sub r25 r26 r25 ; r25 := b-a
mov r26 stk ; r26 := (p,g,b,a,a)
lea r26 r25 ; r26 := (p,g,b,a,b)
zero_stk_loop2:
jnz r25 2 ; if (i = 0) then (end of loop), otherwise continue
jmp (zero_stk_end2 - zero_stk_loop2 - 1) ;
store r26 0 ; mem[b+i] := 0
lea r26 1 ; r26 := (p,g,b,a,b+i)
add r25 r25 1 ; i := i + 1
zero_stk_loopp2:
jmp (zero_stk_loop2 - zero_stk_loopp2)
zero_stk_end2:
mov r0 r24 ; mov cra, ca2
mov r1 0
mov r2 0
mov r3 0
mov r30 0
jalr cra cra
movsr ctp mtdc
load csp ctp
lea ctp 1
movsr mtdc ctp
load cgp csp
lea csp 1
load ca2 csp
lea csp 1
load cs1 csp
lea csp 1
load cs0 csp
lea csp 1
switcher_zero_stk_init_post:
geta ct0 csp
getb ct1 csp
sub ct0 ct1 ct0
mov ct1 csp
lea ct1 ct0
switcher_zero_stk_loop_post:
jnz ct0 2
jmp (switcher_zero_stk_end_post - switcher_zero_stk_loop_post - 1) ;
store ct1 0
lea ct1 1
add ct0 ct0 1
switcher_zero_stk_loop_end_post:
jmp (switcher_zero_stk_loop_post - switcher_zero_stk_loop_end_post)
switcher_zero_stk_end_post:
mov cra ca2
mov r0 0
mov r4 0
mov r5 0
mov r6 0
mov r7 0
mov r8 0
mov r9 0
mov r10 0
mov r11 0
mov r12 0
mov r13 0
mov r14 0
Expand All @@ -252,11 +259,16 @@ zero_stk_end2:
mov r17 0
mov r18 0
mov r19 0
mov r20 0
mov r21 0
mov r22 0
mov r23 0
mov r24 0
mov r25 0
mov r26 0
mov r27 0
mov r28 0
mov r29 0
jalr r0 r0
mov r30 0
jalr cra cra
switcher_end:

0 comments on commit b3f914f

Please sign in to comment.