An implementation of dynamic safety in OCaml for CS4400/5400 Spr24

dynamic-safety.ml

(**********************************************************************************)
(* micro-asm *)

exception Trap

(** a memory unsafe language *)
type asm =
  (* load location in register 0 into reg *)
  | Load of { reg: int; addr: int }
  (* store register[reg] into heap[addr] *)
  | Store of { reg : int; addr: int }
  (* set register[reg] = value *)
  | Setreg of { reg: int; value: int }
  (* trap: gives a runtime error if register[0] != v *)
  | Trap of int
  (* set register[0] = register[1] + register[2] *)
  | AddInt
  | MulInt
  (* terminate *)
  | Ret

type state = { reg: int array;
               heap: int array;
               program: asm array;
               (* instruction counter *)
               insn: int ref}

let rec interp_insn (state:state) : unit =
  match Array.get state.program (!(state.insn)) with
  | Load { reg=r; addr=addr} ->
    Array.set state.reg r (Array.get state.heap addr);
    state.insn := !(state.insn) + 1;
    interp_insn state
  | Store { reg=r; addr=addr } ->
    let v = Array.get state.reg r in
    Array.set state.heap addr v;
    state.insn := !(state.insn) + 1;
    interp_insn state
  | Setreg { reg=r; value=v } ->
    Array.set state.reg r v;
    state.insn := !(state.insn) + 1;
    interp_insn state
  | Trap(i) ->
    if (Array.get state.reg 0) = i then () else raise Trap;
    state.insn := !(state.insn) + 1;
    interp_insn state
  | AddInt ->
    let v = (Array.get state.reg 1) + (Array.get state.reg 2) in
    Array.set state.reg 0 v;
    state.insn := !(state.insn) + 1;
    interp_insn state
  | MulInt ->
    let v = (Array.get state.reg 1) * (Array.get state.reg 2) in
    Array.set state.reg 0 v;
    state.insn := !(state.insn) + 1;
    interp_insn state
  | Ret -> ()

(** run all instructions in l and return the result in register 0 *)
let interp_asm (l: asm list) : int =
  let arr = Array.of_list l in
  let state = {reg = (Array.make 4 (-1));
               heap=(Array.make 100 (-1));
               program=arr;
               insn=ref 0
              } in
  interp_insn state;
  Array.get state.reg 0

let asm1 = [Setreg { reg=1; value=1 };
            Setreg { reg=2; value=2 };
            AddInt;
            Ret]

let asm2 = [
  Setreg { reg=1; value=1 };
  (* store register 1 into heap[0x4] *)
  Store { reg = 1; addr=4 };
  Load { reg=0; addr=4 };
  Ret
]


let () =
  assert ((interp_asm asm1) = 3);
  assert ((interp_asm asm2) = 1);

(**********************************************************************************)
(* cast-safety: compiling to micr-asm *)

(** now, let's compile a safe functional language into a non-memory-safe
    imperative language *)
type calc =
  | Num of int
  | AddInt of calc * calc
  | Bool of bool
  | And of calc * calc

type calcv =
    VNum of int
  | VBool of bool

let fresh (iref: int ref) : int =
  let cur = !iref in
  iref := cur + 1;
  cur

(**
   compiles calculator lang to TinyAsm

   returns a pair (Listof TinyAsm, Number) where the second component is the
   address that holds the result.
*)
let rec unsafe_calc_to_asm (counter: int ref) (c: calc) : (int * asm list) =
  match c with
  | Num(n) ->
    (* store n in a fresh location *)
    let new_loc = fresh counter in
    (new_loc, [Setreg {reg=0; value=n};
               Store {reg=0; addr=new_loc}])
  | Bool(b) ->
    (* store n in a fresh location *)
    let new_loc = fresh counter in
    (new_loc, [Setreg {reg=0; value=if b then 1 else 0};
               Store {reg=0; addr=new_loc}])
  | AddInt(e1, e2) ->
    let (addr1, prog1) = unsafe_calc_to_asm counter e1 in
    let (addr2, prog2) = unsafe_calc_to_asm counter e2 in
    let result_addr = fresh counter in
    let new_prog = [Load { reg=1; addr=addr1 };
                    Load { reg=2; addr=addr2 };
                    AddInt;
                    Store {reg=0; addr=result_addr}] in
    (result_addr, List.concat[prog1; prog2; new_prog])
  | And(e1, e2) ->
    let (addr1, prog1) = unsafe_calc_to_asm counter e1 in
    let (addr2, prog2) = unsafe_calc_to_asm counter e2 in
    let result_addr = fresh counter in
    let new_prog = [Load { reg=1; addr=addr1 };
                    Load { reg=2; addr=addr2 };
                    MulInt;
                    Store {reg=0; addr=result_addr}] in
    (result_addr, List.concat[prog1; prog2; new_prog])

let unsafe_calc_to_asm_prog (c:calc) : asm list =
  let (addr, asm) = unsafe_calc_to_asm (ref 0) c in
  let asm = List.concat [asm; [Load{reg = 0; addr=addr}; Ret]] in
  asm

(* compile a calc program to asm and run it *)
let run_calc_unsafe (c:calc) : calcv =
  let asm = unsafe_calc_to_asm_prog c in
  VNum(interp_asm asm)

let calc1 = AddInt(Num(2), Num(20))

let calc2 = AddInt(AddInt(Num(2), Num(4)), Num(20))

let calc3 = And(Bool(true), And(Bool(true), Bool(false)))

let () =
  assert ((run_calc_unsafe calc1) = VNum(22));
  assert ((run_calc_unsafe calc2) = VNum(26));
  assert ((run_calc_unsafe calc3) = VNum(0))

(**********************************************************************************)
(* dynamic type-safety *)

let bool_tag = 1924

let int_tag = 9418

(**
   compiles calculator lang to TinyAsm

   returns a pair (Listof TinyAsm, Number) where the second component is the
   address that holds the result.
*)
let rec safe_calc_to_asm (counter: int ref) (c: calc) : (int * asm list) =
  match c with
  | Num(n) ->
    (* store n in a fresh location *)
    let addr_v = fresh counter in
    let addr_tag = fresh counter in
    (addr_v, [Setreg {reg=0; value=n};
              Setreg {reg=1; value=int_tag};
              Store {reg=0; addr=addr_v};
              Store {reg=1; addr=addr_tag}])
  | Bool(b) ->
    (* store n in a fresh location *)
    let addr_v = fresh counter in
    let addr_tag = fresh counter in
    (addr_v, [Setreg {reg=0; value=if b then 1 else 0};
              Setreg {reg=1; value=bool_tag};
              Store {reg=0; addr=addr_v};
              Store {reg=1; addr=addr_tag}])
  | AddInt(e1, e2) ->
    let (addr1, prog1) = safe_calc_to_asm counter e1 in
    let (addr2, prog2) = safe_calc_to_asm counter e2 in
    let result_addr = fresh counter in
    let tag_addr = fresh counter in
    let new_prog = [
      (* add a check to ensure e1 and e2 have the correct tag *)
      Load {reg = 0; addr = addr1 + 1};
      Trap(int_tag);
      Load {reg = 0; addr = addr2 + 1};
      Trap(int_tag);
      (* now load the desired values in and add them *)
      Load { reg=1; addr=addr1 };
      Load { reg=2; addr=addr2 };
      AddInt;
      Store {reg=0; addr=result_addr};
      (* store the tag *)
      Setreg {reg = 1; value = int_tag};
      Store {reg = 1; addr=tag_addr};
    ] in
    (result_addr, List.concat[prog1; prog2; new_prog])
  | And(e1, e2) ->
    let (addr1, prog1) = safe_calc_to_asm counter e1 in
    let (addr2, prog2) = safe_calc_to_asm counter e2 in
    let result_addr = fresh counter in
    let tag_addr = fresh counter in
    let new_prog = [
      (* add a check to ensure e1 and e2 have the correct tag *)
      Load {reg = 0; addr = addr1 + 1};
      Trap(bool_tag);
      Load {reg = 0; addr = addr2 + 1};
      Trap(bool_tag);
      (* now load the desired values in and add them *)
      Load { reg=1; addr=addr1 };
      Load { reg=2; addr=addr2 };
      MulInt;
      Store {reg = 0; addr=result_addr};
      (* store the tag *)
      Setreg {reg = 1; value = bool_tag};
      Store {reg = 1; addr=tag_addr};
    ] in
    (result_addr, List.concat[prog1; prog2; new_prog])

let safe_calc_to_asm_prog (c:calc) : asm list =
  let (addr, asm) = safe_calc_to_asm (ref 0) c in
  (* add ret to the end *)
  List.concat [asm; [Load{reg = 0; addr=addr}; Ret]]


let run_calc_safe (c:calc) : calcv =
  let asm = safe_calc_to_asm_prog c in
  VNum(interp_asm asm)

let () =
  assert ((run_calc_safe calc1) = VNum(22));
  assert ((run_calc_safe calc2) = VNum(26));
  assert ((run_calc_safe calc3) = VNum(0))

(* test for exceptions *)
let () =
  try
    (let _ = run_calc_safe (AddInt(Bool(true), Num(10))) in
    assert false)
  with
  Trap -> ();
  try
    (let _ = run_calc_safe (AddInt(AddInt(Num(10), Num(20)), Bool(true))) in
     assert false)
  with
    Trap -> ()