Changeset 740 for Deliverables/D2.2

Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml

-                      r631
+                      r740
 let interpret print_result p =
+  if print_result then Printf.printf "8051: %!" ;
   if p.ASM.has_main then
     let st = load_program p in
 …
     let res = result st in
     if print_result then
       Printf.printf "8051: %s\n%!" (IntValue.Int8.to_string res) ;
+      Printf.printf "%s\n%!" (IntValue.Int8.to_string res) ;
     (res, List.rev !trace)
   else (IntValue.Int8.zero, [])

Deliverables/D2.2/8051/src/ASM/I8051.ml

-                      r619
+                      r740
 let reg_addr r = `DIRECT (BitVectors.vect_of_int r `Eight)
+(* External RAM size *)
+let ext_ram_size = MiscPottier.pow 2 16
+(* Internal RAM size *)
+let int_ram_size = MiscPottier.pow 2 8

Deliverables/D2.2/8051/src/ASM/I8051.mli

r486	r740
60	60
61	61	val reg_addr : register -> [> ASM.direct]
	62
	63	val ext_ram_size : int
	64	val int_ram_size : int

Deliverables/D2.2/8051/src/ERTL/ERTL.mli

-                      r486
+                      r740
   (* Load from external memory. Parameters are the destination register, the
+     address registers, and the label of the next statement. *)
+     address registers (low bytes first), and the label of the next
+     statement. *)
   | St_load of Register.t * Register.t * Register.t * Label.t
   (* Store to external memory. Parameters are the address registers, the source
      register, and the label of the next statement. *)
+  (* Store to external memory. Parameters are the address registers (low bytes
+     first), the source register, and the label of the next statement. *)
   | St_store of Register.t * Register.t * Register.t * Label.t

Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

-                      r619
+                      r740
 module Eval = I8051.Eval (Val)
-(* External RAM size *)
-let ext_ram_size = 1000
-(* Internal RAM size *)
-let int_ram_size = 100
-let change_offset v off =
-  if Val.is_pointer v then
-    let (b, _) = Val.to_pointer v in
-    Val.of_pointer (b, off)
-  else error ((Val.to_string v) ^ " is not a pointer.")
 (* Memory *)
 …
 type state =
     { st_frs : stack_frame list ;
+      pc     : Val.t ;
+      isp    : Val.t ;
+      pc     : Val.address ;
+      isp    : Val.address ;
+      exit   : Val.address ;
       lenv   : local_env ;
       carry  : Val.t ;
 …
 let change_pc st pc = { st with pc = pc }
 let change_isp st isp = { st with isp = isp }
+let change_exit st exit = { st with exit = exit }
 let change_lenv st lenv = { st with lenv = lenv }
 let change_carry st carry = { st with carry = carry }
 …
 let change_mem st mem = { st with mem = mem }
 let change_trace st trace = { st with trace = trace }
+let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
 let empty_state =
   { st_frs = [] ;
+    pc     = Val.undef ;
+    isp    = Val.undef ;
+    pc     = Val.null ;
+    isp    = Val.null ;
+    exit   = Val.null ;
     lenv   = Register.Map.empty ;
     carry  = Val.undef ;
 …
 (* Each label of each function is associated a pointer. The base of this pointer
    is the base of the function in memory. Inside a function, offsets are
+(* Each label of each function is associated an address. The base of this
+   address is the base of the function in memory. Inside a function, offsets are
    bijectively associated to labels. *)
 …
 (* [labels_offsets p] builds a bijection between the labels found in the
    functions of [p] and some offsets. *)
+   functions of [p] and some memory addresses. *)
 let labels_offsets p =
 …
 let fetch_stmt lbls_offs st =
   let msg =
     Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in
   let error () = error msg in
   if Val.is_pointer st.pc then
     let (_, off) = Val.to_pointer st.pc in
+    Printf.sprintf "%s does not point to a statement."
+      (Val.string_of_address st.pc) in
+  if Val.is_mem_address st.pc then
+    let off = Val.offset_of_address st.pc in
     let def = fun_def_of_ptr st.mem st.pc in
     let lbl = Labels_Offsets.find2 off lbls_offs in
     Label.Map.find lbl def.ERTL.f_graph
   else error ()
+  else error msg
 let entry_pc lbls_offs ptr def =
+  change_offset ptr (Labels_Offsets.find1 def.ERTL.f_entry lbls_offs)
+  let off = Labels_Offsets.find1 def.ERTL.f_entry lbls_offs in
+  Val.change_address_offset ptr off
 let init_fun_call lbls_offs st ptr def =
 …
 let next_pc lbls_offs st lbl =
   let off = Labels_Offsets.find1 lbl lbls_offs in
   change_pc st (change_offset st.pc off)
+  change_pc st (Val.change_address_offset st.pc off)
 let framesize st =
   if Val.is_pointer st.pc then
+  if Val.is_mem_address st.pc then
     let def = fun_def_of_ptr st.mem st.pc in
     def.ERTL.f_stacksize
 …
 let push st v =
   let mem = Mem.store2 st.mem chunk st.isp v in
   let isp = Val.succ st.isp in
+  let mem = Mem.store st.mem chunk st.isp v in
+  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
   change_mem (change_isp st isp) mem
 let pop st =
   let isp = Val.pred st.isp in
+  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
   let st = change_isp st isp in
   let v = Mem.load2 st.mem chunk st.isp in
+  let v = Mem.load st.mem chunk st.isp in
   (st, v)
+let get_ra st =
+  let (st, pch) = pop st in
+  let (st, pcl) = pop st in
+  [pcl ; pch]
 let save_ra lbls_offs st lbl =
   let ra = change_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
   let vs = Val.break ra 2 in
   let st = push st (List.nth vs 1) in
   let st = push st (List.nth vs 0) in
+  let ra =
+    Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
+  let st = push st (List.nth ra 0) in
+  let st = push st (List.nth ra 1) in
   st
+let save_frame st =
+  add_st_frs st st.lenv
+let save_frame st = add_st_frs st st.lenv
 let label_of_pointer lbls_offs ptr =
 …
   Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
 *)
   let (_, off) = Val.to_pointer ptr in
+  let off = Val.offset_of_address ptr in
   Labels_Offsets.find2 off lbls_offs
 let pointer_of_label lbls_offs ptr lbl =
+  let (b, _) = Val.to_pointer ptr in
+  let off = Labels_Offsets.find1 lbl lbls_offs in
+  Val.of_pointer (b, off)
+  Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
 let get_sp st =
+  let sph = get_reg (Hdw I8051.sph) st in
+  let spl = get_reg (Hdw I8051.spl) st in
+  Val.merge [sph ; spl]
+let set_sp v st =
+  let vs = Val.break v 2 in
+  let sph = List.nth vs 0 in
+  let spl = List.nth vs 1 in
+  List.map (fun r -> get_reg (Hdw r) st) [I8051.spl ; I8051.sph]
+let set_sp vs st =
+  let spl = List.nth vs 0 in
+  let sph = List.nth vs 1 in
+  let st = add_reg (Hdw I8051.spl) spl st in
   let st = add_reg (Hdw I8051.sph) sph st in
-  let st = add_reg (Hdw I8051.spl) spl st in
   st
+(*
+let get_int () =
+  try Val.of_int (int_of_string (read_line ()))
+  with Failure "int_of_string" -> error "Failed to scan an integer."
+let get_float () =
+  try Val.of_float (float_of_string (read_line ()))
+  with Failure "float_of_string" -> error "Failed to scan a float."
+let interpret_external
+    (mem  : memory)
+    (def  : AST.external_function)
+    (args : Val.t list) :
+    memory * Val.t list =
+  match def.AST.ef_tag, args with
+    | s, _ when s = Primitive.scan_int ->
+      (mem, [get_int ()])
+    | "scan_float", _ ->
+      (mem, [get_float ()])
+    | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
+      Printf.printf "%d" (Val.to_int v) ;
+      (mem, [Val.zero])
+    | "print_float", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, [Val.zero])
+    | "print_ptr", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, [Val.zero])
+    | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
+      Printf.printf "%d\n" (Val.to_int v) ;
+      (mem, [Val.zero])
+    | "print_floatln", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, [Val.zero])
+    | "print_ptrln", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s\n"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, [Val.zero])
+    | s, v :: _ when s = Primitive.alloc ->
+      let (mem, ptr) = Mem.alloc mem v in
+      let vs = Val.break ptr 2 in
+      (mem, vs)
+    | s, v1 :: v2 :: _ when s = Primitive.modulo ->
+      (mem, [Val.modulo v1 v2])
+    (* The other cases are either a type error (only integers and pointers
+       may not be differenciated during type checking) or an unknown
+       function. *)
+    | "print_int", _ | "print_intln", _ ->
+      error "Illegal cast from pointer to integer."
+    | "print_ptr", _ | "print_ptrln", _ ->
+      error "Illegal cast from integer to pointer."
+    | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
+*)
+module InterpretExternal = Primitive.Interpret (Mem)
+let interpret_external mem f args = match InterpretExternal.t mem f args with
+  | (mem', InterpretExternal.V v) -> (mem', [v])
+  | (mem', InterpretExternal.A addr) -> (mem', addr)
+let fetch_external_args st =
+  (* TODO: this is bad when parameters are the empty list. *)
+  [get_reg (Hdw (List.hd I8051.parameters)) st]
+let set_result st = function
+  | [] -> assert false (* should be impossible: at least one value returned *)
+  | [v] -> add_reg (Hdw I8051.dpl) v st
+  | v1 :: v2 :: _ ->
+    let st = add_reg (Hdw I8051.dpl) v1 st in
+    add_reg (Hdw I8051.dph) v2 st
+let interpret_external_call st f next_pc =
+  let args = fetch_external_args st in
+  let (mem, vs) = interpret_external st.mem f args in
+  let st = change_mem st mem in
+  let st = set_result st vs in
+  change_pc st next_pc
 let interpret_call lbls_offs st f ra =
 …
   match Mem.find_fun_def st.mem ptr with
     | ERTL.F_int def ->
-(*
-      Printf.printf "Pushing return address in IRAM: %s = %s\n%!"
-        ra (Val.to_string (pointer_of_label lbls_offs st.pc ra)) ;
-*)
       let st = save_ra lbls_offs st ra in
       let st = save_frame st in
       init_fun_call lbls_offs st ptr def
+    | ERTL.F_ext def -> assert false (* TODO *)
+    | ERTL.F_ext def ->
+      let next_pc =
+        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
+      interpret_external_call st def.AST.ef_tag next_pc
 let interpret_return lbls_offs st =
 …
   let (st, pch) = pop st in
   let (st, pcl) = pop st in
+  let pc = Val.merge [pch ; pcl] in
+(*
+  Printf.printf "Returning to %s = %s\n%!"
+    (Val.to_string pc) (label_of_pointer lbls_offs pc) ;
+*)
+  let pc = [pcl ; pch] in
   change_pc st pc
 …
     | ERTL.St_cost (cost_lbl, lbl) ->
       let st = change_trace st (cost_lbl :: st.trace) in
+      let st = add_trace st cost_lbl in
       next_pc st lbl
 …
       let size = framesize st in
       let sp = get_sp st in
       let new_sp = Val.sub sp (Val.of_int size) in
+      let new_sp = Val.add_address sp (Val.Offset.of_int (-size)) in
       let st = set_sp new_sp st in
       next_pc st lbl
 …
       let size = framesize st in
       let sp = get_sp st in
       let new_sp = Val.add sp (Val.of_int size) in
+      let new_sp = Val.add_address sp (Val.Offset.of_int size) in
       let st = set_sp new_sp st in
       next_pc st lbl
 …
     | ERTL.St_addrH (r, x, lbl) ->
+      let v = Mem.find_global st.mem x in
+      let vs = Val.break v 2 in
+      let vs = Mem.find_global st.mem x in
+      let st = add_reg (Psd r) (List.nth vs 1) st in
+      next_pc st lbl
+    | ERTL.St_addrL (r, x, lbl) ->
+      let vs = Mem.find_global st.mem x in
       let st = add_reg (Psd r) (List.nth vs 0) st in
-      next_pc st lbl
-    | ERTL.St_addrL (r, x, lbl) ->
-      let v = Mem.find_global st.mem x in
-      let vs = Val.break v 2 in
-      let st = add_reg (Psd r) (List.nth vs 1) st in
       next_pc st lbl
 …
     | ERTL.St_load (destr, addr1, addr2, lbl) ->
+      let addr =
+        Val.merge (List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2]) in
+      let v = Mem.load2 st.mem chunk addr in
+      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
+      let v = Mem.load st.mem chunk addr in
       let st = add_reg (Psd destr) v st in
       next_pc st lbl
     | ERTL.St_store (addr1, addr2, srcr, lbl) ->
+      let addr =
+        Val.merge (List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2]) in
+      let mem = Mem.store2 st.mem chunk addr (get_reg (Psd srcr) st) in
+      let addr = List.map (fun r -> get_reg (Psd r) st) [addr1 ; addr2] in
+      let mem = Mem.store st.mem chunk addr (get_reg (Psd srcr) st) in
       let st = change_mem st mem in
       next_pc st lbl
 …
-let fetch_result renv ret_regs = match ret_regs with
-  | [] -> Val.undef
-  | [_] -> I8051.RegisterMap.find I8051.dpl renv
-  | _ -> Val.merge [I8051.RegisterMap.find I8051.dph renv ;
-                    I8051.RegisterMap.find I8051.dpl renv]
 let print_lenv lenv =
   let f r v =
 …
 let current_label lbls_offs st =
+  let (_, off) = Val.to_pointer st.pc in
+  Labels_Offsets.find2 off lbls_offs
+  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
 let print_state lbls_offs st =
   Printf.printf "PC: %s (%s)\n%!"
+    (Val.to_string st.pc) (current_label lbls_offs st) ;
+  Printf.printf "SP: %s\n%!"
+    (Val.to_string (Val.merge [get_reg (Hdw I8051.sph) st ;
+                               get_reg (Hdw I8051.spl) st])) ;
+  Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
+    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
+  Printf.printf "SP: %s\n%!" (Val.string_of_address (get_sp st)) ;
+  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
   print_lenv st.lenv ;
   print_renv st.renv ;
 …
 let compute_result st ret_regs =
   try
     let v = get_reg (Psd (MiscPottier.last ret_regs)) st in
+    let v = get_reg (Psd (List.hd ret_regs)) st in
     if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
     else IntValue.Int8.zero
   with Not_found -> IntValue.Int8.zero
+let rec iter_small_step print_result lbls_offs st =
+let rec iter_small_step debug lbls_offs st =
+  if debug then print_state lbls_offs st ;
   match fetch_stmt lbls_offs st with
+    | ERTL.St_return ret_regs when st.st_frs = [] ->
+      let (res, cost_labels) as trace =
+        (compute_result st ret_regs, List.rev st.trace) in
+      if print_result then
+        Printf.printf "ERTL: %s\n%!" (IntValue.Int8.to_string res) ;
+      trace
+    | ERTL.St_return ret_regs when Val.eq_address (get_ra st) st.exit ->
+      (compute_result st ret_regs, List.rev st.trace)
     | stmt ->
-    (*
-      print_state lbls_offs st ;
-    *)
       let st' = interpret_stmt lbls_offs st stmt in
       iter_small_step print_result lbls_offs st'
+      iter_small_step debug lbls_offs st'
 …
   change_mem st mem
+let init_sp st =
+  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
+  let sp =
+    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
+  let st = change_mem st mem in
+  (st, sp)
+let init_isp st =
+  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
+  let st = change_mem (change_isp st isp) mem in
+  let (mem, exit) = Mem.alloc st.mem 1 in
+  let st = change_exit st exit in
+  let st = push st (List.nth exit 0) in
+  let st = push st (List.nth exit 1) in
+  st
 let init_renv st sp =
   let f r renv = I8051.RegisterMap.add r Val.undef renv in
   let renv = I8051.RegisterSet.fold f I8051.registers I8051.RegisterMap.empty in
+  let vs = Val.break sp 2 in
+  let sph = List.nth vs 0 in
+  let spl = List.nth vs 1 in
+  let spl = List.nth sp 0 in
+  let sph = List.nth sp 1 in
   let renv = I8051.RegisterMap.add I8051.sph sph renv in
   let renv = I8051.RegisterMap.add I8051.spl spl renv in
   change_renv st renv
-let init_sp st =
-  let (mem, sp) = Mem.alloc st.mem ext_ram_size in
-  let (b, _) = Val.to_pointer sp in
-  let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
-  let st = change_mem st mem in
-  (st, sp)
-let init_isp st =
-  let (mem, isp) = Mem.alloc st.mem int_ram_size in
-  let st = change_mem (change_isp st isp) mem in
-  let st = push st Val.zero in
-  let st = push st Val.zero in
-  st
 let init_main_call lbls_offs st main =
 …
    - Initialize the carry flag to 0. *)
+let interpret print_result p = match p.ERTL.main with
+  | None -> (IntValue.Int8.zero (* TODO *), [])
+  | Some main ->
+    let lbls_offs = labels_offsets p in
+    let st = empty_state in
+    let st = init_prog st p in
+    let (st, sp) = init_sp st in
+    let st = init_isp st in
+    let st = init_renv st sp in
+    let st = init_main_call lbls_offs st main in
+    let st = change_carry st Val.zero in
+    iter_small_step print_result lbls_offs st
+let interpret debug p =
+  if debug then Printf.printf "*** ERTL ***\n\n%!" ;
+  match p.ERTL.main with
+    | None -> (IntValue.Int8.zero, [])
+    | Some main ->
+      let lbls_offs = labels_offsets p in
+      let st = empty_state in
+      let st = init_prog st p in
+      let (st, sp) = init_sp st in
+      let st = init_isp st in
+      let st = init_renv st sp in
+      let st = init_main_call lbls_offs st main in
+      let st = change_carry st Val.zero in
+      iter_small_step debug lbls_offs st

Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

-                      r486
+                      r740
         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
+        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
+        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
         let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
-        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
         LTL.St_skip l
 …
         let l = generate (LTL.St_to_acc (I8051.st0, l)) in
         let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
+        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
+        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
         let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
-        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
         let l = generate (LTL.St_from_acc (I8051.st1, l)) in
         let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in

Deliverables/D2.2/8051/src/LIN/LINInterpret.ml

-                      r619
+                      r740
 module Eval = I8051.Eval (Val)
-(* External RAM size *)
-let ext_ram_size = 1000
-(* Internal RAM size *)
-let int_ram_size = 100
-let change_offset v off =
-  if Val.is_pointer v then
-    let (b, _) = Val.to_pointer v in
-    Val.of_pointer (b, off)
-  else error ((Val.to_string v) ^ " is not a pointer.")
 (* Memory *)
 …
 type memory = LIN.function_def Mem.memory
 (* Hardware registers environments. They associate a value to the each hardware
+(* Hardware registers environments. They associate a value to each hardware
    register. *)
 …
 type state =
+    { pc     : Val.t ;
+      isp    : Val.t ;
+    { pc     : Val.address ;
+      isp    : Val.address ;
+      exit   : Val.address ;
       carry  : Val.t ;
       renv   : hdw_reg_env ;
 …
 let change_pc st pc = { st with pc = pc }
 let change_isp st isp = { st with isp = isp }
+let change_exit st exit = { st with exit = exit }
 let change_carry st carry = { st with carry = carry }
 let change_renv st renv = { st with renv = renv }
 let change_mem st mem = { st with mem = mem }
 let change_trace st trace = { st with trace = trace }
+let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
 let empty_state =
+  { pc     = Val.undef ;
+    isp    = Val.undef ;
+  { pc     = Val.null ;
+    isp    = Val.null ;
+    exit   = Val.null ;
     carry  = Val.undef ;
     renv   = I8051.RegisterMap.empty ;
 …
 let fetch_stmt st =
   let msg =
     Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in
   let error () = error msg in
   if Val.is_pointer st.pc then
     let (_, off) = Val.to_pointer st.pc in
+    Printf.sprintf "%s does not point to a statement."
+      (Val.string_of_address st.pc) in
+  if Val.is_mem_address st.pc then
+    let off = Val.offset_of_address st.pc in
     let def = int_fun_of_ptr st.mem st.pc in
     List.nth def (Val.Offset.to_int off)
   else error ()
+  else error msg
 let init_fun_call st ptr =
   change_pc st (change_offset ptr Val.Offset.zero)
+  change_pc st (Val.change_address_offset ptr Val.Offset.zero)
 let next_pc st =
   change_pc st (Val.succ st.pc)
+  change_pc st (Val.add_address st.pc Val.Offset.one)
 let add_reg r v st =
 …
 let push st v =
   let mem = Mem.store2 st.mem chunk st.isp v in
   let isp = Val.succ st.isp in
+  let mem = Mem.store st.mem chunk st.isp v in
+  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
   change_mem (change_isp st isp) mem
 let pop st =
   let isp = Val.pred st.isp in
+  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
   let st = change_isp st isp in
   let v = Mem.load2 st.mem chunk st.isp in
+  let v = Mem.load st.mem chunk st.isp in
   (st, v)
 let save_ra st =
+  let ra = Val.succ st.pc in
+  let vs = Val.break ra 2 in
+  let st = push st (List.nth vs 1) in
+  let st = push st (List.nth vs 0) in
+  let ra = Val.add_address st.pc Val.Offset.one in
+  let st = push st (List.nth ra 0) in
+  let st = push st (List.nth ra 1) in
   st
 …
   let code = current_int_fun st in
   let off = find_label lbl code in
   change_offset st.pc (Val.Offset.of_int off)
+  Val.change_address_offset st.pc (Val.Offset.of_int off)
 let goto st lbl =
 …
   let (st, pch) = pop st in
   let (st, pcl) = pop st in
+  Val.merge [pch ; pcl]
+(*
+let get_int () =
+  try Val.of_int (int_of_string (read_line ()))
+  with Failure "int_of_string" -> error "Failed to scan an integer."
+let get_float () =
+  try Val.of_float (float_of_string (read_line ()))
+  with Failure "float_of_string" -> error "Failed to scan a float."
+let interpret_external
+    (mem  : memory)
+    (def  : AST.external_function)
+    (args : Val.t list) :
+    memory * Val.t list =
+  match def.AST.ef_tag, args with
+    | s, _ when s = Primitive.scan_int ->
+      (mem, [get_int ()])
+    | "scan_float", _ ->
+      (mem, [get_float ()])
+    | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
+      Printf.printf "%d" (Val.to_int v) ;
+      (mem, [Val.zero])
+    | "print_float", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, [Val.zero])
+    | "print_ptr", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, [Val.zero])
+    | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
+      Printf.printf "%d\n" (Val.to_int v) ;
+      (mem, [Val.zero])
+    | "print_floatln", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, [Val.zero])
+    | "print_ptrln", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s\n"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, [Val.zero])
+    | s, v :: _ when s = Primitive.alloc ->
+      let (mem, ptr) = Mem.alloc mem v in
+      let vs = Val.break ptr 2 in
+      (mem, vs)
+    | s, v1 :: v2 :: _ when s = Primitive.modulo ->
+      (mem, [Val.modulo v1 v2])
+    (* The other cases are either a type error (only integers and pointers
+       may not be differenciated during type checking) or an unknown
+       function. *)
+    | "print_int", _ | "print_intln", _ ->
+      error "Illegal cast from pointer to integer."
+    | "print_ptr", _ | "print_ptrln", _ ->
+      error "Illegal cast from integer to pointer."
+    | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
+*)
+  (st, [pcl ; pch])
+let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
+(* State pretty-printing *)
+let print_renv renv =
+  let f r v =
+    if not (Val.eq v Val.undef) then
+    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
+  I8051.RegisterMap.iter f renv
+let print_state st =
+  Printf.printf "PC: %s\n%!" (Val.string_of_address st.pc) ;
+  Printf.printf "SP: %s\n%!"
+    (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
+  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
+  print_renv st.renv ;
+  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
+  Mem.print st.mem ;
+  Printf.printf "\n%!"
+module InterpretExternal = Primitive.Interpret (Mem)
+let interpret_external mem f args = match InterpretExternal.t mem f args with
+  | (mem', InterpretExternal.V v) -> (mem', [v])
+  | (mem', InterpretExternal.A addr) -> (mem', addr)
+let fetch_external_args st =
+  (* TODO: this is bad when parameters are the empty list. *)
+  [get_reg (List.hd I8051.parameters) st]
+let set_result st = function
+  | [] -> assert false (* should be impossible: at least one value returned *)
+  | [v] -> add_reg I8051.dpl v st
+  | v1 :: v2 :: _ ->
+    let st = add_reg I8051.dpl v1 st in
+    add_reg I8051.dph v2 st
+let interpret_external_call st f =
+  let args = fetch_external_args st in
+  let (mem, vs) = interpret_external st.mem f args in
+  let st = change_mem st mem in
+  set_result st vs
 let interpret_call st f =
 …
       let st = save_ra st in
       init_fun_call st ptr
+    | LIN.F_ext def -> assert false (* TODO *)
+    | LIN.F_ext def ->
+      let st = next_pc st in
+      interpret_external_call st def.AST.ef_tag
 let interpret_return st =
   let pc = return_pc st in
+  let (st, pc) = return_pc st in
   change_pc st pc
 …
     | LIN.St_cost cost_lbl ->
       let st = change_trace st (cost_lbl :: st.trace) in
+      let st = add_trace st cost_lbl in
       next_pc st
 …
     | LIN.St_addr x ->
+      let v = Mem.find_global st.mem x in
+      let vs = Val.break v 2 in
+      let st = add_reg I8051.dph (List.nth vs 0) st in
+      let st = add_reg I8051.dpl (List.nth vs 1) st in
+      let vs = Mem.find_global st.mem x in
+      let st = add_reg I8051.dpl (List.nth vs 0) st in
+      let st = add_reg I8051.dph (List.nth vs 1) st in
       next_pc st
 …
     | LIN.St_load ->
+      let addr =
+        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
+      let v = Mem.load2 st.mem chunk addr in
+      let addr = dptr st in
+      let v = Mem.load st.mem chunk addr in
       let st = add_reg I8051.a v st in
       next_pc st
     | LIN.St_store ->
+      let addr =
+        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
+      let mem = Mem.store2 st.mem chunk addr (get_reg I8051.a st) in
+      let addr = dptr st in
+      let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
       let st = change_mem st mem in
       next_pc st
 …
-let print_renv renv =
-  let f r v =
-    if not (Val.eq v Val.undef) then
-    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
-  I8051.RegisterMap.iter f renv
-let print_state st =
-  Printf.printf "PC: %s\n%!" (Val.to_string st.pc) ;
-  Printf.printf "SP: %s\n%!"
-    (Val.to_string (Val.merge [get_reg I8051.sph st ; get_reg I8051.spl st])) ;
-  Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
-  print_renv st.renv ;
-  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
-  Mem.print st.mem ;
-  Printf.printf "\n%!"
 let compute_result st =
   let v = get_reg I8051.dpl st in
 …
   else IntValue.Int8.zero
+let rec iter_small_step print_result st =
+(*
+  (* <DEBUG> *)
+  print_state st ;
+  (* </DEBUG> *)
+*)
+let rec iter_small_step debug st =
+  if debug then print_state st ;
   match fetch_stmt st with
+    | LIN.St_return when Val.eq (return_pc st) Val.zero ->
+      let (res, cost_labels) as trace =
+        (compute_result st, List.rev st.trace) in
+      if print_result then
+        Printf.printf "LIN: %s\n%!" (IntValue.Int8.to_string res) ;
+      trace
+    | LIN.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
+      (compute_result st, List.rev st.trace)
     | stmt ->
       let st' = interpret_stmt st stmt in
       iter_small_step print_result st'
+      iter_small_step debug st'
 …
   change_mem st mem
+let init_sp st =
+  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
+  let sp =
+    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
+  let st = change_mem st mem in
+  (st, sp)
+let init_isp st =
+  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
+  let st = change_mem (change_isp st isp) mem in
+  let (mem, exit) = Mem.alloc st.mem 1 in
+  let st = change_exit st exit in
+  let st = push st (List.nth exit 0) in
+  let st = push st (List.nth exit 1) in
+  st
 let init_renv st sp =
   let f r st = add_reg r Val.undef st in
   let st = I8051.RegisterSet.fold f I8051.registers st in
   let vs = Val.break sp 2 in
   let sph = List.nth vs 0 in
   let spl = List.nth vs 1 in
+  let spl = List.nth sp 0 in
+  let sph = List.nth sp 1 in
+  let st = add_reg I8051.spl spl st in
   let st = add_reg I8051.sph sph st in
-  let st = add_reg I8051.spl spl st in
   st
-let init_sp st =
-  let (mem, sp) = Mem.alloc st.mem ext_ram_size in
-  let (b, _) = Val.to_pointer sp in
-  let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
-  let st = change_mem st mem in
-  (st, sp)
-let init_isp st =
-  let (mem, isp) = Mem.alloc st.mem int_ram_size in
-  let st = change_mem (change_isp st isp) mem in
-  let vs = Val.break Val.zero 2 in
-  let st = push st (List.nth vs 1) in
-  let st = push st (List.nth vs 0) in
-  st
 let init_main_call st main =
 …
    - Initialize the carry flag to 0. *)
+let interpret print_result p = match p.LIN.main with
+  | None -> (IntValue.Int8.zero, [])
+  | Some main ->
+    let st = empty_state in
+    let st = init_prog st p in
+    let (st, sp) = init_sp st in
+    let st = init_isp st in
+    let st = init_renv st sp in
+    let st = init_main_call st main in
+    let st = change_carry st Val.zero in
+    iter_small_step print_result st
+let interpret debug p =
+  if debug then Printf.printf "*** LIN ***\n\n%!" ;
+  match p.LIN.main with
+    | None -> (IntValue.Int8.zero, [])
+    | Some main ->
+      let st = empty_state in
+      let st = init_prog st p in
+      let (st, sp) = init_sp st in
+      let st = init_isp st in
+      let st = init_renv st sp in
+      let st = init_main_call st main in
+      let st = change_carry st Val.zero in
+      iter_small_step debug st

Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

-                      r619
+                      r740
 module Val = Mem.Value
 let chunk = Driver.LTLMemory.int_size
-(*
-let load mem = Mem.load2 st.mem chunk st.isp
-*)
 module Eval = I8051.Eval (Val)
-(* External RAM size *)
-let ext_ram_size = 1000
-(* Internal RAM size *)
-let int_ram_size = 100
-let change_offset v off =
-  if Val.is_pointer v then
-    let (b, _) = Val.to_pointer v in
-    Val.of_pointer (b, off)
-  else error ((Val.to_string v) ^ " is not a pointer.")
 …
 type state =
+    { pc     : Val.t ;
+      isp    : Val.t ;
+    { pc     : Val.address ;
+      isp    : Val.address ;
+      exit   : Val.address ;
       carry  : Val.t ;
       renv   : hdw_reg_env ;
 …
 let change_pc st pc = { st with pc = pc }
 let change_isp st isp = { st with isp = isp }
+let change_exit st exit = { st with exit = exit }
 let change_carry st carry = { st with carry = carry }
 let change_renv st renv = { st with renv = renv }
 let change_mem st mem = { st with mem = mem }
 let change_trace st trace = { st with trace = trace }
+let add_trace st cost_lbl = change_trace st (cost_lbl :: st.trace)
 let empty_state =
+  { pc     = Val.undef ;
+    isp    = Val.undef ;
+  { pc     = Val.null ;
+    isp    = Val.null ;
+    exit   = Val.null ;
     carry  = Val.undef ;
     renv   = I8051.RegisterMap.empty ;
 …
 let fetch_stmt lbls_offs st =
   let msg =
     Printf.sprintf "%s does not point to a statement." (Val.to_string st.pc) in
   let error () = error msg in
   if Val.is_pointer st.pc then
     let (_, off) = Val.to_pointer st.pc in
+    Printf.sprintf "%s does not point to a statement."
+      (Val.string_of_address st.pc) in
+  if Val.is_mem_address st.pc then
+    let off = Val.offset_of_address st.pc in
     let def = fun_def_of_ptr st.mem st.pc in
     let lbl = Labels_Offsets.find2 off lbls_offs in
     Label.Map.find lbl def.LTL.f_graph
   else error ()
+  else error msg
 let entry_pc lbls_offs ptr def =
   change_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
+  Val.change_address_offset ptr (Labels_Offsets.find1 def.LTL.f_entry lbls_offs)
 let init_fun_call lbls_offs st ptr def =
 …
 let next_pc lbls_offs st lbl =
   let off = Labels_Offsets.find1 lbl lbls_offs in
   change_pc st (change_offset st.pc off)
+  change_pc st (Val.change_address_offset st.pc off)
 let framesize st =
   if Val.is_pointer st.pc then
+  if Val.is_mem_address st.pc then
     let def = fun_def_of_ptr st.mem st.pc in
     def.LTL.f_stacksize
 …
 let push st v =
   let mem = Mem.store2 st.mem chunk st.isp v in
   let isp = Val.succ st.isp in
+  let mem = Mem.store st.mem chunk st.isp v in
+  let isp = Val.add_address st.isp (Val.Offset.of_int chunk) in
   change_mem (change_isp st isp) mem
 let pop st =
   let isp = Val.pred st.isp in
+  let isp = Val.add_address st.isp (Val.Offset.of_int (-chunk)) in
   let st = change_isp st isp in
   let v = Mem.load2 st.mem chunk st.isp in
+  let v = Mem.load st.mem chunk st.isp in
   (st, v)
 let save_ra lbls_offs st lbl =
   let ra = change_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
   let vs = Val.break ra 2 in
   let st = push st (List.nth vs 1) in
   let st = push st (List.nth vs 0) in
+  let ra =
+    Val.change_address_offset st.pc (Labels_Offsets.find1 lbl lbls_offs) in
+  let st = push st (List.nth ra 0) in
+  let st = push st (List.nth ra 1) in
   st
 …
   Printf.printf "Retrieving label of %s\n%!" (Val.to_string ptr) ;
 *)
   let (_, off) = Val.to_pointer ptr in
+  let off = Val.offset_of_address ptr in
   Labels_Offsets.find2 off lbls_offs
 let pointer_of_label lbls_offs ptr lbl =
+  let (b, _) = Val.to_pointer ptr in
+  let off = Labels_Offsets.find1 lbl lbls_offs in
+  Val.of_pointer (b, off)
+  Val.change_address_offset ptr (Labels_Offsets.find1 lbl lbls_offs)
 let return_pc st =
   let (st, pch) = pop st in
   let (st, pcl) = pop st in
+  Val.merge [pch ; pcl]
+(*
+let get_int () =
+  try Val.of_int (int_of_string (read_line ()))
+  with Failure "int_of_string" -> error "Failed to scan an integer."
+let get_float () =
+  try Val.of_float (float_of_string (read_line ()))
+  with Failure "float_of_string" -> error "Failed to scan a float."
+let interpret_external
+    (mem  : memory)
+    (def  : AST.external_function)
+    (args : Val.t list) :
+    memory * Val.t list =
+  match def.AST.ef_tag, args with
+    | s, _ when s = Primitive.scan_int ->
+      (mem, [get_int ()])
+    | "scan_float", _ ->
+      (mem, [get_float ()])
+    | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
+      Printf.printf "%d" (Val.to_int v) ;
+      (mem, [Val.zero])
+    | "print_float", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, [Val.zero])
+    | "print_ptr", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, [Val.zero])
+    | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
+      Printf.printf "%d\n" (Val.to_int v) ;
+      (mem, [Val.zero])
+    | "print_floatln", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, [Val.zero])
+    | "print_ptrln", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s\n"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, [Val.zero])
+    | s, v :: _ when s = Primitive.alloc ->
+      let (mem, ptr) = Mem.alloc mem v in
+      let vs = Val.break ptr 2 in
+      (mem, vs)
+    | s, v1 :: v2 :: _ when s = Primitive.modulo ->
+      (mem, [Val.modulo v1 v2])
+    (* The other cases are either a type error (only integers and pointers
+       may not be differenciated during type checking) or an unknown
+       function. *)
+    | "print_int", _ | "print_intln", _ ->
+      error "Illegal cast from pointer to integer."
+    | "print_ptr", _ | "print_ptrln", _ ->
+      error "Illegal cast from integer to pointer."
+    | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
+*)
+  (st, [pcl ; pch])
+let dptr st = List.map (fun r -> get_reg r st) [I8051.dpl ; I8051.dph]
+(* State pretty-printing *)
+let current_label lbls_offs st =
+  Labels_Offsets.find2 (Val.offset_of_address st.pc) lbls_offs
+let print_renv renv =
+  let f r v =
+    if not (Val.eq v Val.undef) then
+    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
+  I8051.RegisterMap.iter f renv
+let print_state lbls_offs st =
+  Printf.printf "PC: %s (%s)\n%!"
+    (Val.string_of_address st.pc) (current_label lbls_offs st) ;
+  Printf.printf "SP: %s\n%!"
+    (Val.string_of_address [get_reg I8051.spl st ; get_reg I8051.sph st]) ;
+  Printf.printf "ISP: %s%!" (Val.string_of_address st.isp) ;
+  print_renv st.renv ;
+  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
+  Mem.print st.mem ;
+  Printf.printf "\n%!"
+module InterpretExternal = Primitive.Interpret (Mem)
+let interpret_external mem f args = match InterpretExternal.t mem f args with
+  | (mem', InterpretExternal.V v) -> (mem', [v])
+  | (mem', InterpretExternal.A addr) -> (mem', addr)
+let fetch_external_args st =
+  (* TODO: this is bad when parameters are the empty list. *)
+  [get_reg (List.hd I8051.parameters) st]
+let set_result st = function
+  | [] -> assert false (* should be impossible: at least one value returned *)
+  | [v] -> add_reg I8051.dpl v st
+  | v1 :: v2 :: _ ->
+    let st = add_reg I8051.dpl v1 st in
+    add_reg I8051.dph v2 st
+let interpret_external_call st f next_pc =
+  let args = fetch_external_args st in
+  let (mem, vs) = interpret_external st.mem f args in
+  let st = change_mem st mem in
+  let st = set_result st vs in
+  change_pc st next_pc
 let interpret_call lbls_offs st f ra =
 …
   match Mem.find_fun_def st.mem ptr with
     | LTL.F_int def ->
-(*
-      Printf.printf "Pushing return address in IRAM: %s = %s\n%!"
-        ra (Val.to_string (pointer_of_label lbls_offs st.pc ra)) ;
-*)
       let st = save_ra lbls_offs st ra in
       init_fun_call lbls_offs st ptr def
+    | LTL.F_ext def -> assert false (* TODO *)
+    | LTL.F_ext def ->
+      let next_pc =
+        Val.change_address_offset st.pc (Labels_Offsets.find1 ra lbls_offs) in
+      interpret_external_call st def.AST.ef_tag next_pc
 let interpret_return lbls_offs st =
+  let pc = return_pc st in
+(*
+  Printf.printf "Returning to %s = %s\n%!"
+    (Val.to_string pc) (label_of_pointer lbls_offs pc) ;
+*)
+  let (st, pc) = return_pc st in
   change_pc st pc
 …
     | LTL.St_cost (cost_lbl, lbl) ->
       let st = change_trace st (cost_lbl :: st.trace) in
+      let st = add_trace st cost_lbl in
       next_pc st lbl
 …
     | LTL.St_addr (x, lbl) ->
+      let v = Mem.find_global st.mem x in
+      let vs = Val.break v 2 in
+      let st = add_reg I8051.dph (List.nth vs 0) st in
+      let st = add_reg I8051.dpl (List.nth vs 1) st in
+      let vs = Mem.find_global st.mem x in
+      let st = add_reg I8051.dpl (List.nth vs 0) st in
+      let st = add_reg I8051.dph (List.nth vs 1) st in
       next_pc st lbl
 …
     | LTL.St_load lbl ->
+      let addr =
+        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
+      let v = Mem.load2 st.mem chunk addr in
+      let addr = dptr st in
+      let v = Mem.load st.mem chunk addr in
       let st = add_reg I8051.a v st in
       next_pc st lbl
     | LTL.St_store lbl ->
+      let addr =
+        Val.merge (List.map (fun r -> get_reg r st) [I8051.dph ; I8051.dpl]) in
+      let mem = Mem.store2 st.mem chunk addr (get_reg I8051.a st) in
+      let addr = dptr st in
+      let mem = Mem.store st.mem chunk addr (get_reg I8051.a st) in
       let st = change_mem st mem in
       next_pc st lbl
 …
-let current_label lbls_offs st =
-  let (_, off) = Val.to_pointer st.pc in
-  Labels_Offsets.find2 off lbls_offs
-let print_renv renv =
-  let f r v =
-    if not (Val.eq v Val.undef) then
-    Printf.printf "\n%s = %s%!" (I8051.print_register r) (Val.to_string v) in
-  I8051.RegisterMap.iter f renv
-let print_state lbls_offs st =
-  Printf.printf "PC: %s (%s)\n%!"
-    (Val.to_string st.pc) (current_label lbls_offs st) ;
-  Printf.printf "SP: %s\n%!"
-    (Val.to_string (Val.merge [get_reg I8051.sph st ; get_reg I8051.spl st])) ;
-  Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
-  print_renv st.renv ;
-  Printf.printf "\nC = %s%!" (Val.to_string st.carry) ;
-  Mem.print st.mem ;
-  Printf.printf "\n%!"
-let print_result st =
-  let string_of_reg r = Val.to_string (get_reg r st) in
-  Printf.printf "DPH: %s - DPL: %s\n%!"
-    (string_of_reg I8051.dph) (string_of_reg I8051.dpl)
 let compute_result st =
   let v = get_reg I8051.dpl st in
 …
   else IntValue.Int8.zero
+let rec iter_small_step print_result lbls_offs st =
+(*
+    print_state lbls_offs st ;
+*)
+let rec iter_small_step debug lbls_offs st =
+  if debug then print_state lbls_offs st ;
   match fetch_stmt lbls_offs st with
+    | LTL.St_return when Val.eq (return_pc st) Val.zero ->
+      let (res, cost_labels) as trace =
+        (compute_result st, List.rev st.trace) in
+      if print_result then
+        Printf.printf "LTL: %s\n%!" (IntValue.Int8.to_string res) ;
+      trace
+    | LTL.St_return when Val.eq_address (snd (return_pc st)) st.exit ->
+      (compute_result st, List.rev st.trace)
     | stmt ->
       let st' = interpret_stmt lbls_offs st stmt in
       iter_small_step print_result lbls_offs st'
+      iter_small_step debug lbls_offs st'
 …
   change_mem st mem
+let init_sp st =
+  let (mem, sp) = Mem.alloc st.mem I8051.ext_ram_size in
+  let sp =
+    Val.change_address_offset sp (Val.Offset.of_int I8051.ext_ram_size) in
+  let st = change_mem st mem in
+  (st, sp)
+let init_isp st =
+  let (mem, isp) = Mem.alloc st.mem I8051.int_ram_size in
+  let st = change_mem (change_isp st isp) mem in
+  let (mem, exit) = Mem.alloc st.mem 1 in
+  let st = change_exit st exit in
+  let st = push st (List.nth exit 0) in
+  let st = push st (List.nth exit 1) in
+  st
 let init_renv st sp =
   let f r st = add_reg r Val.undef st in
   let st = I8051.RegisterSet.fold f I8051.registers st in
   let vs = Val.break sp 2 in
   let sph = List.nth vs 0 in
   let spl = List.nth vs 1 in
+  let spl = List.nth sp 0 in
+  let sph = List.nth sp 1 in
+  let st = add_reg I8051.spl spl st in
   let st = add_reg I8051.sph sph st in
-  let st = add_reg I8051.spl spl st in
   st
-let init_sp st =
-  let (mem, sp) = Mem.alloc st.mem ext_ram_size in
-  let (b, _) = Val.to_pointer sp in
-  let sp = Val.of_pointer (b, Val.Offset.of_int ext_ram_size) in
-  let st = change_mem st mem in
-  (st, sp)
-let init_isp st =
-  let (mem, isp) = Mem.alloc st.mem int_ram_size in
-  let st = change_mem (change_isp st isp) mem in
-  let vs = Val.break Val.zero 2 in
-  let st = push st (List.nth vs 1) in
-  let st = push st (List.nth vs 0) in
-  st
 let init_main_call lbls_offs st main =
 …
    - Initialize the carry flag to 0. *)
+let interpret print_result p = match p.LTL.main with
+  | None -> (IntValue.Int8.zero, [])
+  | Some main ->
+    let lbls_offs = labels_offsets p in
+    let st = empty_state in
+    let st = init_prog st p in
+    let (st, sp) = init_sp st in
+    let st = init_isp st in
+    let st = init_renv st sp in
+    let st = init_main_call lbls_offs st main in
+    let st = change_carry st Val.zero in
+    iter_small_step print_result lbls_offs st
+let interpret debug p =
+  if debug then Printf.printf "*** LTL ***\n\n%!" ;
+  match p.LTL.main with
+    | None -> (IntValue.Int8.zero, [])
+    | Some main ->
+      let lbls_offs = labels_offsets p in
+      let st = empty_state in
+      let st = init_prog st p in
+      let (st, sp) = init_sp st in
+      let st = init_isp st in
+      let st = init_renv st sp in
+      let st = init_main_call lbls_offs st main in
+      let st = change_carry st Val.zero in
+      iter_small_step debug lbls_offs st

Deliverables/D2.2/8051/src/RTL/RTL.mli

-                      r486
+                      r740
   (* Assign the address of a symbol to registers. Parameters are the destination
+     registers, the symbol and the label of the next statement. *)
+     registers (low bytes first), the symbol and the label of the next
+     statement. *)
   | St_addr of Register.t * Register.t * AST.ident * Label.t
   (* Assign the stack pointer to registers. Parameters are the destination
      registers, and the label of the next statement. *)
+     registers (low bytes first), and the label of the next statement. *)
   | St_stackaddr of Register.t * Register.t * Label.t
 …
   (* Load from external memory. Parameters are the destination register, the
+     address registers, and the label of the next statement. *)
+     address registers (low bytes first), and the label of the next
+     statement. *)
   | St_load of Register.t * Register.t * Register.t * Label.t
   (* Store to external memory. Parameters are the address registers, the source
      register, and the label of the next statement. *)
+  (* Store to external memory. Parameters are the address registers (low bytes
+     first), the source register, and the label of the next statement. *)
   | St_store of Register.t * Register.t * Register.t * Label.t
 …
   (* Call to a function given its address. Parameters are the registers holding
+     the address of the function, the arguments of the function, the destination
+     registers, and the label of the next statement. *)
+     the address of the function (low bytes first), the arguments of the
+     function, the destination registers, and the label of the next
+     statement. *)
   | St_call_ptr of Register.t * Register.t * Register.t list * registers *
                    Label.t
+      Label.t
   (* Tail call to a function given its name. Parameters are the name of the
 …
   (* Tail call to a function given its address. Parameters are the registers
+     holding the address of the function, and the arguments of the function. *)
+     holding the address of the function (low bytes first), and the arguments of
+     the function. *)
   | St_tailcall_ptr of Register.t * Register.t * Register.t list
 …
   (* Return the value of some registers. Their may be no register in case of
      procedures, one register when returning an integer, or two registers when
      returning an address. *)
+     returning an address (low bytes first). *)
   | St_return of registers
 …
       f_runiverse : Register.universe ;
       f_sig       : AST.signature ;
       f_result    : Register.t list ;
+      f_result    : Register.t list (* low byte first *) ;
       f_params    : Register.t list ;
       f_locals    : Register.Set.t ;

Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

-                      r619
+                      r740
       graph    : RTL.graph ;
       pc       : Label.t ;
       sp       : Val.t ;
+      sp       : Val.address ;
       lenv     : local_env ;
       carry    : Val.t }
 …
 type state =
   | State of stack_frame list * RTL.graph * Label.t * Val.t (* sp *) *
+  | State of stack_frame list * RTL.graph * Label.t * Val.address (* sp *) *
              local_env * Val.t (* carry *) * memory * CostLabel.t list
   | CallState of stack_frame list * RTL.function_def *
 …
                    memory * CostLabel.t list
+let string_of_local_env lenv =
+  let f x v s =
+    s ^
+      (if Val.eq v Val.undef then ""
+       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
+  Register.Map.fold f lenv ""
+let string_of_args args =
+  let f s v = s ^ " " ^ (Val.to_string v) in
+  List.fold_left f "" args
+let print_state = function
+  | State (_, _, lbl, sp, lenv, carry, mem, _) ->
+    Printf.printf "Stack pointer: %s\n\nCarry: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
+      (Val.string_of_address sp)
+      (Val.to_string carry)
+      (string_of_local_env lenv)
+      (Mem.to_string mem)
+      lbl
+  | CallState (_, _, args, mem, _) ->
+    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
+      (Mem.to_string mem)
+      (string_of_args args)
+  | ReturnState (_, vs, mem, _) ->
+    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
+      (Mem.to_string mem)
+      (string_of_args vs)
 let find_function mem f =
   let v = Mem.find_global mem f in
   Mem.find_fun_def mem v
+  let addr = Mem.find_global mem f in
+  Mem.find_fun_def mem addr
 let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
 …
 let get_local_addr lenv f1 f2 =
+  Val.merge (List.map (get_local_value lenv) [f1 ; f2])
+(* An address is represented by two pseudo-registers (because in 8051, addresses
+   are coded on two bytes). Thus, assignments may involve several
+   registers. When we want to assign a single value to several registers, we
+   break the value into as many parts as there are registers, and then we update
+   each register with a part of the value. *)
+let adds rs v lenv = match rs with
+  | [] -> lenv
+  | _ ->
+    let vs = Val.break v (List.length rs) in
+    let f lenv r v = Register.Map.add r v lenv in
+    List.fold_left2 f lenv rs vs
+  List.map (get_local_value lenv) [f1 ; f2]
+let adds rs vs lenv =
+  let f lenv r v = Register.Map.add r v lenv in
+  List.fold_left2 f lenv rs vs
 (* Assign a value to some destinations registers. *)
 let assign_state cs c lbl sp lenv carry mem t destrs v =
   let lenv = adds destrs v lenv in
   State (cs, c, lbl, sp, lenv, carry, mem, t)
+let assign_state sfrs graph lbl sp lenv carry mem trace destrs vs =
+  let lenv = adds destrs vs lenv in
+  State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
 (* Branch on a value. *)
 let branch_state cs c lbl_true lbl_false sp lenv carry mem t v =
+let branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v =
   let next_lbl =
     if Val.is_true v then lbl_true
 …
       if Val.is_false v then lbl_false
       else error "Undefined conditional value." in
   State (cs, c, next_lbl, sp, lenv, carry, mem, t)
+  State (sfrs, graph, next_lbl, sp, lenv, carry, mem, trace)
 …
 let interpret_statement
     (cs    : stack_frame list)
     (c     : RTL.graph)
     (sp    : Val.t)
+    (sfrs  : stack_frame list)
+    (graph : RTL.graph)
+    (sp    : Val.address)
     (lenv  : local_env)
     (carry : Val.t)
     (mem   : memory)
     (stmt  : RTL.statement)
     (t     : CostLabel.t list) :
+    (trace : CostLabel.t list) :
     state = match stmt with
       | RTL.St_skip lbl ->
         State (cs, c, lbl, sp, lenv, carry, mem, t)
+        State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
       | RTL.St_cost (cost_lbl, lbl) ->
         State (cs, c, lbl, sp, lenv, carry, mem, cost_lbl :: t)
+        State (sfrs, graph, lbl, sp, lenv, carry, mem, cost_lbl :: trace)
       | RTL.St_addr (r1, r2, x, lbl) ->
         assign_state cs c lbl sp lenv carry mem t [r1 ; r2]
+        assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2]
           (Mem.find_global mem x)
       | RTL.St_stackaddr (r1, r2, lbl) ->
         assign_state cs c lbl sp lenv carry mem t [r1 ; r2] sp
+        assign_state sfrs graph lbl sp lenv carry mem trace [r1 ; r2] sp
       | RTL.St_int (r, i, lbl) ->
         assign_state cs c lbl sp lenv carry mem t [r] (Val.of_int i)
+        assign_state sfrs graph lbl sp lenv carry mem trace [r] [Val.of_int i]
       | RTL.St_move (destr, srcr, lbl) ->
         assign_state cs c lbl sp lenv carry mem t [destr]
           (get_local_value lenv srcr)
+        assign_state sfrs graph lbl sp lenv carry mem trace [destr]
+          [get_local_value lenv srcr]
       | RTL.St_opaccs (opaccs, destr, srcr1, srcr2, lbl) ->
 …
             (get_local_value lenv srcr1)
             (get_local_value lenv srcr2) in
         assign_state cs c lbl sp lenv carry mem t [destr] v
+        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
       | RTL.St_op1 (op1, destr, srcr, lbl) ->
         let v = Eval.op1 op1 (get_local_value lenv srcr) in
         assign_state cs c lbl sp lenv carry mem t [destr] v
+        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
       | RTL.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
 …
             (get_local_value lenv srcr1)
             (get_local_value lenv srcr2) in
         assign_state cs c lbl sp lenv carry mem t [destr] v
+        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
       | RTL.St_clear_carry lbl ->
         State (cs, c, lbl, sp, lenv, Val.zero, mem, t)
+        State (sfrs, graph, lbl, sp, lenv, Val.zero, mem, trace)
       | RTL.St_load (destr, addr1, addr2, lbl) ->
+        let dph = get_local_value lenv addr1 in
+        let dpl = get_local_value lenv addr2 in
+        let addr = Val.merge [dph ; dpl] in
+        let v = Mem.load2 mem chunk addr in
+        assign_state cs c lbl sp lenv carry mem t [destr] v
+        let addr = get_local_addr lenv addr1 addr2 in
+        let v = Mem.load mem chunk addr in
+        assign_state sfrs graph lbl sp lenv carry mem trace [destr] [v]
       | RTL.St_store (addr1, addr2, srcr, lbl) ->
+        let dph = get_local_value lenv addr1 in
+        let dpl = get_local_value lenv addr2 in
+        let addr = Val.merge [dph ; dpl] in
+        let mem = Mem.store2 mem chunk addr (get_local_value lenv srcr) in
+        State (cs, c, lbl, sp, lenv, carry, mem, t)
+        let addr = get_local_addr lenv addr1 addr2 in
+        let mem = Mem.store mem chunk addr (get_local_value lenv srcr) in
+        State (sfrs, graph, lbl, sp, lenv, carry, mem, trace)
       | RTL.St_call_id (f, args, ret_regs, lbl) ->
 …
         let args = get_arg_values lenv args in
         let sf =
           { ret_regs = ret_regs ; graph = c ; pc = lbl ;
+          { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
             sp = sp ; lenv = lenv ; carry = carry }
         in
         CallState (sf :: cs, f_def, args, mem, t)
+        CallState (sf :: sfrs, f_def, args, mem, trace)
       | RTL.St_call_ptr (f1, f2, args, ret_regs, lbl) ->
 …
         let f_def = Mem.find_fun_def mem addr in
         let args = get_arg_values lenv args in
         let sf = { ret_regs = ret_regs ; graph = c ; pc = lbl ;
+        let sf = { ret_regs = ret_regs ; graph = graph ; pc = lbl ;
                    sp = sp ; lenv = lenv ; carry = carry } in
         CallState (sf :: cs, f_def, args, mem, t)
+        CallState (sf :: sfrs, f_def, args, mem, trace)
       | RTL.St_tailcall_id (f, args) ->
 …
         let args = get_arg_values lenv args in
         let mem = Mem.free mem sp in
         CallState (cs, f_def, args, mem, t)
+        CallState (sfrs, f_def, args, mem, trace)
       | RTL.St_tailcall_ptr (f1, f2, args) ->
 …
         let args = get_arg_values lenv args in
         let mem = Mem.free mem sp in
         CallState (cs, f_def, args, mem, t)
+        CallState (sfrs, f_def, args, mem, trace)
       | RTL.St_condacc (srcr, lbl_true, lbl_false) ->
         let v = get_local_value lenv srcr in
         branch_state cs c lbl_true lbl_false sp lenv carry mem t v
+        branch_state sfrs graph lbl_true lbl_false sp lenv carry mem trace v
       | RTL.St_return rl ->
         let vl = List.map (get_local_value lenv) rl in
         let mem = Mem.free mem sp in
+        ReturnState (cs, vl, mem, t)
+let get_int () =
+  try Val.of_int (int_of_string (read_line ()))
+  with Failure "int_of_string" -> error "Failed to scan an integer."
+let get_float () =
+  try Val.of_float (float_of_string (read_line ()))
+  with Failure "float_of_string" -> error "Failed to scan a float."
+let interpret_external
+    (mem  : memory)
+    (def  : AST.external_function)
+    (args : Val.t list) :
+    memory * Val.t list =
+  match def.AST.ef_tag, args with
+    | s, _ when s = Primitive.scan_int ->
+      (mem, [get_int ()])
+    | "scan_float", _ ->
+      (mem, [get_float ()])
+    | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
+      Printf.printf "%d" (Val.to_int v) ;
+      (mem, [Val.zero])
+    | "print_float", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, [Val.zero])
+    | "print_ptr", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, [Val.zero])
+    | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
+      Printf.printf "%d\n" (Val.to_int v) ;
+      (mem, [Val.zero])
+    | "print_floatln", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, [Val.zero])
+    | "print_ptrln", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s\n"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, [Val.zero])
+    | s, v :: _ when s = Primitive.alloc ->
+      let (mem, ptr) = Mem.alloc mem (Val.to_int v) in
+      let vs = Val.break ptr 2 in
+      (mem, vs)
+    | s, v1 :: v2 :: _ when s = Primitive.modulo ->
+      (mem, [Val.modulo v1 v2])
+    (* The other cases are either a type error (only integers and pointers
+       may not be differenciated during type checking) or an unknown
+       function. *)
+    | "print_int", _ | "print_intln", _ ->
+      error "Illegal cast from pointer to integer."
+    | "print_ptr", _ | "print_ptrln", _ ->
+      error "Illegal cast from integer to pointer."
+    | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
+        ReturnState (sfrs, vl, mem, trace)
+module InterpretExternal = Primitive.Interpret (Mem)
+let interpret_external mem f args = match InterpretExternal.t mem f args with
+  | (mem', InterpretExternal.V v) -> (mem', [v])
+  | (mem', InterpretExternal.A addr) -> (mem', addr)
 let init_locals
 …
 let state_after_call
     (cs    : stack_frame list)
+    (sfrs  : stack_frame list)
     (f_def : RTL.function_def)
     (args  : Val.t list)
     (mem   : memory)
     (t     : CostLabel.t list) :
+    (trace : CostLabel.t list) :
     state =
   match f_def with
     | RTL.F_int def ->
       let (mem', sp) = Mem.alloc mem def.RTL.f_stacksize in
       State (cs, def.RTL.f_graph, def.RTL.f_entry, sp,
+      State (sfrs, def.RTL.f_graph, def.RTL.f_entry, sp,
              init_locals def.RTL.f_locals def.RTL.f_params args,
              Val.undef, mem', t)
+             Val.undef, mem', trace)
     | RTL.F_ext def ->
       let (mem', vs) = interpret_external mem def args in
       ReturnState (cs, vs, mem', t)
+      let (mem', vs) = interpret_external mem def.AST.ef_tag args in
+      ReturnState (sfrs, vs, mem', trace)
 let state_after_return
     (sf       : stack_frame)
     (cs       : stack_frame list)
+    (sfrs     : stack_frame list)
     (ret_vals : Val.t list)
     (mem      : memory)
     (t        : CostLabel.t list) :
+    (trace    : CostLabel.t list) :
     state =
   let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
   let lenv = MiscPottier.foldi f sf.lenv sf.ret_regs in
   State (cs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, t)
+  State (sfrs, sf.graph, sf.pc, sf.sp, lenv, sf.carry, mem, trace)
 let small_step (st : state) : state = match st with
   | State (cs, graph, pc, sp, lenv, carry, mem, t) ->
+  | State (sfrs, graph, pc, sp, lenv, carry, mem, trace) ->
     let stmt = Label.Map.find pc graph in
     interpret_statement cs graph sp lenv carry mem stmt t
   | CallState (cs, f_def, args, mem, t) ->
     state_after_call cs f_def args mem t
   | ReturnState ([], ret_vals, mem, t) ->
+    interpret_statement sfrs graph sp lenv carry mem stmt trace
+  | CallState (sfrs, f_def, args, mem, trace) ->
+    state_after_call sfrs f_def args mem trace
+  | ReturnState ([], ret_vals, mem, trace) ->
     assert false (* End of execution; handled in iter_small_step. *)
+  | ReturnState (sf :: cs, ret_vals, mem, t) ->
+    state_after_return sf cs ret_vals mem t
+let print_args = MiscPottier.string_of_list ", " Val.to_string
+let print_ret_vals = MiscPottier.string_of_list ", " Val.to_string
+let print_lenv =
+  Register.Map.iter (fun r v -> Printf.printf "%s = %s\n%!"
+    (Register.print r) (Val.to_string v))
+  | ReturnState (sf :: sfrs, ret_vals, mem, trace) ->
+    state_after_return sf sfrs ret_vals mem trace
 let compute_result vs =
   try
     let v = MiscPottier.last vs in
+    let v = List.hd vs in
     if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
     else IntValue.Int8.zero
   with Not_found -> IntValue.Int8.zero
+let rec iter_small_step print_result st = match small_step st with
+(*
+  (* <DEBUG> *)
+  | ReturnState ([], vs, mem, t) ->
+    Mem.print mem ;
+    Printf.printf "Return: %s\n%!" (print_ret_vals vs) ;
+    List.rev t
+  | CallState (_, _, args, mem, _) as st' ->
+    Printf.printf "Call state: %s\n%!" (print_args args) ;
+    Mem.print mem ;
+    iter_small_step st'
+  | ReturnState (_, ret_vals, mem, _) as st' ->
+    Printf.printf "Return state: %s\n%!" (print_ret_vals ret_vals) ;
+    Mem.print mem ;
+    iter_small_step st'
+  | State (_, _, pc, sp, lenv, carry, mem, _) as st' ->
+    Printf.printf "State: PC = %s ; SP = %s\n%!" pc (Val.to_string sp) ;
+    Mem.print mem ;
+    print_lenv lenv ;
+    Printf.printf "Carry = %s\n\n%!" (Val.to_string carry) ;
+    iter_small_step st'
+  (* </DEBUG> *)
+*)
+  | ReturnState ([], vs, mem, t) ->
+    let (res, cost_labels) as trace = (compute_result vs, List.rev t) in
+    if print_result then
+      Printf.printf "RTL: %s\n%!" (IntValue.Int8.to_string res) ;
+    trace
+  | st' -> iter_small_step print_result st'
+let rec iter_small_step debug st =
+  if debug then print_state st ;
+  match small_step st with
+    | ReturnState ([], vs, mem, trace) -> (compute_result vs, List.rev trace)
+    | st' -> iter_small_step debug st'
 …
 (* The memory is initialized by load the code into it, and by reserving space
+(* The memory is initialized by loading the code into it, and by reserving space
    for the global variables. *)
 …
 (* Interpret the program only if it has a main. *)
+let interpret print_result p = match p.RTL.main with
+  | None -> (IntValue.Int8.zero, [])
+  | Some main ->
+    let mem = init_mem p in
+    let main_def = find_function mem main in
+    let st = CallState ([], main_def, [], mem, []) in
+    iter_small_step print_result st
+let interpret debug p =
+  if debug then Printf.printf "*** RTL ***\n\n%!" ;
+  match p.RTL.main with
+    | None -> (IntValue.Int8.zero, [])
+    | Some main ->
+      let mem = init_mem p in
+      let main_def = find_function mem main in
+      let st = CallState ([], main_def, [], mem, []) in
+      iter_small_step debug st

Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

-                      r624
+                      r740
   let (def, tmpr) = fresh_reg def in
   adds_graph
     [ERTL.St_framesize (addr2, start_lbl) ;
+    [ERTL.St_framesize (addr1, start_lbl) ;
      ERTL.St_int (tmpr, off+I8051.int_size, start_lbl) ;
      ERTL.St_op2 (I8051.Sub, addr2, addr2, tmpr, start_lbl) ;
+     ERTL.St_op2 (I8051.Sub, addr1, addr1, tmpr, start_lbl) ;
      ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
      ERTL.St_op2 (I8051.Add, addr2, addr2, tmpr, start_lbl) ;
      ERTL.St_int (addr1, 0, start_lbl) ;
+     ERTL.St_op2 (I8051.Add, addr1, addr1, tmpr, start_lbl) ;
+     ERTL.St_int (addr2, 0, start_lbl) ;
      ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
      ERTL.St_op2 (I8051.Addc, addr1, addr1, tmpr, start_lbl) ;
+     ERTL.St_op2 (I8051.Addc, addr2, addr2, tmpr, start_lbl) ;
      ERTL.St_load (destr, addr1, addr2, start_lbl)]
     start_lbl dest_lbl def
 …
   (get_params_hdw hdw_params) @ (get_params_stack stack_params)
 let add_prologue params srah sral sregs def =
+let add_prologue params sral srah sregs def =
   let start_lbl = def.ERTL.f_entry in
   let tmp_lbl = fresh_label def in
 …
       let (def, r_tmp) = fresh_reg def in
       adds_graph [ERTL.St_int (r_tmp, 0, start_lbl) ;
                   ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl) ;
                   ERTL.St_set_hdw (I8051.st0, r, start_lbl)]
+                  ERTL.St_set_hdw (I8051.st0, r, start_lbl) ;
+                  ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl)]
         start_lbl dest_lbl def]
   | r1 :: r2 :: _ ->
     [(fun start_lbl ->
       adds_graph [ERTL.St_set_hdw (I8051.st1, r1, start_lbl) ;
                   ERTL.St_set_hdw (I8051.st0, r2, start_lbl)] start_lbl)]
 let add_epilogue ret_regs srah sral sregs def =
+      adds_graph [ERTL.St_set_hdw (I8051.st0, r1, start_lbl) ;
+                  ERTL.St_set_hdw (I8051.st1, r2, start_lbl)] start_lbl)]
+let add_epilogue ret_regs sral srah sregs def =
   let start_lbl = def.ERTL.f_exit in
   let tmp_lbl = fresh_label def in
 …
        (* assign the result to actual return registers *)
        [adds_graph [ERTL.St_comment ("Set result", start_lbl)]] @
        [adds_graph [ERTL.St_hdw_to_hdw (I8051.dph, I8051.st1, start_lbl) ;
                     ERTL.St_hdw_to_hdw (I8051.dpl, I8051.st0, start_lbl) ;
+       [adds_graph [ERTL.St_hdw_to_hdw (I8051.dpl, I8051.st0, start_lbl) ;
+                    ERTL.St_hdw_to_hdw (I8051.dph, I8051.st1, start_lbl) ;
                     ERTL.St_comment ("End Epilogue", start_lbl)]])
       start_lbl tmp_lbl def in
 …
   (* Allocate registers to hold the return address. *)
   let (def, sra) = fresh_regs def 2 in
   let srah = List.nth sra 0 in
   let sral = List.nth sra 1 in
+  let sral = List.nth sra 0 in
+  let srah = List.nth sra 1 in
   (* Allocate registers to save callee-saved registers. *)
   let (def, sregs) = allocate_regs I8051.callee_saved def in
   (* Add a prologue and a epilogue. *)
   let def = add_prologue params srah sral sregs def in
   let def = add_epilogue ret_regs srah sral sregs def in
+  let def = add_prologue params sral srah sregs def in
+  let def = add_epilogue ret_regs sral srah sregs def in
   def
 …
      ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
      ERTL.St_clear_carry start_lbl ;
+     ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ;
+     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
+     ERTL.St_int (addr2, 0, start_lbl) ;
      ERTL.St_op2 (I8051.Sub, addr2, tmpr, addr2, start_lbl) ;
-     ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
-     ERTL.St_int (addr1, 0, start_lbl) ;
-     ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ;
      ERTL.St_store (addr1, addr2, srcr, start_lbl)]
     start_lbl dest_lbl def
 …
   | r1 :: r2 :: _ ->
     adds_graph
       [ERTL.St_hdw_to_hdw (I8051.st1, I8051.dph, start_lbl) ;
        ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ;
        ERTL.St_get_hdw (r1, I8051.st1, start_lbl) ;
        ERTL.St_get_hdw (r2, I8051.st0, start_lbl)]
+      [ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ;
+       ERTL.St_hdw_to_hdw (I8051.st1, I8051.dph, start_lbl) ;
+       ERTL.St_get_hdw (r1, I8051.st0, start_lbl) ;
+       ERTL.St_get_hdw (r2, I8051.st1, start_lbl)]
       start_lbl
 …
   | RTL.St_addr (r1, r2, x, lbl') ->
     adds_graph
       [ERTL.St_addrH (r1, x, lbl) ; ERTL.St_addrL (r2, x, lbl) ;]
+      [ERTL.St_addrL (r1, x, lbl) ; ERTL.St_addrH (r2, x, lbl) ;]
       lbl lbl' def
   | RTL.St_stackaddr (r1, r2, lbl') ->
     adds_graph
       [ERTL.St_get_hdw (r1, I8051.sph, lbl) ;
        ERTL.St_get_hdw (r2, I8051.spl, lbl)]
+      [ERTL.St_get_hdw (r1, I8051.spl, lbl) ;
+       ERTL.St_get_hdw (r2, I8051.sph, lbl)]
       lbl lbl' def

Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli

-                      r486
+                      r740
    RTLabs is the last language of the frontend. It is intended to
    ease retargetting. *)
-(* From the RTLabs point of view, a pseudo-register can represent a physical
-   location or a pointer. When instruction selection is over, a pseudo-register
-   represents a physical location. Thus, some operations --- those on pointers
-   --- may involve several pseudo-registers when a pointer value is more than
-   one physical location (which is the case of the 8051). *)
-type registers = Register.t list
 …
   | St_cost of CostLabel.t * Label.t
   (* Assign a constant to registers. Parameters are the destination registers,
+  (* Assign a constant to registers. Parameters are the destination register,
      the constant and the label of the next statement. *)
   | St_cst of registers * AST.cst * Label.t
+  | St_cst of Register.t * AST.cst * Label.t
   (* Application of an unary operation. Parameters are the operation, the
      destination registers, the argument registers and the label of the next
+     destination register, the argument register and the label of the next
      statement. *)
   | St_op1 of AST.op1 * registers * registers * Label.t
+  | St_op1 of AST.op1 * Register.t * Register.t * Label.t
   (* Application of a binary operation. Parameters are the operation, the
      destination register, the argument registers and the label of the next
+     destination register, the two argument registers and the label of the next
      statement. *)
   | St_op2 of AST.op2 * registers * registers * registers * Label.t
+  | St_op2 of AST.op2 * Register.t * Register.t * Register.t * Label.t
   (* Memory load. Parameters are the size and type of what to load,
      the addressing mode and its arguments, the destination register
      and the label of the next statement. *)
   | St_load of Memory.memory_q * addressing * registers list *
                registers * Label.t
+  (* Memory load. Parameters are the size in bytes of what to load, the
+     addressing mode and its arguments, the destination register and the label
+     of the next statement. *)
+  | St_load of Memory.quantity * addressing * Register.t list * Register.t *
+               Label.t
   (* Memory store. Parameters are the size and type of what to store,
      the addressing mode and its arguments, the source register
      and the label of the next statement. *)
   | St_store of Memory.memory_q * addressing * registers list *
                 registers * Label.t
+  (* Memory store. Parameters are the size in bytes of what to store, the
+     addressing mode and its arguments, the source register and the label of the
+     next statement. *)
+  | St_store of Memory.quantity * addressing * Register.t list * Register.t *
+                Label.t
   (* Call to a function given its name. Parameters are the name of the
      function, the arguments of the function, the destination
      registers, the signature of the function and the label of the next
+     register, the signature of the function and the label of the next
      statement. *)
   | St_call_id of AST.ident * registers list * registers *
+  | St_call_id of AST.ident * Register.t list * Register.t *
                   AST.signature * Label.t
   (* Call to a function given its address. Parameters are registers
+  (* Call to a function given its address. Parameters are the register
      holding the address of the function, the arguments of the
      function, the destination registers, the signature of the function
+     function, the destination register, the signature of the function
      and the label of the next statement. This statement with an
      [St_op] before can represent a [St_call_id]. However, we
      differenciate the two to allow translation to a formalism with no
      function pointer. *)
   | St_call_ptr of registers * registers list * registers *
+  | St_call_ptr of Register.t * Register.t list * Register.t *
                    AST.signature * Label.t
+  (* Tail call to a function given its name. Parameters are the name
+     of the function, the arguments of the function, the destination
+     register, the signature of the function and the label of the next
+     statement. *)
+  | St_tailcall_id of AST.ident * registers list * AST.signature
+  (* Tail call to a function given its name. Parameters are the name of the
+     function, the arguments of the function, the signature of the function and
+     the label of the next statement. *)
+  | St_tailcall_id of AST.ident * Register.t list * AST.signature
+  (* Tail call to a function given its address. Parameters are a
+     register holding the address of the function, the arguments of
+     the function, the destination register, the signature of the
+     function and the label of the next statement. Same remark as for
+     the [St_call_ptr]. *)
+  | St_tailcall_ptr of registers * registers list * AST.signature
+  (* Tail call to a function given its address. Parameters are a register
+     holding the address of the function, the arguments of the function, the
+     signature of the function and the label of the next statement. Same remark
+     as for the [St_call_ptr]. *)
+  | St_tailcall_ptr of Register.t * Register.t list * AST.signature
   (* Constant branch. Parameters are the constant, the label to go to when the
 …
      true (not 0), and the label to go to when the operation on the
      argument evaluates to false (0). *)
   | St_cond1 of AST.op1 * registers * Label.t * Label.t
+  | St_cond1 of AST.op1 * Register.t * Label.t * Label.t
   (* Binary branch. Parameters are the operation, its arguments, the
 …
      true (not 0), and the label to go to when the operation on the
      arguments evaluates to false (0). *)
   | St_cond2 of AST.op2 * registers * registers * Label.t * Label.t
+  | St_cond2 of AST.op2 * Register.t * Register.t * Label.t * Label.t
   (* Jump statement. Parameters are a register and a list of
      labels. The execution will go to the [n]th label of the list of
      labels, where [n] is the natural value held in the register. *)
   | St_jumptable of registers * Label.t list
+  | St_jumptable of Register.t * Label.t list
   (* Return statement. *)
   | St_return of registers
+  | St_return of Register.t
 …
       f_runiverse : Register.universe ;
       f_sig       : AST.signature ;
+      f_result    : registers ;
+      f_params    : registers list ;
+      f_locals    : registers list ;
+      f_result    : Register.t ;
+      f_params    : Register.t list ;
+      f_locals    : Register.t list ;
+      f_ptrs      : Register.t list ;
       f_stacksize : int ;
       f_graph     : graph ;

Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

-                      r619
+                      r740
 module Mem = Driver.RTLabsMemory
 module Val = Mem.Value
+let error_float () = error "float not supported"
 …
 type stack_frame =
     { ret_regs : Register.t list ;
+    { ret_reg  : Register.t ;
       graph    : RTLabs.graph ;
       sp       : Val.t ;
+      sp       : Val.address ;
       pc       : Label.t ;
       lenv     : local_env }
 …
 type state =
   | State of stack_frame list * RTLabs.graph * Val.t (* stack pointer *) *
+  | State of stack_frame list * RTLabs.graph * Val.address (* stack pointer *) *
              Label.t * local_env * memory * CostLabel.t list
   | CallState of stack_frame list * RTLabs.function_def *
 …
                    memory * CostLabel.t list
+let string_of_local_env lenv =
+  let f x v s =
+    s ^
+      (if Val.eq v Val.undef then ""
+       else (Register.print x) ^ " = " ^ (Val.to_string v) ^ "  ") in
+  Register.Map.fold f lenv ""
+let string_of_args args =
+  let f s v = s ^ " " ^ (Val.to_string v) in
+  List.fold_left f "" args
+let print_state = function
+  | State (_, _, sp, lbl, lenv, mem, _) ->
+    Printf.printf "Stack pointer: %s\n\nLocal environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
+      (Val.string_of_address sp)
+      (string_of_local_env lenv)
+      (Mem.to_string mem)
+      lbl
+  | CallState (_, _, args, mem, _) ->
+    Printf.printf "Memory:%s\nCall state: %s\n\n%!"
+      (Mem.to_string mem)
+      (string_of_args args)
+  | ReturnState (_, v, mem, _) ->
+    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
+      (Mem.to_string mem)
+      (Val.to_string v)
 let find_function mem f =
   let v = Mem.find_global mem f in
   Mem.find_fun_def mem v
+  let addr = Mem.find_global mem f in
+  Mem.find_fun_def mem addr
 let get_local_value (lenv : local_env) (r : Register.t) : Val.t =
 …
 let get_arg_values lenv args = List.map (get_local_value lenv) args
+let get_local_valuel (lenv : local_env) (rl : Register.t list) : Val.t =
+  let vl = List.map (get_local_value lenv) rl in
+  Val.merge vl
+let get_arg_valuesl lenv argsl = List.map (get_local_valuel lenv) argsl
+(* An address is represented by two pseudo-registers (because in 8051, addresses
+   are coded on two bytes). Thus, assignments may involve several
+   registers. When we want to assign a single value to several registers, we
+   break the value into as many parts as there are registers, and then we update
+   each register with a part of the value. *)
+let adds rs v lenv = match rs with
+  | [] -> lenv
+  | _ ->
+    let vs = Val.break v (List.length rs) in
+    let f lenv r v = Register.Map.add r v lenv in
+    List.fold_left2 f lenv rs vs
+let adds rs vs lenv =
+  let f lenv r v = Register.Map.add r v lenv in
+  List.fold_left2 f lenv rs vs
+let value_of_address = List.hd
+let address_of_value v = [v]
 let eval_addressing
     (mem  : memory)
     (sp   : Val.t)
+    (sp   : Val.address)
     (mode : RTLabs.addressing)
     (args : Val.t list) :
+    Val.t = match mode, args with
+      | RTLabs.Aindexed off, addr :: _ when Val.is_pointer addr ->
+        Val.add addr (Val.of_int off)
+      | RTLabs.Aindexed2, addr :: shift :: _
+        when Val.is_pointer addr && Val.is_int shift ->
+        Val.add addr shift
+      | RTLabs.Aindexed2, shift :: addr :: _
+        when Val.is_pointer addr && Val.is_int shift ->
+        Val.add addr shift
+    Val.address = match mode, args with
+      | RTLabs.Aindexed off, v :: _ ->
+        address_of_value (Val.add v (Val.of_int off))
+      | RTLabs.Aindexed2, v1 :: v2 :: _ ->
+        address_of_value (Val.add v1 v2)
       | RTLabs.Aglobal (id, off), _ ->
         Val.add (Mem.find_global mem id) (Val.of_int off)
+        Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off)
       | RTLabs.Abased (id, off), v :: _ ->
+        let addr = Val.add (Mem.find_global mem id) (Val.of_int off) in
+        Val.add addr v
+        let addr =
+          Val.add_address (Mem.find_global mem id) (Val.Offset.of_int off) in
+        address_of_value (Val.add (value_of_address addr) v)
       | RTLabs.Ainstack off, _ ->
         Val.add sp (Val.of_int off)
+        Val.add_address sp (Val.Offset.of_int off)
       | _, _ -> error "Bad addressing mode."
 …
 let eval_cst mem sp = function
   | AST.Cst_int i -> Val.of_int i
+  | AST.Cst_float f -> Val.of_float f
+  | AST.Cst_addrsymbol id -> Mem.find_global mem id
+  | AST.Cst_stackoffset shift -> Val.add sp (Val.of_int shift)
+  | AST.Cst_float f -> error_float ()
+  | AST.Cst_addrsymbol id -> value_of_address (Mem.find_global mem id)
+  | AST.Cst_stackoffset shift ->
+    value_of_address (Val.add_address sp (Val.Offset.of_int shift))
 let eval_op1 = function
 …
   | AST.Op_notbool -> Val.notbool
   | AST.Op_notint -> Val.notint
   | AST.Op_negf -> Val.negf
   | AST.Op_absf -> Val.absf
   | AST.Op_singleoffloat -> Val.singleoffloat
   | AST.Op_intoffloat -> Val.intoffloat
   | AST.Op_intuoffloat -> Val.intuoffloat
   | AST.Op_floatofint -> Val.floatofint
   | AST.Op_floatofintu -> Val.floatofintu
+  | AST.Op_negf
+  | AST.Op_absf
+  | AST.Op_singleoffloat
+  | AST.Op_intoffloat
+  | AST.Op_intuoffloat
+  | AST.Op_floatofint
+  | AST.Op_floatofintu -> error_float ()
   | AST.Op_id -> (fun (v : Val.t) -> v)
   | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO? *)
+  | AST.Op_intofptr | AST.Op_ptrofint -> assert false (* TODO or not? *)
 let rec eval_op2 = function
 …
   | AST.Op_shr -> Val.shr
   | AST.Op_shru -> Val.shru
-  | AST.Op_addf -> Val.addf
-  | AST.Op_subf -> Val.subf
-  | AST.Op_mulf -> Val.mulf
-  | AST.Op_divf -> Val.divf
   | AST.Op_cmp AST.Cmp_eq -> Val.cmp_eq
   | AST.Op_cmp AST.Cmp_ne -> Val.cmp_ne
 …
   | AST.Op_cmpu AST.Cmp_gt -> Val.cmp_gt_u
   | AST.Op_cmpu AST.Cmp_ge -> Val.cmp_ge_u
-  | AST.Op_cmpf AST.Cmp_eq -> Val.cmp_eq_f
-  | AST.Op_cmpf AST.Cmp_ne -> Val.cmp_ne_f
-  | AST.Op_cmpf AST.Cmp_lt -> Val.cmp_lt_f
-  | AST.Op_cmpf AST.Cmp_le -> Val.cmp_le_f
-  | AST.Op_cmpf AST.Cmp_gt -> Val.cmp_gt_f
-  | AST.Op_cmpf AST.Cmp_ge -> Val.cmp_ge_f
   | AST.Op_cmpp cmp -> eval_op2 (AST.Op_cmp cmp)
+  | AST.Op_addf
+  | AST.Op_subf
+  | AST.Op_mulf
+  | AST.Op_divf
+  | AST.Op_cmpf _ -> error_float ()
 (* Assign a value to some destinations registers. *)
 let assign_state cs c sp lbl lenv mem t destrs v =
   let lenv = adds destrs v lenv in
   State (cs, c, sp, lbl, lenv, mem, t)
+let assign_state sfrs graph sp lbl lenv mem trace destr v =
+  let lenv = Register.Map.add destr v lenv in
+  State (sfrs, graph, sp, lbl, lenv, mem, trace)
 (* Branch on a value. *)
 let branch_state cs c sp lbl_true lbl_false lenv mem t v =
+let branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v =
   let next_lbl =
     if Val.is_true v then lbl_true
 …
       if Val.is_false v then lbl_false
       else error "Undefined conditional value." in
   State (cs, c, sp, next_lbl, lenv, mem, t)
+  State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
 …
 let interpret_statement
     (cs   : stack_frame list)
     (c    : RTLabs.graph)
     (sp   : Val.t)
     (lenv : local_env)
     (mem  : memory)
     (stmt : RTLabs.statement)
     (t    : CostLabel.t list) :
+    (sfrs  : stack_frame list)
+    (graph : RTLabs.graph)
+    (sp    : Val.address)
+    (lenv  : local_env)
+    (mem   : memory)
+    (stmt  : RTLabs.statement)
+    (trace : CostLabel.t list) :
     state = match stmt with
       | RTLabs.St_skip lbl -> State (cs, c, sp, lbl, lenv, mem, t)
+      | RTLabs.St_skip lbl -> State (sfrs, graph, sp, lbl, lenv, mem, trace)
       | RTLabs.St_cost (cost_lbl, lbl) ->
         State (cs, c, sp, lbl, lenv, mem, cost_lbl :: t)
       | RTLabs.St_cst (destrs, cst, lbl) ->
+        State (sfrs, graph, sp, lbl, lenv, mem, cost_lbl :: trace)
+      | RTLabs.St_cst (destr, cst, lbl) ->
         let v = eval_cst mem sp cst in
         assign_state cs c sp lbl lenv mem t destrs v
       | RTLabs.St_op1 (op1, destrs, srcrs, lbl) ->
         let v = eval_op1 op1 (get_local_valuel lenv srcrs) in
         assign_state cs c sp lbl lenv mem t destrs v
       | RTLabs.St_op2 (op2, destrs, srcrs1, srcrs2, lbl) ->
+        assign_state sfrs graph sp lbl lenv mem trace destr v
+      | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
+        let v = eval_op1 op1 (get_local_value lenv srcr) in
+        assign_state sfrs graph sp lbl lenv mem trace destr v
+      | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
         let v =
           eval_op2 op2
+            (get_local_valuel lenv srcrs1)
+            (get_local_valuel lenv srcrs2) in
+        assign_state cs c sp lbl lenv mem t destrs v
+      | RTLabs.St_load (chunk, mode, args, destrs, lbl) ->
+        let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in
+        let v = Mem.load mem chunk addr in
+        assign_state cs c sp lbl lenv mem t destrs v
+      | RTLabs.St_store (chunk, mode, args, srcrs, lbl) ->
+        let addr = eval_addressing mem sp mode (get_arg_valuesl lenv args) in
+        let mem = Mem.store mem chunk addr (get_local_valuel lenv srcrs) in
+        State (cs, c, sp, lbl, lenv, mem, t)
+            (get_local_value lenv srcr1)
+            (get_local_value lenv srcr2) in
+        assign_state sfrs graph sp lbl lenv mem trace destr v
+      | RTLabs.St_load (q, mode, args, destr, lbl) ->
+        let addr = eval_addressing mem sp mode (get_arg_values lenv args) in
+        let v = Mem.loadq mem q addr in
+        assign_state sfrs graph sp lbl lenv mem trace destr v
+      | RTLabs.St_store (q, mode, args, srcr, lbl) ->
+        let addr = eval_addressing mem sp mode (get_arg_values lenv args) in
+        let v = get_local_value lenv srcr in
+        let mem = Mem.storeq mem q addr v in
+        State (sfrs, graph, sp, lbl, lenv, mem, trace)
       | RTLabs.St_call_id (f, args, destr, sg, lbl) ->
         let f_def = find_function mem f in
         let args = get_arg_valuesl lenv args in
+        let args = get_arg_values lenv args in
         (* Save the stack frame. *)
         let sf =
           { ret_regs = destr ; graph = c ; sp = sp ; pc = lbl ; lenv = lenv }
+          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
         in
         CallState (sf :: cs, f_def, args, mem, t)
       | RTLabs.St_call_ptr (rs, args, destrs, sg, lbl) ->
         let addr = get_local_valuel lenv rs in
         let f_def = Mem.find_fun_def mem addr in
         let args = get_arg_valuesl lenv args in
+        CallState (sf :: sfrs, f_def, args, mem, trace)
+      | RTLabs.St_call_ptr (r, args, destr, sg, lbl) ->
+        let addr = get_local_value lenv r in
+        let f_def = Mem.find_fun_def mem (address_of_value addr) in
+        let args = get_arg_values lenv args in
         (* Save the stack frame. *)
         let sf =
           { ret_regs = destrs ; graph = c ; sp = sp ; pc = lbl ; lenv = lenv }
+          { ret_reg = destr ; graph = graph ; sp = sp ; pc = lbl ; lenv = lenv }
         in
         CallState (sf :: cs, f_def, args, mem, t)
+        CallState (sf :: sfrs, f_def, args, mem, trace)
       | RTLabs.St_tailcall_id (f, args, sg) ->
         let f_def = find_function mem f in
         let args = get_arg_valuesl lenv args in
+        let args = get_arg_values lenv args in
         (* No need to save the stack frame. But free the stack. *)
         let mem = Mem.free mem sp in
         CallState (cs, f_def, args, mem, t)
       | RTLabs.St_tailcall_ptr (rs, args, sg) ->
         let addr = get_local_valuel lenv rs in
         let f_def = Mem.find_fun_def mem addr in
         let args = get_arg_valuesl lenv args in
+        CallState (sfrs, f_def, args, mem, trace)
+      | RTLabs.St_tailcall_ptr (r, args, sg) ->
+        let addr = get_local_value lenv r in
+        let f_def = Mem.find_fun_def mem (address_of_value addr) in
+        let args = get_arg_values lenv args in
         (* No need to save the stack frame. But free the stack. *)
         let mem = Mem.free mem sp in
         CallState (cs, f_def, args, mem, t)
+        CallState (sfrs, f_def, args, mem, trace)
       | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
         let v = eval_cst mem sp cst in
         branch_state cs c sp lbl_true lbl_false lenv mem t v
       | RTLabs.St_cond1 (op1, srcrs, lbl_true, lbl_false) ->
         let v = eval_op1 op1 (get_local_valuel lenv srcrs) in
         branch_state cs c sp lbl_true lbl_false lenv mem t v
       | RTLabs.St_cond2 (op2, srcrs1, srcrs2, lbl_true, lbl_false) ->
+        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
+      | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
+        let v = eval_op1 op1 (get_local_value lenv srcr) in
+        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
+      | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
         let v =
           eval_op2 op2
             (get_local_valuel lenv srcrs1)
             (get_local_valuel lenv srcrs2) in
         branch_state cs c sp lbl_true lbl_false lenv mem t v
       | RTLabs.St_jumptable (r, table) -> assert false (* TODO *)
+            (get_local_value lenv srcr1)
+            (get_local_value lenv srcr2) in
+        branch_state sfrs graph sp lbl_true lbl_false lenv mem trace v
+      | RTLabs.St_jumptable (r, table) -> assert false (* TODO: jumptable *)
       (*
         let i = match get_local_value lenv r with
 …
         (try
         let next_lbl = List.nth table i in
         State (cs, c, sp, next_lbl, lenv, mem, t)
+        State (sfrs, graph, sp, next_lbl, lenv, mem, trace)
         with
         | Failure "nth" | Invalid_argument "List.nth" ->
 …
       *)
       | RTLabs.St_return rs ->
         let v = get_local_valuel lenv rs in
+      | RTLabs.St_return r ->
+        let v = get_local_value lenv r in
         let mem = Mem.free mem sp in
+        ReturnState (cs, v, mem, t)
+let get_int () =
+  try Val.of_int (int_of_string (read_line ()))
+  with Failure "int_of_string" -> error "Failed to scan an integer."
+let get_float () =
+  try Val.of_float (float_of_string (read_line ()))
+  with Failure "float_of_string" -> error "Failed to scan a float."
+let interpret_external
+    (mem  : memory)
+    (def  : AST.external_function)
+    (args : Val.t list) :
+    memory * Val.t =
+  match def.AST.ef_tag, args with
+    | s, _ when s = Primitive.scan_int ->
+      (mem, get_int ())
+    | "scan_float", _ ->
+      (mem, get_float ())
+    | s, v :: _ when s = Primitive.print_int && Val.is_int v ->
+      Printf.printf "%d" (Val.to_int v) ;
+      (mem, Val.zero)
+    | "print_float", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, Val.zero)
+    | "print_ptr", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, Val.zero)
+    | s, v :: _ when s = Primitive.print_intln && Val.is_int v ->
+      Printf.printf "%d\n" (Val.to_int v) ;
+      (mem, Val.zero)
+    | "print_floatln", v :: _ when Val.is_float v ->
+      Printf.printf "%f" (Val.to_float v) ;
+      (mem, Val.zero)
+    | "print_ptrln", v :: _ when Val.is_pointer v ->
+      let (b, off) = Val.to_pointer v in
+      Printf.printf "block: %s, offset: %s\n"
+        (Val.Block.to_string b) (Val.Offset.to_string off) ;
+      (mem, Val.zero)
+    | s, v :: _ when s = Primitive.alloc ->
+      let (mem, ptr) = Mem.alloc mem (Val.to_int v) in
+      (mem, ptr)
+    | s, v1 :: v2 :: _ when s = Primitive.modulo ->
+      (mem, Val.modulo v1 v2)
+    (* The other cases are either a type error (only integers and pointers
+       may not be differenciated during type checking) or an unknown
+       function. *)
+    | "print_int", _ | "print_intln", _ ->
+      error "Illegal cast from pointer to integer."
+    | "print_ptr", _ | "print_ptrln", _ ->
+      error "Illegal cast from integer to pointer."
+    | ef_tag, _ -> error ("Unknown external function \"" ^ ef_tag ^ "\".")
+        ReturnState (sfrs, v, mem, trace)
+module InterpretExternal = Primitive.Interpret (Mem)
+let interpret_external mem f args = match InterpretExternal.t mem f args with
+  | (mem', InterpretExternal.V v) -> (mem', v)
+  | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr)
 let init_locals
     (locals : Register.t list list)
     (params : Register.t list list)
+    (locals : Register.t list)
+    (params : Register.t list)
     (args   : Val.t list) :
     local_env =
   let f lenv rs = adds rs Val.undef lenv in
+  let f lenv r = Register.Map.add r Val.undef lenv in
   let lenv = List.fold_left f Register.Map.empty locals in
   let f lenv rs v = adds rs v lenv in
+  let f lenv r v = Register.Map.add r v lenv in
   List.fold_left2 f lenv params args
 let state_after_call
     (cs    : stack_frame list)
+    (sfrs  : stack_frame list)
     (f_def : RTLabs.function_def)
     (args  : Val.t list)
     (mem   : memory)
     (t     : CostLabel.t list) :
+    (trace : CostLabel.t list) :
     state =
   match f_def with
     | RTLabs.F_int def ->
       let (mem', sp) = Mem.alloc mem def.RTLabs.f_stacksize in
       State (cs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,
+      State (sfrs, def.RTLabs.f_graph, sp, def.RTLabs.f_entry,
              init_locals def.RTLabs.f_locals def.RTLabs.f_params args,
              mem', t)
+             mem', trace)
     | RTLabs.F_ext def ->
       let (mem', v) = interpret_external mem def args in
       ReturnState (cs, v, mem', t)
+      let (mem', v) = interpret_external mem def.AST.ef_tag args in
+      ReturnState (sfrs, v, mem', trace)
 let state_after_return
     (sf      : stack_frame)
     (cs      : stack_frame list)
+    (sfrs    : stack_frame list)
     (ret_val : Val.t)
     (mem     : memory)
     (t       : CostLabel.t list) :
+    (trace   : CostLabel.t list) :
     state =
   let lenv = adds sf.ret_regs ret_val sf.lenv in
   State (cs, sf.graph, sf.sp, sf.pc, lenv, mem, t)
+  let lenv = Register.Map.add sf.ret_reg ret_val sf.lenv in
+  State (sfrs, sf.graph, sf.sp, sf.pc, lenv, mem, trace)
 let small_step (st : state) : state = match st with
   | State (cs, graph, sp, pc, lenv, mem, t) ->
+  | State (sfrs, graph, sp, pc, lenv, mem, trace) ->
     let stmt = Label.Map.find pc graph in
     interpret_statement cs graph sp lenv mem stmt t
   | CallState (cs, f_def, args, mem, t) ->
     state_after_call cs f_def args mem t
   | ReturnState ([], ret_val, mem, t) ->
+    interpret_statement sfrs graph sp lenv mem stmt trace
+  | CallState (sfrs, f_def, args, mem, trace) ->
+    state_after_call sfrs f_def args mem trace
+  | ReturnState ([], ret_val, mem, trace) ->
     assert false (* End of execution; handled in iter_small_step. *)
   | ReturnState (sf :: cs, ret_val, mem, t) ->
     state_after_return sf cs ret_val mem t
+  | ReturnState (sf :: sfrs, ret_val, mem, trace) ->
+    state_after_return sf sfrs ret_val mem trace
 …
   else IntValue.Int8.zero
+let rec iter_small_step print_result st = match small_step st with
+(*
+  (* <DEBUG> *)
+  | ReturnState ([], v, mem, t) ->
+    Mem.print mem ;
+    Printf.printf "Return: %s\n%!" (Val.to_string v) ;
+    List.rev t
+  | CallState (_, _, _, mem, _)
+  | ReturnState (_, _, mem, _)
+  | State (_, _, _, _, _, mem, _) as st' -> Mem.print mem ; iter_small_step st'
+  (* </DEBUG> *)
+*)
+  | ReturnState ([], v, mem, t) ->
+    let (res, cost_labels) as trace = (compute_result v, List.rev t) in
+    if print_result then
+      Printf.printf "RTLabs: %s\n%!" (IntValue.Int8.to_string res) ;
+    trace
+  | st' -> iter_small_step print_result st'
+let rec iter_small_step debug st =
+  if debug then print_state st ;
+  match small_step st with
+    | ReturnState ([], v, mem, trace) -> (compute_result v, List.rev trace)
+    | st' -> iter_small_step debug st'
 …
 (* Interpret the program only if it has a main. *)
+let interpret print_result p = match p.RTLabs.main with
+  | None -> (IntValue.Int8.zero, [])
+  | Some main ->
+    let mem = init_mem p in
+    let main_def = find_function mem main in
+    let st = CallState ([], main_def, [], mem, []) in
+    iter_small_step print_result st
+let interpret debug p =
+  if debug then Printf.printf "*** RTLabs ***\n\n%!" ;
+  match p.RTLabs.main with
+    | None -> (IntValue.Int8.zero, [])
+    | Some main ->
+      let mem = init_mem p in
+      let main_def = find_function mem main in
+      let st = CallState ([], main_def, [], mem, []) in
+      iter_small_step debug st

Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

-                      r486
+                      r740
+let print_reg_list rl =
+  Printf.sprintf "[%s]" (MiscPottier.string_of_list " ; " Register.print rl)
+let print_reg = Register.print
 let rec print_args args =
+  Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg_list args)
+let print_result rl = print_reg_list rl
+let print_params rl =
+  Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg_list rl)
+let print_locals rl =
+  Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg_list rl)
+let print_memory_q = Memory.string_of_memory_q
+  Printf.sprintf "[%s]" (MiscPottier.string_of_list ", " print_reg args)
+let print_result r = print_reg r
+let print_params r =
+  Printf.sprintf "(%s)" (MiscPottier.string_of_list ", " print_reg r)
+let print_locals r =
+  Printf.sprintf "%s" (MiscPottier.string_of_list ", " print_reg r)
 …
   | AST.Op_floatofint -> "floatofint"
   | AST.Op_floatofintu -> "floatofintu"
   | AST.Op_id -> "mov"
+  | AST.Op_id -> "id"
   | AST.Op_ptrofint -> "ptrofint"
   | AST.Op_intofptr -> "intofptr"
 …
   | RTLabs.St_cost (cost_lbl, lbl) ->
       Printf.sprintf "emit %s --> %s" cost_lbl lbl
   | RTLabs.St_cst (dests, cst, lbl) ->
+  | RTLabs.St_cst (destr, cst, lbl) ->
       Printf.sprintf "imm %s, %s --> %s"
         (print_reg_list dests)
+        (print_reg destr)
         (print_cst cst)
         lbl
   | RTLabs.St_op1 (op1, dests, srcs, lbl) ->
+  | RTLabs.St_op1 (op1, destr, srcr, lbl) ->
       Printf.sprintf "%s %s, %s --> %s"
         (print_op1 op1)
         (print_reg_list dests)
         (print_reg_list srcs)
         lbl
   | RTLabs.St_op2 (op2, dests, srcs1, srcs2, lbl) ->
+        (print_reg destr)
+        (print_reg srcr)
+        lbl
+  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl) ->
       Printf.sprintf "%s %s, %s, %s --> %s"
         (print_op2 op2)
         (print_reg_list dests)
         (print_reg_list srcs1)
         (print_reg_list srcs2)
         lbl
   | RTLabs.St_load (chunk, mode, args, dests, lbl) ->
+        (print_reg destr)
+        (print_reg srcr1)
+        (print_reg srcr2)
+        lbl
+  | RTLabs.St_load (q, mode, args, destr, lbl) ->
       Printf.sprintf "load %s, %s, %s, %s --> %s"
         (print_memory_q chunk)
+        (Memory.string_of_quantity q)
         (print_addressing mode)
         (print_args args)
         (print_reg_list dests)
         lbl
   | RTLabs.St_store (chunk, mode, args, srcs, lbl) ->
+        (print_reg destr)
+        lbl
+  | RTLabs.St_store (q, mode, args, srcr, lbl) ->
       Printf.sprintf "store %s, %s, %s, %s --> %s"
         (print_memory_q chunk)
+        (Memory.string_of_quantity q)
         (print_addressing mode)
         (print_args args)
         (print_reg_list srcs)
+        (print_reg srcr)
         lbl
   | RTLabs.St_call_id (f, args, res, sg, lbl) ->
 …
+        f
         (print_params args)
         (print_reg_list res)
+        (print_reg res)
         (Primitive.print_sig sg)
         lbl
   | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
       Printf.sprintf "call_ptr %s, %s, %s: %s --> %s"
         (print_reg_list f)
         (print_params args)
         (print_reg_list res)
+        (print_reg f)
+        (print_params args)
+        (print_reg res)
         (Primitive.print_sig sg)
         lbl
 …
   | RTLabs.St_tailcall_ptr (f, args, sg) ->
       Printf.sprintf "tailcall_ptr \"%s\", %s: %s"
         (print_reg_list f)
+        (print_reg f)
         (print_params args)
         (Primitive.print_sig sg)
 …
         lbl_true
         lbl_false
   | RTLabs.St_cond1 (op1, srcs, lbl_true, lbl_false) ->
+  | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
       Printf.sprintf "%s %s --> %s, %s"
         (print_op1 op1)
         (print_reg_list srcs)
+        (print_reg srcr)
         lbl_true
         lbl_false
   | RTLabs.St_cond2 (op2, srcs1, srcs2, lbl_true, lbl_false) ->
+  | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
       Printf.sprintf "%s %s, %s --> %s, %s"
         (print_op2 op2)
         (print_reg_list srcs1)
         (print_reg_list srcs2)
+        (print_reg srcr1)
+        (print_reg srcr2)
         lbl_true
         lbl_false
   | RTLabs.St_jumptable (rs, tbl) ->
+  | RTLabs.St_jumptable (r, tbl) ->
       Printf.sprintf "j_tbl %s --> %s"
         (print_reg_list rs)
+        (print_reg r)
         (print_table tbl)
   | RTLabs.St_return rs -> Printf.sprintf "return %s" (print_reg_list rs)
+  | RTLabs.St_return r -> Printf.sprintf "return %s" (print_reg r)
 …
   Printf.sprintf
     "%s\"%s\"%s: %s\n%slocals: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
+    "%s\"%s\"%s: %s\n%slocals: %s\n%spointers: %s\n%sresult: %s\n%sstacksize: %d\n%sentry: %s\n%sexit: %s\n\n%s"
     (n_spaces n)
+    f
 …
     (n_spaces (n+2))
     (print_locals def.RTLabs.f_locals)
+    (n_spaces (n+2))
+    (print_locals def.RTLabs.f_ptrs)
     (n_spaces (n+2))
     (print_result def.RTLabs.f_result)

Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli

r486	r740
2	2	(** This module provides a function to print [RTLabs] programs. *)
3	3
	4	val print_statement : RTLabs.statement -> string
	5
4	6	val print_program : RTLabs.program -> string

Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

-                      r486
+                      r740
     (def, r :: res)
-let rtl_args regs_list = List.flatten regs_list
 let addr_regs regs = match regs with
   | r1 :: r2 :: _ -> (r1, r2)
   | _ -> error "Function pointer is not an address."
+(* Local environments associate one (in case of an integer) or two (in case of a
+   pointer) RTL pseudo-registers to one RTLabs pseudo-register. *)
+type reg_type =
+  | Int of Register.t
+  | Ptr of Register.t * Register.t
+type local_env = reg_type Register.Map.t
+let initialize_local_env runiverse ptrs registers =
+  let f lenv r =
+    let rt =
+      if List.mem r ptrs then Ptr (r, Register.fresh runiverse)
+      else Int r in
+    Register.Map.add r rt lenv in
+  List.fold_left f Register.Map.empty registers
+let filter_and_to_list_local_env lenv registers =
+  let f l r =
+    l @ (match Register.Map.find r lenv with
+      | Int r -> [r]
+      | Ptr (r1, r2) -> [r1 ; r2]) in
+  List.fold_left f [] registers
+let list_of_reg_type = function
+  | Int r -> [r]
+  | Ptr (r1, r2) -> [r1 ; r2]
+let find_and_list r lenv = list_of_reg_type (Register.Map.find r lenv)
+let find_and_list_args args lenv =
+  List.map (fun r -> find_and_list r lenv) args
+let find_and_addr r lenv = match find_and_list r lenv with
+  | r1 :: r2 :: _ -> (r1, r2)
+  | _ -> assert false (* do not use on these arguments *)
+let rtl_args regs_list lenv = List.flatten (find_and_list_args regs_list lenv)
 …
       [RTL.St_stackaddr (r1, r2, start_lbl) ;
        RTL.St_int (tmpr, off, start_lbl) ;
        RTL.St_op2 (I8051.Add, r2, r2, tmpr, start_lbl) ;
+       RTL.St_op2 (I8051.Add, r1, r1, tmpr, start_lbl) ;
        RTL.St_int (tmpr, 0, start_lbl) ;
        RTL.St_op2 (I8051.Addc, r1, r1, tmpr, start_lbl)]
+       RTL.St_op2 (I8051.Addc, r2, r2, tmpr, start_lbl)]
       start_lbl dest_lbl def
 …
     | AST.Op_cast8unsigned, _, _ | AST.Op_cast8signed, _, _
     | AST.Op_cast16unsigned, _, _ | AST.Op_cast16signed, _, _ ->
       def
+      translate_move destrs srcrs start_lbl dest_lbl def
     | AST.Op_negint, [destr], [srcr] ->
 …
     | AST.Op_ptrofint, [destr1 ; destr2], [srcr] ->
       adds_graph
         [RTL.St_move (destr2, srcr, dest_lbl) ;
          RTL.St_int (destr1, 0, start_lbl)]
         start_lbl dest_lbl def
     | AST.Op_intofptr, [destr], [_ ; srcr] ->
+        [RTL.St_move (destr1, srcr, dest_lbl) ;
+         RTL.St_int (destr2, 0, start_lbl)]
+        start_lbl dest_lbl def
+    | AST.Op_intofptr, [destr], [srcr ; _] ->
       add_graph start_lbl (RTL.St_move (destr, srcr, dest_lbl)) def
 …
       error_float ()
+    | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
+    | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]
+    | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] ->
       let (def, tmpr1) = fresh_reg def in
       let (def, tmpr2) = fresh_reg def in
       adds_graph
         [RTL.St_op2 (I8051.Add, tmpr2, srcr12, srcr2, start_lbl) ;
          RTL.St_int (tmpr1, 0, start_lbl) ;
          RTL.St_op2 (I8051.Addc, destr1, tmpr1, srcr11, start_lbl) ;
          RTL.St_move (destr2, tmpr2, start_lbl)]
         start_lbl dest_lbl def
     | AST.Op_subp, [destr], [_ ; srcr1], [_ ; srcr2] ->
+        [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ;
+         RTL.St_int (tmpr2, 0, start_lbl) ;
+         RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ;
+         RTL.St_move (destr1, tmpr1, start_lbl)]
+        start_lbl dest_lbl def
+    | AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] ->
       let (def, tmpr1) = fresh_reg def in
       let (def, tmpr2) = fresh_reg def in
 …
     | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
-      let (def, tmpr1) = fresh_reg def in
-      let (def, tmpr2) = fresh_reg def in
-      let (def, tmpr3) = fresh_reg def in
       adds_graph
         [RTL.St_clear_carry start_lbl ;
          RTL.St_op2 (I8051.Sub, destr2, srcr12, srcr2, start_lbl) ;
          RTL.St_int (destr1, 0, start_lbl) ;
          RTL.St_op2 (I8051.Sub, destr1, srcr11, destr1, start_lbl)]
+         RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ;
+         RTL.St_int (destr2, 0, start_lbl) ;
+         RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)]
         start_lbl dest_lbl def
 …
     | AST.Op_cmpu AST.Cmp_gt, _, _, _ ->
       translate_op2 (AST.Op_cmp AST.Cmp_lt)
+      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
         destrs srcrs2 srcrs1 start_lbl dest_lbl def
 …
       let (def, tmpr2) = fresh_reg def in
       add_translates
         [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr11] [srcr21] ;
          translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr11] [srcr21] ;
          translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr12] [srcr22] ;
+        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ;
+         translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ;
+         translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ;
          translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ;
          translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]]
 …
   | AST.Cst_addrsymbol x ->
+    let (def, rs) = fresh_regs def 2 in
+    let r1 = List.nth rs 0 in
+    let r2 = List.nth rs 1 in
+    let (def, r1) = fresh_reg def in
+    let (def, r2) = fresh_reg def in
     let lbl = fresh_label def in
     let def = add_graph start_lbl (RTL.St_addr (r1, r2, x, lbl)) def in
 …
     | AST.Op_id, _ -> assert false (* wrong number of arguments *)
     | _, _ ->
+    | _, srcrs ->
       let (def, destrs) = fresh_regs def (size_of_op1_ret op1) in
       let lbl = fresh_label def in
 …
   | AST.Op_addp -> 2
   | AST.Op_subp ->
     if n = 1 (* sub between pointer and integer *) then 2
     else (* sub between two pointers *) 1
+    if n = 4 (* sub between two pointers, result is an integer *) then 1
+    else (* sub between a pointer and an integer, result is a pointer *) 2
   | AST.Op_addf
   | AST.Op_subf
 …
     | _, _, _ ->
       let n = List.length srcrs2 in
+      let n = (List.length srcrs1) + (List.length srcrs2) in
       let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in
       let lbl = fresh_label def in
 …
+let translate_load chunk mode args destrs start_lbl dest_lbl def =
+  match chunk, destrs with
+    | Memory.MQ_pointer, [destr1 ; destr2] ->
+let translate_load q mode args destrs start_lbl dest_lbl def =
+  match q, destrs with
+    | Memory.QInt 1, [destr] ->
+      let (def, addr1) = fresh_reg def in
+      let (def, addr2) = fresh_reg def in
+      add_translates
+        [addressing_pointer mode args addr1 addr2 ;
+         adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
+        start_lbl dest_lbl def
+    | Memory.QPtr, [destr1 ; destr2] ->
       let (def, addr1) = fresh_reg def in
       let (def, addr2) = fresh_reg def in
 …
       add_translates
         [addressing_pointer mode args addr1 addr2 ;
          adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl) ;
+         adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ;
                      RTL.St_int (tmpr, 1, start_lbl)] ;
          translate_op2 AST.Op_addp addr addr [tmpr] ;
+         adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl)]]
+        start_lbl dest_lbl def
+    | Memory.MQ_int8signed, [destr]
+    | Memory.MQ_int8unsigned, [destr] ->
+         adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl)]]
+        start_lbl dest_lbl def
+    | _ -> error "Size error in load."
+let translate_store q mode args srcrs start_lbl dest_lbl def =
+  match q, srcrs with
+    | Memory.QInt 1, [srcr] ->
       let (def, addr1) = fresh_reg def in
       let (def, addr2) = fresh_reg def in
       add_translates
         [addressing_pointer mode args addr1 addr2 ;
+         adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
+        start_lbl dest_lbl def
+    | Memory.MQ_int16signed, _ | Memory.MQ_int16unsigned, _
+    | Memory.MQ_int32, _ ->
+      error_int ()
+    | Memory.MQ_float32, _ | Memory.MQ_float64, _ ->
+      error_float ()
+    | _ -> assert false (* wrong number of argument *)
+let translate_store chunk mode args srcrs start_lbl dest_lbl def =
+  match chunk, srcrs with
+    | Memory.MQ_pointer, [srcr1 ; srcr2] ->
+         adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]]
+        start_lbl dest_lbl def
+    | Memory.QPtr, [srcr1 ; srcr2] ->
       let (def, addr1) = fresh_reg def in
       let (def, addr2) = fresh_reg def in
 …
       add_translates
         [addressing_pointer mode args addr1 addr2 ;
          adds_graph [RTL.St_store (addr1, addr2, srcr2, start_lbl) ;
+         adds_graph [RTL.St_store (addr1, addr2, srcr1, start_lbl) ;
                      RTL.St_int (tmpr, 1, start_lbl)] ;
          translate_op2 AST.Op_addp addr addr [tmpr] ;
+         adds_graph [RTL.St_store (addr1, addr2, srcr1, dest_lbl)]]
+        start_lbl dest_lbl def
+    | Memory.MQ_int8signed, [srcr]
+    | Memory.MQ_int8unsigned, [srcr] ->
+      let (def, addr1) = fresh_reg def in
+      let (def, addr2) = fresh_reg def in
+      add_translates
+        [addressing_pointer mode args addr1 addr2 ;
+         adds_graph [RTL.St_store (addr1, addr2, srcr, dest_lbl)]]
+        start_lbl dest_lbl def
+    | Memory.MQ_int16signed, _ | Memory.MQ_int16unsigned, _
+    | Memory.MQ_int32, _ ->
+      error_int ()
+    | Memory.MQ_float32, _ | Memory.MQ_float64, _ ->
+      error_float ()
+    | _ -> assert false (* wrong number of argument *)
+let translate_stmt lbl stmt def = match stmt with
+         adds_graph [RTL.St_store (addr1, addr2, srcr2, dest_lbl)]]
+        start_lbl dest_lbl def
+    | _ -> error "Size error in store."
+let translate_stmt lenv lbl stmt def = match stmt with
   | RTLabs.St_skip lbl' ->
 …
     add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def
+  | RTLabs.St_cst (destrs, cst, lbl') ->
+    translate_cst cst destrs lbl lbl' def
+  | RTLabs.St_op1 (op1, destrs, srcrs, lbl') ->
+    translate_op1 op1 destrs srcrs lbl lbl' def
+  | RTLabs.St_op2 (op2, destrs, srcrs1, srcrs2, lbl') ->
+    translate_op2 op2 destrs srcrs1 srcrs2 lbl lbl' def
+  | RTLabs.St_load (chunk, mode, args, destrs, lbl') ->
+    translate_load chunk mode args destrs lbl lbl' def
+  | RTLabs.St_store (chunk, mode, args, srcrs, lbl') ->
+    translate_store chunk mode args srcrs lbl lbl' def
+  | RTLabs.St_call_id (f, args, retrs, _, lbl') ->
+    add_graph lbl (RTL.St_call_id (f, rtl_args args, retrs, lbl')) def
+  | RTLabs.St_call_ptr (f, args, retrs, _, lbl') ->
+    let (f1, f2) = addr_regs f in
+  | RTLabs.St_cst (destr, cst, lbl') ->
+    translate_cst cst (find_and_list destr lenv) lbl lbl' def
+  | RTLabs.St_op1 (op1, destr, srcr, lbl') ->
+    translate_op1 op1 (find_and_list destr lenv) (find_and_list srcr lenv)
+      lbl lbl' def
+  | RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') ->
+    translate_op2 op2 (find_and_list destr lenv)
+      (find_and_list srcr1 lenv) (find_and_list srcr2 lenv) lbl lbl' def
+  | RTLabs.St_load (q, mode, args, destr, lbl') ->
+    translate_load q mode (find_and_list_args args lenv)
+      (find_and_list destr lenv) lbl lbl' def
+  | RTLabs.St_store (q, mode, args, srcr, lbl') ->
+    translate_store q mode (find_and_list_args args lenv)
+      (find_and_list srcr lenv) lbl lbl' def
+  | RTLabs.St_call_id (f, args, retr, _, lbl') ->
+    add_graph lbl (RTL.St_call_id (f, rtl_args args lenv,
+                                   find_and_list retr lenv, lbl')) def
+  | RTLabs.St_call_ptr (f, args, retr, _, lbl') ->
+    let (f1, f2) = find_and_addr f lenv in
     add_graph lbl
+      (RTL.St_call_ptr (f1, f2, rtl_args args, retrs, lbl')) def
+      (RTL.St_call_ptr
+         (f1, f2, rtl_args args lenv, find_and_list retr lenv, lbl')) def
   | RTLabs.St_tailcall_id (f, args, _) ->
     add_graph lbl (RTL.St_tailcall_id (f, rtl_args args)) def
+    add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def
   | RTLabs.St_tailcall_ptr (f, args, _) ->
     let (f1, f2) = addr_regs f in
     add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args)) def
+    let (f1, f2) = find_and_addr f lenv in
+    add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def
   | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
     translate_condcst cst lbl lbl_true lbl_false def
+  | RTLabs.St_cond1 (op1, srcrs, lbl_true, lbl_false) ->
+    translate_cond1 op1 srcrs lbl lbl_true lbl_false def
+  | RTLabs.St_cond2 (op2, srcrs1, srcrs2, lbl_true, lbl_false) ->
+    translate_cond2 op2 srcrs1 srcrs2 lbl lbl_true lbl_false def
+  | RTLabs.St_cond1 (op1, srcr, lbl_true, lbl_false) ->
+    translate_cond1 op1 (find_and_list srcr lenv)
+      lbl lbl_true lbl_false def
+  | RTLabs.St_cond2 (op2, srcr1, srcr2, lbl_true, lbl_false) ->
+    translate_cond2 op2 (find_and_list srcr1 lenv)
+      (find_and_list srcr2 lenv) lbl lbl_true lbl_false def
   | RTLabs.St_jumptable _ ->
     error "Jump tables not supported yet."
   | RTLabs.St_return regs ->
     add_graph lbl (RTL.St_return regs) def
+  | RTLabs.St_return r ->
+    add_graph lbl (RTL.St_return (find_and_list r lenv)) def
 let translate_internal def =
+  let set_of_list_list l =
+    let l = List.flatten l in
+    List.fold_left (fun res x -> Register.Set.add x res) Register.Set.empty l
+  in
+  let runiverse = def.RTLabs.f_runiverse in
+  let lenv =
+    initialize_local_env runiverse def.RTLabs.f_ptrs
+      (def.RTLabs.f_params @ def.RTLabs.f_locals) in
+  let result = find_and_list def.RTLabs.f_result lenv in
+  let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in
+  let params = filter_and_to_list_local_env lenv def.RTLabs.f_params in
+  let locals = filter_and_to_list_local_env lenv def.RTLabs.f_locals in
+  let locals = set_of_list locals in
   let res =
     { RTL.f_luniverse = def.RTLabs.f_luniverse ;
       RTL.f_runiverse = def.RTLabs.f_runiverse ;
+      RTL.f_runiverse = runiverse ;
       RTL.f_sig       = def.RTLabs.f_sig ;
       RTL.f_result    = def.RTLabs.f_result ;
       RTL.f_params    = List.flatten def.RTLabs.f_params ;
       RTL.f_locals    = set_of_list_list def.RTLabs.f_locals ;
+      RTL.f_result    = result ;
+      RTL.f_params    = params ;
+      RTL.f_locals    = locals ;
       RTL.f_stacksize = def.RTLabs.f_stacksize ;
       RTL.f_graph     = Label.Map.empty ;
       RTL.f_entry     = def.RTLabs.f_entry ;
       RTL.f_exit      = def.RTLabs.f_exit } in
   Label.Map.fold translate_stmt def.RTLabs.f_graph res
+  Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res

Deliverables/D2.2/8051/src/acc.ml

-                      r640
+                      r740
     | None -> (false, filename)
     | Some filename' -> (true, filename') in
+  let save = Languages.save exact_output output_filename in
+  let save ?(suffix="") ast =
+    Languages.save exact_output output_filename suffix ast
+  in
   let target_asts =
     (** If debugging is enabled, the compilation function returns all
 …
   in
   let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
+    save final_ast;
+    (if Options.annotation_requested () then
+       let (annotated_input_ast, cost_id, cost_incr) =
+         Languages.annotate input_ast final_ast in
+       save annotated_input_ast;
+       Languages.save_cost output_filename cost_id cost_incr);
+    (if Options.is_debug_enabled () then
+      List.iter save intermediate_asts);
+    if Options.interpretation_requested () || Options.is_debug_enabled () then
+      begin
+        let asts = input_ast :: target_asts in
+        let print_result = Options.is_print_result_enabled () in
+        let label_traces = List.map (Languages.interpret print_result) asts in
+        Printf.eprintf "Checking execution traces...%!";
+        Checker.same_traces (List.combine asts label_traces);
+        Printf.eprintf "OK.\n%!";
+      end
+  save final_ast;
+  if Options.annotation_requested () then
+    begin
+      let (annotated_input_ast, cost_id, cost_incr) =
+        Languages.annotate input_ast final_ast in (
+          save ~suffix:"-annotated" annotated_input_ast;
+          Languages.save_cost output_filename cost_id cost_incr);
+    end;
+  if Options.is_debug_enabled () then
+    List.iter save intermediate_asts;
+  if Options.interpretation_requested () || Options.is_debug_enabled () then
+    begin
+      let asts = input_ast :: target_asts in
+      let label_traces = List.map (Languages.interpret false) asts in
+      Printf.eprintf "Checking execution traces...%!";
+      Checker.same_traces (List.combine asts label_traces);
+      Printf.eprintf "OK.\n%!";
+    end
 let _ =

Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml

-                      r619
+                      r740
 let translate p =
+  (* TODO: restore below *)
+(*
   let (p, unop_assoc, binop_assoc) = Runtime.add p in
   let p = ClightCasts.simplify p in
 …
   (* TODO: do the translation *)
+  p
+*)
+  ClightCasts.simplify p

Deliverables/D2.2/8051/src/clight/clightCasts.ml

-                      r624
+                      r740
     Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char]
+    will be transformed into [x + y]. *)
+    will be transformed into [x + y]. Primitive operations are thus supposed to
+    be polymorphic, but working only on homogene types. *)
 let f_ctype ctype _ = ctype
+(*
 let f_expr = ClightFold.expr_fill_subs
 …
                   (Clight.Expr (_,
                                 Clight.Tint (Clight.I8, signedness2)) as e1)),
                _)),
+               _)),sub_ctypes_res sub_exprs_res
          _) :: _ when signedness1 = signedness2 ->
       Clight.Ebinop (binop,
 …
                      e1)
     | _ -> ClightFold.expr_descr_fill_subs e sub_ctypes_res sub_exprs_res
+*)
+let f_statement = ClightFold.statement_fill_subs
+let simplify_exp ctype_opt e = e (* TODO *)
+let f_expr e _ _ = e
+let f_expr_descr e _ _ =  e
+let f_statement stmt _ sub_stmts_res =
+  let sub_exprs = match stmt with
+    | _ -> assert false in
+  ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res
 let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement
 …
   (id, fundef')
+let simplify p =
+let simplify p = p
+(* (* TODO: below *)
   { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct }
+*)

Deliverables/D2.2/8051/src/clight/clightCasts.mli

-                      r619
+                      r740
     Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char]
+    will be transformed into [x + y]. *)
+    will be transformed into [x + y]. Primitive operations are thus supposed to
+    be polymorphic, but working only on homogene types. *)
 val simplify : Clight.program -> Clight.program

Deliverables/D2.2/8051/src/clight/clightFold.mli

-                      r619
+                      r740
 val ctype : (Clight.ctype -> 'a list -> 'a) -> Clight.ctype -> 'a
+val expr : (Clight.expr_descr -> 'a list -> 'b list -> 'c) ->
+           (Clight.ctype -> 'a list -> 'a) ->
+           (Clight.expr -> 'c list -> 'a list -> 'b) ->
+           Clight.expr ->
+           'b
+val expr_fill_subs :
+  Clight.expr -> Clight.ctype list -> Clight.expr_descr list ->
+  Clight.expr
+val expr_descr : (Clight.ctype -> 'a list -> 'a) ->
+                 (Clight.expr -> 'b list -> 'a list -> 'c) ->
+                 (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
+                 Clight.expr_descr ->
+                 'b
+val expr :
+  (Clight.ctype -> 'a list -> 'a) ->
+  (Clight.expr -> 'a list -> 'b list -> 'c) ->
+  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
+  Clight.expr ->
+  'c
+(*
+(* In [statement_left f_expr f_stmt stmt], [f_stmt]'s second argument is the
+   list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and
+   [f_stmt]'s third argument is the list of [statement_left]'s results
+   on [stmt]'s sub-statements. The results are computed from left to right
+   following their appearance order in the [Cminor.statement] type. *)
+val expr_descr_fill_subs :
+  Clight.expr_descr -> Clight.ctype list -> Clight.expr list ->
+  Clight.expr_descr
+val statement_left : (Cminor.expression -> 'a list -> 'a) ->
+                     (Cminor.statement -> 'a list -> 'b list -> 'b) ->
+                     Cminor.statement ->
+                     'b
+*)
+val expr_descr :
+  (Clight.ctype -> 'a list -> 'a) ->
+  (Clight.expr -> 'a list -> 'b list -> 'c) ->
+  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
+  Clight.expr_descr ->
+  'b
+val statement_fill_subs :
+  Clight.statement -> Clight.expr list -> Clight.statement list ->
+  Clight.statement
+val statement :
+  (Clight.ctype -> 'a list -> 'a) ->
+  (Clight.expr -> 'a list -> 'b list -> 'c) ->
+  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
+  (Clight.statement -> 'c list -> 'd list -> 'd) ->
+  Clight.statement ->
+  'd

Deliverables/D2.2/8051/src/clight/clightInterpret.ml

-                      r630
+                      r740
 module Mem = Driver.ClightMemory
 module Value = Driver.ClightMemory.Value
+module Valtbl = Hashtbl.Make(Value)
+module LocalEnv = Map.Make(String)
+type localEnv = Value.address LocalEnv.t
+type memory = Clight.fundef Mem.memory
 open Clight
 open AST
+let warning msg = print_string ("Warning: "^msg^" (clightInterpret.ml)\n")
+type localEnv = (ident,Value.t) Hashtbl.t
+let error_prefix = "Clight interpret"
+let error s = Error.global_error error_prefix s
+let warning s = Error.warning error_prefix s
+let error_float () = error "float not supported."
+(* Helpers *)
+let value_of_address = List.hd
+let address_of_value v = [v]
+(* State of execution *)
 type continuation =
 …
   | Kfor3 of expr*statement*statement*continuation
   | Kswitch of continuation
   | Kcall of (Value.t*ctype) option*cfunction*localEnv*continuation
+  | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
 type state =
+  | State of cfunction*statement*continuation*localEnv*(fundef Mem.memory)
+  | Callstate of fundef*Value.t list*continuation*(fundef Mem.memory)
+  | Returnstate of Value.t*continuation*(fundef Mem.memory)
+(* ctype functions *)
+let rec sizeof = function
+  | Tvoid               -> 0
+  | Tint (I8,_)         -> 1
+  | Tint (I16,_)        -> 2
+  | Tint (I32,_)        -> 4
+  | Tfloat _            -> assert false (* Not supported *)
+  | Tpointer _          -> Mem.ptr_size
+  | Tarray (t,s)        -> s*(sizeof t)
+  | Tfunction (_,_)     -> assert false (* Not supported *)
+  | Tstruct (_,lst)     ->
+      List.fold_left
+        (fun n (_,ty) -> (fun a b -> a+b) n (sizeof ty)) 0 lst
+  | Tunion (_,lst)      ->
+      List.fold_left
+        (fun n (_,ty)   ->
+           let sz = (sizeof ty) in (if n>sz then n else sz)
+        ) 0 lst
+  | Tcomp_ptr _         -> Mem.ptr_size
+let rec mq_of_ty = function
+  | Tvoid               -> assert false
+  | Tint (I8,Signed)    -> Memory.MQ_int8signed
+  | Tint (I8,Unsigned)  -> Memory.MQ_int8unsigned
+  | Tint (I16,Signed)   -> Memory.MQ_int16signed
+  | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned
+  (*FIXME MQ_int32 : signed or unsigned ?*)
+  | Tint (I32,Signed)   -> Memory.MQ_int32
+  | Tint (I32,Unsigned) -> Memory.MQ_int32
+  | Tfloat _            -> assert false (* Not supported *)
+  | Tpointer _          -> Mem.mq_of_ptr
+  | Tarray (c,s)        -> Mem.mq_of_ptr
+  | Tfunction (_,_)     -> assert false (* Not supported *)
+  | Tstruct (_,_)       -> Mem.mq_of_ptr
+  | Tunion (_,_)        -> Mem.mq_of_ptr
+  | Tcomp_ptr _         -> Mem.mq_of_ptr
+(* Pretty printing for Clight states *)
+let string_s = function
+  | Sskip                               -> "skip"
+  | Sassign (Expr (Evar id,_),_)        -> "assign "^id
+  | Sassign (_,_)                       -> "assign"
+  | Scall (_,_,_)                       -> "call"
+  | Ssequence (_,_)                     -> "seq"
+  | Sifthenelse (_,_,_)                 -> "ifthenelse"
+  | Swhile (_,_)                        -> "while"
+  | Sdowhile (_,_)                      -> "dowhile"
+  | Sfor (_,_,_,_)                      -> "for"
+  | Sbreak                              -> "break"
+  | Scontinue                           -> "continue"
+  | Sreturn _                           -> "return"
+  | Sswitch (_,_)                       -> "switch"
+  | Slabel (_,_)                        -> "label"
+  | Sgoto _                             -> "goto"
+  | Scost (_,_)                         -> "cost"
+let string_f = function
+  | Internal _          -> "func"
+  | External (id,_,_)   -> id
+let string_c = function
+  | Kstop               -> "stop"
+  | Kseq (_,_)          -> "seq"
+  | Kwhile (_,_,_)      -> "while"
+  | Kdowhile (_,_,_)    -> "dowhile"
+  | Kfor2 (_,_,_,_)     -> "for2"
+  | Kfor3 (_,_,_,_)     -> "for3"
+  | Kswitch _           -> "switch"
+  | Kcall (_,_,_,_)     -> "call"
+let string_of_state = function
+  | State (_,s,c,_,_) -> "Regular("^(string_s s)^","^(string_c c)^")"
+  | Callstate (f,_,c,_) -> "Call("^(string_f f)^","^(string_c c)^")"
+  | Returnstate (v,c,_) ->
+      "Return("^(Value.to_string v)^","^(string_c c)^")"
+(* Global and local environment management *)
+let find_funct_id g id =
+  try Valtbl.find (snd g) (Hashtbl.find (fst g) id)
+  with Not_found -> assert false
+let find_funct g v =
+  try Valtbl.find (snd g) (fst v)
+  with Not_found -> assert false
+let find_symbol globalenv localenv id =
+  try Hashtbl.find localenv id
+  with Not_found -> (
+    try Hashtbl.find (fst globalenv) id
+    with Not_found ->
+     Printf.eprintf "Error: cannot find symbol %s\n" id;
+      assert false
+  )
+  | State of cfunction*statement*continuation*localEnv*memory
+  | Callstate of fundef*Value.t list*continuation*memory
+  | Returnstate of Value.t*continuation*memory
+let string_of_unop = function
+  | Onotbool -> "!"
+  | Onotint -> "~"
+  | Oneg -> "-"
+let string_of_binop = function
+  | Oadd -> "+"
+  | Osub -> "-"
+  | Omul -> "*"
+  | Odiv -> "/"
+  | Omod -> "%"
+  | Oand -> "&"
+  | Oor  -> "|"
+  | Oxor -> "^"
+  | Oshl -> "<<"
+  | Oshr -> ">>"
+  | Oeq -> "=="
+  | One -> "!="
+  | Olt -> "<"
+  | Ogt -> ">"
+  | Ole -> "<="
+  | Oge -> ">="
+let string_of_signedness = function
+  | Signed -> "signed"
+  | Unsigned -> "unsigned"
+let string_of_sized_int = function
+  | I8 -> "char"
+  | I16 -> "short"
+  | I32 -> "int"
+let rec string_of_ctype = function
+  | Tvoid -> "void"
+  | Tint (size, sign) ->
+    (string_of_signedness sign) ^ " " ^ (string_of_sized_int size)
+  | Tfloat _ -> error_float ()
+  | Tpointer ty -> (string_of_ctype ty) ^ "*"
+  | Tarray (ty, _) -> (string_of_ctype ty) ^ "[]"
+  | Tfunction _ -> assert false (* do not cast to a function type *)
+  | Tstruct (id, _)
+  | Tunion (id, _) -> id
+  | Tcomp_ptr id -> id ^ "*"
+let rec string_of_expr (Expr (e, _)) = string_of_expr_descr e
+and string_of_expr_descr = function
+  | Econst_int i -> string_of_int i
+  | Econst_float _ -> error_float ()
+  | Evar x -> x
+  | Ederef e -> "*(" ^ (string_of_expr e) ^ ")"
+  | Eaddrof e -> "&(" ^ (string_of_expr e) ^ ")"
+  | Eunop (unop, e) -> (string_of_unop unop) ^ "(" ^ (string_of_expr e) ^ ")"
+  | Ebinop (binop, e1, e2) ->
+    "(" ^ (string_of_expr e1) ^ ")" ^ (string_of_binop binop) ^
+    "(" ^ (string_of_expr e2) ^ ")"
+  | Ecast (ty, e) ->
+    "(" ^ (string_of_ctype ty) ^ ") (" ^ (string_of_expr e) ^ ")"
+  | Econdition (e1, e2, e3) ->
+    "(" ^ (string_of_expr e1) ^ ") ? (" ^ (string_of_expr e2) ^
+    ") : (" ^ (string_of_expr e3) ^ ")"
+  | Eandbool (e1, e2) ->
+    "(" ^ (string_of_expr e1) ^ ") && (" ^ (string_of_expr e2) ^ ")"
+  | Eorbool (e1, e2) ->
+    "(" ^ (string_of_expr e1) ^ ") || (" ^ (string_of_expr e2) ^ ")"
+  | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
+  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
+  | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
+  | Ecall (f, arg, e) ->
+    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
+let string_of_args args =
+  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
+let rec string_of_statement = function
+  | Sskip -> "skip"
+  | Sassign (e1, e2) -> (string_of_expr e1) ^ " = " ^ (string_of_expr e2)
+  | Scall (None, f, args) -> (string_of_expr f) ^ (string_of_args args)
+  | Scall (Some e, f, args) ->
+    (string_of_expr e) ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
+  | Ssequence _ -> "sequence"
+  | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
+  | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")"
+  | Sdowhile _ -> "dowhile"
+  | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)"
+  | Sbreak -> "break"
+  | Scontinue -> "continue"
+  | Sreturn None -> "return"
+  | Sreturn (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
+  | Sswitch (e, _) -> "switch (" ^ (string_of_expr e) ^ ")"
+  | Slabel (lbl, _) -> "label " ^ lbl
+  | Sgoto lbl -> "goto " ^ lbl
+  | Scost (lbl, _) -> "cost " ^ lbl
+let string_of_local_env lenv =
+  let f x addr s =
+    s ^ x ^ " = " ^ (Value.to_string (value_of_address addr)) ^ "  " in
+  LocalEnv.fold f lenv ""
+let print_state = function
+  | State (_, stmt, _, lenv, mem) ->
+    Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
+      (string_of_local_env lenv)
+      (Mem.to_string mem)
+      (string_of_statement stmt)
+  | Callstate (_, args, _, mem) ->
+    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
+      (Mem.to_string mem)
+      (MiscPottier.string_of_list " " Value.to_string args)
+  | Returnstate (v, _, mem) ->
+    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
+      (Mem.to_string mem)
+      (Value.to_string v)
 (* Continuations and labels *)
 let rec call_cont = function
+  | Kseq (_,k)          -> call_cont k
+  | Kwhile (_,_,k)      -> call_cont k
+  | Kdowhile (_,_,k)    -> call_cont k
+  | Kfor2 (_,_,_,k)     -> call_cont k
+  | Kfor3 (_,_,_,k)     -> call_cont k
+  | Kswitch k           -> call_cont k
+  | k                   -> k
+let is_call_cont = function
+  | Kstop | Kcall (_,_,_,_) -> true
+  | _ -> false
+  | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
+  | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
+  | k -> k
 let rec seq_of_labeled_statement = function
   | LSdefault s -> s
   | LScase (c,s,sl') -> Ssequence (s,(seq_of_labeled_statement sl'))
+let rec find_label1 lbl s k = match s with
+   | Ssequence (s1,s2) ->
+      (match find_label1 lbl s1 (Kseq (s2,k)) with
+      | Some sk -> Some sk
+      | None -> find_label1 lbl s2 k
+      )
+  | Sifthenelse (a,s1,s2) ->
+      (match find_label1 lbl s1 k with
+      | Some sk -> Some sk
+      | None -> find_label1 lbl s2 k
+      )
+  | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k))
+  | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k))
+  | Sfor (a1,a2,a3,s1) ->
+      (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
+      | Some sk -> Some sk
+      | None ->
+          (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
+          | Some sk -> Some sk
+          | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
+          ))
+  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
+  | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label1 lbl s' k
+  | Scost (_,s') -> find_label1 lbl s' k
+  | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak
+  | Scontinue | Sreturn _ | Sgoto _ -> None
+and find_label_ls lbl sl k =  match sl with
+  | LSdefault s -> find_label1 lbl s k
+  | LScase (_,s,sl') ->
+      (match find_label1 lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
+      | Some sk -> Some sk
+      | None -> find_label_ls lbl sl' k
+      )
+let find_label lbl s k = match find_label1 lbl s k with
+  | Some res -> res
+  | _ -> assert false (* should be impossible *)
 let rec select_switch i = function
 …
   | LScase (_,_,sl') -> select_switch i sl'
+let rec find_label lbl s k = match s with
+   | Ssequence (s1,s2) ->
+      (match find_label lbl s1 (Kseq (s2,k)) with
+      | Some sk -> Some sk
+      | None -> find_label lbl s2 k
+      )
+  | Sifthenelse (a,s1,s2) ->
+      (match find_label lbl s1 k with
+      | Some sk -> Some sk
+      | None -> find_label lbl s2 k
+      )
+  | Swhile (a,s1) -> find_label lbl s1 (Kwhile(a,s1,k))
+  | Sdowhile (a,s1) -> find_label lbl s1 (Kdowhile(a,s1,k))
+  | Sfor (a1,a2,a3,s1) ->
+      (match find_label lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
+      | Some sk -> Some sk
+      | None ->
+          (match find_label lbl s1 (Kfor2(a2,a3,s1,k)) with
+          | Some sk -> Some sk
+          | None -> find_label lbl a3 (Kfor3(a2,a3,s1,k))
+          ))
+  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
+  | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label lbl s' k
+  | Scost (_,s') -> find_label lbl s' k
+  | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak
+  | Scontinue | Sreturn _ | Sgoto _ -> None
+and find_label_ls lbl sl k =  match sl with
+  | LSdefault s -> find_label lbl s k
+  | LScase (_,s,sl') ->
+      (match find_label lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
+      | Some sk -> Some sk
+      | None -> find_label_ls lbl sl' k
+      )
+(* ctype functions *)
+let rec sizeof = function
+  | Tint (I8, _)  -> 1
+  | Tint (I16, _) -> 2
+  | Tint (I32, _) -> 4
+  | Tfloat _ -> error_float ()
+  | Tcomp_ptr _ -> Mem.ptr_size
+  | Tpointer _ -> Mem.ptr_size
+  | Tarray (ty, n) -> n * (sizeof ty)
+  | Tstruct (_, fields) ->
+    let sizes = List.map sizeof (List.map snd fields) in
+    snd (Mem.align 0 sizes)
+  | Tunion (_, fields) ->
+    MiscPottier.max_list (List.map sizeof (List.map snd fields))
+  | _ -> assert false (* do not use on these arguments *)
+let size_of_ctype = function
+  | Tint (I8, _)  -> 1
+  | Tint (I16, _) -> 2
+  | Tint (I32, _) -> 4
+  | Tfloat _ -> error_float ()
+  | Tcomp_ptr _
+  | Tpointer _
+  | Tarray _
+  | Tstruct _
+  | Tunion _ -> Mem.ptr_size
+  | _ -> assert false (* do not use on these arguments *)
+let is_function_type = function
+  | Tfunction _ -> true
+  | _ -> false
+let is_array_type = function
+  | Tarray _ -> true
+  | _ -> false
+let is_complex_type = function
+  | Tstruct _ | Tunion _ -> true
+  | _ -> false
+let is_big_type t = (is_array_type t) || (is_complex_type t)
+let dest_type = function
+  | Tpointer ty | Tarray (ty, _) -> ty
+  | _ -> assert false (* do not use on these arguments *)
+(* Global and local environment management *)
+let find_local x lenv =
+  if LocalEnv.mem x lenv then LocalEnv.find x lenv
+  else error ("Unknown local variable " ^ x ^ ".")
+let find_global x mem =
+  if Mem.mem_global mem x then Mem.find_global mem x
+  else error ("Unknown global variable " ^ x ^ ".")
+let find_symbol lenv mem x =
+  if LocalEnv.mem x lenv then LocalEnv.find x lenv
+  else
+    if Mem.mem_global mem x then Mem.find_global mem x
+    else error ("Unknown variable " ^ x ^ ".")
+let find_fundef f mem =
+  let addr = Mem.find_global mem f in
+  Mem.find_fun_def mem addr
 (* Interpret *)
+let is_int_type = function
+  | Tint (_,_)    -> true
+  | _ -> false
+let is_float_type = function
+  | Tfloat _  -> true
+  | _ -> false
+let is_pointer_type = function
+  | Tpointer _ | Tarray (_,_) | Tstruct (_,_)
+  | Tunion (_,_) | Tcomp_ptr _ -> true
+  | _ -> false
+let eval_cast = function
+  (* no cast *)
+  | (e,a,b) when a=b                            -> e
+let int_of_intsize = function
+  | I8 -> 8
+  | I16 -> 16
+  | I32 -> 32
+let choose_cast signedness n m v =
+  let f = match signedness with
+    | Signed -> Value.sign_ext
+    | Unsigned -> Value.zero_ext in
+  f v n m
+let eval_cast = function
   (* Cast Integer *)
+  | (v,_,Tint(I8,Signed))                       -> Value.cast8signed v
+  | (v,_,Tint(I8,Unsigned))                     -> Value.cast8unsigned v
+  | (v,_,Tint(I16,Signed))                      -> Value.cast16signed v
+  | (v,_,Tint(I16,Unsigned))                    -> Value.cast16unsigned v
+  | (v,_,Tint(I32,Signed)) when Value.is_int v  -> v
+  | (v,_,Tint(I32,Unsigned)) when Value.is_int v-> v (*FIXME*)
+  (* Cast float*)
+  | (v,_,Tfloat _)                              -> assert false(*Not supported*)
+  (* Cast pointeur *)
+  | (v,Tarray(_,_),Tpointer _)                  -> v
+  | (v,Tpointer _,Tarray(_,_))                  -> v
+  | (v,Tpointer _,Tpointer _)                   -> v
+  | (v,Tarray (_,_),Tarray(_,_))                -> v
+  | (v,Tstruct(a,b),Tpointer (Tstruct(c,d))) when a=c && b=d -> v (*FIXME is it correct ?*)
+  | (v,Tpointer (Tstruct(a,b)),Tstruct(c,d)) when a=c && b=d -> v (*FIXME is it correct ?*)
+  | (v,Tunion(a,b),Tpointer (Tunion(c,d))) when a=c && b=d -> v (*FIXME is it correct ?*)
+  | (v,Tpointer (Tunion(a,b)),Tunion(c,d)) when a=c && b=d -> v (*FIXME is it correct ?*)
+  (* error *)
+  | (e,_,_)                                     ->
+      warning "eval_cast";e (*Value.undef*)
+let eval_unop (v,t) = function
+  | Onotbool when is_int_type t -> Value.notbool v
+  | Onotint when is_int_type t  -> Value.notint v
+  | Oneg when is_int_type t     -> Value.negint v
+  | Oneg when is_float_type t   -> assert false (*Not supported*)
+  | _                           -> assert false (*Type error*)
+let get_subtype = function
+  | Tarray(t,_) -> t
+  | Tpointer t -> t
+  | _ -> assert false (*Misuse of get_subtype*)
+let eval_add = function
+  (*Integer*)
+  | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 ->
+      let v = Value.add v1 v2 in
+        (match t1 with
+           | Tint(I8,Signed)    -> Value.cast8signed v
+           | Tint(I8,Unsigned)  -> Value.cast8unsigned v
+           | Tint(I16,Signed)   -> Value.cast16signed v
+           | Tint(I16,Unsigned) -> Value.cast16unsigned v
+           | Tint(I32,Signed)   -> v
+           | Tint(I32,Unsigned) -> v (*FIXME*)
+           | _                  -> assert false (*Prevented by is_int_type*))
+  (*Float*)
+  | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 ->
+      assert false (*Not supported*)
+  (*Pointer*)
+  | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
+      Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
+  | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 ->
+      Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
+  (*Error*)
+  | _ -> assert false (*Type error*)
+let eval_sub = function
+  (*Integer*)
+  | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 ->
+      let v = Value.sub v1 v2 in
+        (match t1 with
+           | Tint(I8,Signed)    -> Value.cast8signed v
+           | Tint(I8,Unsigned)  -> Value.cast8unsigned v
+           | Tint(I16,Signed)   -> Value.cast16signed v
+           | Tint(I16,Unsigned) -> Value.cast16unsigned v
+           | Tint(I32,Signed)   -> v
+           | Tint(I32,Unsigned) -> v (*FIXME*)
+           | _                  -> assert false (*Prevented by is_int_type*))
+  (*Float*)
+  | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 ->
+      assert false (*Not supported*)
+  (*Pointer*)
+  | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
+      Value.sub v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
+  (*Error*)
+  | _ -> assert false (*Type error*)
+let eval_mul = function
+  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 ->
+      let v = Value.mul v1 v2 in
+        (match t1 with
+           | Tint(I8,Signed)    -> Value.cast8signed v
+           | Tint(I8,Unsigned)  -> Value.cast8unsigned v
+           | Tint(I16,Signed)   -> Value.cast16signed v
+           | Tint(I16,Unsigned) -> Value.cast16unsigned v
+           | Tint(I32,Signed)   -> v
+           | Tint(I32,Unsigned) -> v (*FIXME*)
+           | _                  -> assert false (*Prevented by is_int_type*))
+  | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 ->
+      assert false (*Not supported*)
+  | _ -> assert false (*Type error*)
+let eval_mod = function
+  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 ->
+      Value.modulo v1 v2
+  | _ -> assert false (*Type error*)
+let eval_div = function
+  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.div v1 v2
+  | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 ->
+      assert false (*Not supported*)
+  | _ -> assert false (*Type error*)
+let eval_and = function
+  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.and_op v1 v2
+  | _ -> assert false (*Type error*)
+let eval_or = function
+  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.or_op v1 v2
+  | _ -> assert false (*Type error*)
+let eval_xor = function
+  | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.xor v1 v2
+  | _ -> assert false (*Type error*)
+let eval_shl = function
+  | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shl v1 v2
+  | _ -> assert false (*Type error*)
+let eval_shr = function
+  | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shr v1 v2
+  | _ -> assert false (*Type error*)
+let eval_eq = function
+  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_eq v1 v2
+  | _ -> assert false (*Type error*)
+let eval_ne = function
+  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ne v1 v2
+  | _ -> assert false (*Type error*)
+let eval_lt = function
+  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_lt v1 v2
+  | _ -> assert false (*Type error*)
+let eval_gt = function
+  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_gt v1 v2
+  | _ -> assert false (*Type error*)
+let eval_le = function
+  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_le v1 v2
+  | _ -> assert false (*Type error*)
+let eval_ge = function
+  | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ge v1 v2
+  | _ -> assert false (*Type error*)
+let eval_binop e1 e2 = function
+  | Oadd -> eval_add (e1,e2)
+  | Osub -> eval_sub (e1,e2)
+  | Omul -> eval_mul (e1,e2)
+  | Odiv -> eval_div (e1,e2)
+  | Omod -> eval_mod (e1,e2)
+  | Oand -> eval_and (e1,e2)
+  | Oor -> eval_or (e1,e2)
+  | Oxor-> eval_xor (e1,e2)
+  | Oshl-> eval_shl (e1,e2)
+  | Oshr-> eval_shr (e1,e2)
+  | Oeq -> eval_eq (e1,e2)
+  | One -> eval_ne (e1,e2)
+  | Olt -> eval_lt (e1,e2)
+  | Ogt -> eval_gt (e1,e2)
+  | Ole -> eval_le (e1,e2)
+  | Oge -> eval_ge (e1,e2)
+let rec get_offset_struct v id = function
+  | [] -> assert false (*Wrong id*)
+  | (fi,_)::_ when fi=id -> v
+  | (_,ty)::ll -> get_offset_struct
+                    (Value.add v (Value.of_int (sizeof ty))) id ll
+let is_true (v,_) = Value.is_true v
+let is_false (v,_) = Value.is_false v
+let rec eval_expr globalenv localenv m e = let Expr (ee,tt) = e in
+  | (v,Tint(isize,signedness),Tint(isize',_)) ->
+    choose_cast signedness (int_of_intsize isize) (int_of_intsize isize') v
+  | (v,_,_) -> v
+let eval_unop = function
+  | Onotbool -> Value.notbool
+  | Onotint -> Value.notint
+  | Oneg -> Value.negint
+let eval_add (v1,t1) (v2,t2) = match t1, t2 with
+  | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
+    let v = Value.mul (Value.of_int (sizeof ty)) v2 in
+    Value.add v1 v
+  | Tint _, Tpointer ty | Tint _, Tarray (ty, _) ->
+    let v = Value.mul (Value.of_int (sizeof ty)) v1 in
+    Value.add v2 v
+  | _ -> Value.add v1 v2
+let eval_sub (v1,t1) (v2,t2) = match t1, t2 with
+  | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
+    let v = Value.mul (Value.of_int (sizeof ty)) v2 in
+    Value.sub v1 v
+  | _ -> Value.sub v1 v2
+let choose_signedness op_signed op_unsigned v1 v2 t =
+  let op = match t with
+    | Tint (_, Signed) -> op_signed
+    | Tint (_, Unsigned) -> op_unsigned
+    | _ -> op_unsigned in
+  op v1 v2
+let eval_binop ret_ctype ((v1,t1) as e1) ((v2,t2) as e2) op =
+  let v = match op with
+    | Oadd -> eval_add e1 e2
+    | Osub -> eval_sub e1 e2
+    | Omul -> Value.mul v1 v2
+    | Odiv -> choose_signedness Value.div Value.divu v1 v2 t1
+    | Omod -> choose_signedness Value.modulo Value.modulou v1 v2 t1
+    | Oand -> Value.and_op v1 v2
+    | Oor -> Value.or_op v1 v2
+    | Oxor -> Value.xor v1 v2
+    | Oshl-> Value.shl v1 v2
+    | Oshr-> Value.shr v1 v2
+    | Oeq -> choose_signedness Value.cmp_eq Value.cmp_eq_u v1 v2 t1
+    | One -> choose_signedness Value.cmp_ne Value.cmp_ne_u v1 v2 t1
+    | Olt -> choose_signedness Value.cmp_lt Value.cmp_lt_u v1 v2 t1
+    | Ole -> choose_signedness Value.cmp_le Value.cmp_le_u v1 v2 t1
+    | Ogt -> choose_signedness Value.cmp_gt Value.cmp_gt_u v1 v2 t1
+    | Oge -> choose_signedness Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
+  eval_cast (v, t1, ret_ctype)
+let rec get_offset_struct v id fields =
+  let sizes = List.map (fun (_, ty) -> sizeof ty) fields in
+  let (offsets, _) = Mem.align 0 sizes in
+  let rec select = function
+    | (x, _) :: _, off :: _ when x = id -> off
+    | _ :: fields, _ :: offsets -> select (fields, offsets)
+    | _ -> assert false (* should be impossible *) in
+  let off = Value.of_int (select (fields, offsets)) in
+  Value.add v off
+let get_offset v id = function
+  | Tstruct (_, fields) -> get_offset_struct v id fields
+  | Tunion _ -> v
+  | _ -> assert false (* do not use on these arguments *)
+let is_true (v, _) = Value.is_true v
+let is_false (v, _) = Value.is_false v
+let rec eval_expr localenv m (Expr (ee, tt)) =
   match ee with
+    | Econst_int i ->
+        let v = (match tt with
+                   | Tint(I8,Signed) -> Value.cast8signed (Value.of_int i)
+                   | Tint(I8,Unsigned) -> Value.cast8unsigned (Value.of_int i)
+                   | Tint(I16,Signed) -> Value.cast16signed (Value.of_int i)
+                   | Tint(I16,Unsigned) -> Value.cast16unsigned (Value.of_int i)
+                   | Tint(I32,Signed) -> Value.of_int i
+                   | Tint(I32,Unsigned) -> Value.of_int i (*FIXME*)
+                   | _ -> assert false (*Type error*))
+      in ((v,tt),[])
+    | Econst_float _ -> assert false (*Not supported *)
+    | Evar id   ->
+        (match tt with
+           | Tfunction (_,_) -> ((find_symbol globalenv localenv id,tt),[])
+           | _ ->
+               ((Mem.load m (mq_of_ty tt) (find_symbol globalenv localenv id),tt),[])
+        )
+    | Ederef exp -> let ((v1,t1),l1) = eval_expr globalenv localenv m exp in
+        ((Mem.load m (mq_of_ty tt) v1,tt),l1)
+    | Eaddrof exp -> eval_lvalue globalenv localenv m exp
+    | Econst_int i ->
+      let v = eval_cast (Value.of_int i, Tint(I32, Signed), tt) in
+      ((v, tt),[])
+    | Econst_float _ -> error_float ()
+    | Evar id when is_function_type tt || is_big_type tt ->
+      let v = value_of_address (find_symbol localenv m id) in
+      ((v, tt), [])
+    | Evar id ->
+      let addr = find_symbol localenv m id in
+      let v = Mem.load m (size_of_ctype tt) addr in
+      ((v, tt), [])
+    | Ederef e when is_function_type tt || is_big_type tt ->
+      let ((v1,_),l1) = eval_expr localenv m e in
+      ((v1,tt),l1)
+    | Ederef e ->
+      let ((v1,_),l1) = eval_expr localenv m e in
+      let addr = address_of_value v1 in
+      let v = Mem.load m (size_of_ctype tt) addr in
+      ((v,tt),l1)
+    | Eaddrof exp ->
+      let ((addr,_),l) = eval_lvalue localenv m exp in
+      ((value_of_address addr,tt),l)
+    | Ebinop (op,exp1,exp2) ->
+      let (v1,l1) = eval_expr localenv m exp1 in
+      let (v2,l2) = eval_expr localenv m exp2 in
+      ((eval_binop tt v1 v2 op,tt),l1@l2)
     | Eunop (op,exp) ->
+        let (v1,l1) = eval_expr globalenv localenv m exp in
+          ((eval_unop v1 op,tt),l1)
+    | Ebinop (op,exp1,exp2) ->
+        let (v1,l1) = eval_expr globalenv localenv m exp1
+        and (v2,l2) = eval_expr globalenv localenv m exp2 in
+          ((eval_binop v1 v2 op,tt),l1@l2)
+    | Ecast (cty,exp) ->
+        let ((v,ty),l1) = eval_expr globalenv localenv m exp in
+          ((eval_cast (v,ty,cty),tt),l1)
+      let ((v1,_),l1) = eval_expr localenv m exp in
+      ((eval_unop op v1,tt),l1)
     | Econdition (e1,e2,e3) ->
+        let (v1,l1) = eval_expr globalenv localenv m e1 in
+          if is_true v1 then
+            let (v2,l2) = eval_expr globalenv localenv m e2 in
+              (v2,l1@l2)
+          else if is_false v1 then
+            let (v2,l2) = eval_expr globalenv localenv m e3 in
+              (v2,l1@l2)
+          else ((Value.undef,tt),l1)
+      let (v1,l1) = eval_expr localenv m e1 in
+      if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
+      else
+        if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)
+      else (v1,l1)
     | Eandbool (e1,e2) ->
+        let (v1,l1) = eval_expr globalenv localenv m e1 in
+          if is_true v1 then (
+            let (v2,l2) = eval_expr globalenv localenv m e2 in
+              if is_true v2 then
+                ((Value.val_true,tt),l1@l2)
+              else (
+                if is_false v2 then ((Value.val_false,tt),l1@l2)
+                else ((Value.undef,tt),l1@l2)
+              )) else (
+                if is_false v1 then ((Value.val_false,tt),l1)
+                else ((Value.undef,tt),l1))
+      let (v1,l1) = eval_expr localenv m e1 in
+      if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
+      else (v1,l1)
     | Eorbool (e1,e2) ->
+        let (v1,l1) = eval_expr globalenv localenv m e1 in
+          if is_false v1 then (
+            let (v2,l2) = eval_expr globalenv localenv m e2 in
+              if is_true v2 then ((Value.val_true,tt),l1@l2)
+              else (
+                if is_false v2 then ((Value.val_false,tt),l1@l2)
+                else ((Value.undef,tt),l1@l2)
+          )) else (
+            if is_true v1 then ((Value.val_true,tt),l1)
+            else ((Value.undef,tt),l1))
+      let (v1,l1) = eval_expr localenv m e1 in
+      if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
+      else (v1,l1)
     | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
     | Efield (e1,id) ->
+        let (v1,l1) = eval_expr globalenv localenv m e1 in
+        (match v1 with
+           | (v,Tstruct(_,lst)) when List.mem (id,tt) lst ->
+               ((Mem.load m (mq_of_ty tt) (get_offset_struct v id lst),tt),l1)
+           | (v,Tunion(_,lst)) when List.mem (id,tt) lst ->
+               ((Mem.load m (mq_of_ty tt) v,tt),l1)
+           | _ -> ((Value.undef,tt),l1)
+        )
+    | Ecost (lbl,e1) -> let (v1,l1) = eval_expr globalenv localenv m e1 in
+        (v1,lbl::l1)
+    | Ecall _ -> assert false (*For annotations only*)
+and eval_lvalue globalenv localenv m expr =
+  let Expr (e,t) = expr in match e with
+    | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
+    | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
+    | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
+    | Efield (ee,id) -> let (v1,l1) = eval_expr globalenv localenv m ee in
+        (match v1 with
+           | (v,Tstruct(_,lst)) when List.mem (id,t) lst ->
+               ((get_offset_struct v id lst,t),l1)
+           | (v,Tunion(_,lst)) when List.mem (id,t) lst -> ((v,t),l1)
+           | _ -> ((Value.undef,t),l1)
+        )
+    | Evar id -> ((find_symbol globalenv localenv id,t),[])
+    | Ederef ee -> let ((v,_),l1) = eval_expr globalenv localenv m ee in
+        ((v,t),l1)
+    | Ecost (lbl,ee) -> let (v,l) = eval_lvalue globalenv localenv m ee in
+        (v,lbl::l)
+    | Ecall _ -> assert false (*For annotation only*)
+let eval_exprlist globalenv localenv m l =
+  let rec eval_exprlist_rec vl ll = function
+    | [] -> (vl,ll)
+    | e::lst ->
+        let (vl0,ll0) = eval_exprlist_rec vl ll lst
+        and ((v,_),t) = eval_expr globalenv localenv m e in
+        (v::vl0,t@ll0)
+  in eval_exprlist_rec [] [] l
+let is_struct = function
+  | Tarray (_,_) | Tunion (_,_) | Tstruct (_,_) -> true
+  | _ -> false
+let bind_parameters m param_l arg_l var_l =
+ let bind (m,e) (id,ty) arg =
+   if is_struct ty then (
+     assert (arg=Value.undef); (*a parameter can't be a struct/union/array*)
+     let (m2,ptr2) = Mem.alloc m (sizeof ty)
+     in let (m3,ptr3) = Mem.alloc m2 (Mem.ptr_size)
+     in let m4 = Mem.store m3 (Mem.mq_of_ptr) ptr3 ptr2
+     in (m4, (Hashtbl.add e id ptr3;e) ))
+   else
+     let (m2,ptr) = Mem.alloc m (sizeof ty) in
+     let m3 = Mem.store m2 (mq_of_ty ty) ptr arg
+     in (m3, (Hashtbl.add e id ptr;e) )
+ in
+   List.fold_left
+     (fun a b -> bind a b Value.undef)
+     (try List.fold_left2 bind (m,Hashtbl.create 13) param_l arg_l
+     with (Invalid_argument _) -> assert false)
+     var_l
+let assign m v ty ptr = Mem.store m (mq_of_ty ty) ptr v
+let type_of_fundef = function
+  | Internal f -> Tfunction (List.map snd f.fn_params,f.fn_return)
+  | External (_,p,t) -> Tfunction (p,t)
+let rec free_list m = function
+  | [] -> m
+  | v::l -> free_list (Mem.free m v) l
+let blocks_of_env e =
+  let l = ref [] in
+    Hashtbl.iter (fun _ b -> l:=b::(!l)) e;!l
+let typeof e = let Expr (_,t) = e in t
+let interpret_external vargs k m = function
+    | "scan_int" ->
+          Returnstate (Value.of_int (int_of_string (read_line ())), k, m)
+    | "print_int" when List.length vargs = 1 ->
+        Printf.printf "%d" (Value.to_int (List.hd vargs)) ;
+        Returnstate (Value.zero, k, m)
+    | "print_intln" when List.length vargs = 1 ->
+        Printf.printf "%d\n" (Value.to_int (List.hd vargs)) ;
+        Returnstate (Value.zero, k, m)
+    | "malloc" | "alloc" when List.length vargs = 1 ->
+        let (m',vv) = Mem.alloc m (Value.to_int (List.hd vargs)) in
+          Returnstate (vv, k, m')
+   | "exit"  when List.length vargs = 1 -> Returnstate(List.hd vargs,Kstop,m)
+   | s -> Printf.eprintf "Error: unknown external function: %s\n" s;
+          assert false (*Unknown external function*)
+let next_step globalenv = function
+    | State(f,Sassign(a1,a2),k,e,m) ->
+        let ((v1,t1),l1) = (eval_lvalue globalenv e m a1)
+        and ((v2,t2),l2) = eval_expr globalenv e m a2
+        in (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
+    | State(f,Scall(None,a,al),k,e,m) ->
+        let (v1,l1) = eval_expr globalenv e m a in
+        let fd = find_funct globalenv v1
+        and (vargs,l2) = (eval_exprlist globalenv e m al) in
+          if type_of_fundef fd = typeof a
+          then (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
+          else assert false (*Signature mismatches*)
+  | State(f,Scall(Some lhs,a,al),k,e,m) ->
+      let (v1,l1) = eval_expr globalenv e m a in
+      let fd = find_funct globalenv v1
+      and (vargs,l2) = (eval_exprlist globalenv e m al)
+      and ((v3,t3),l3) = eval_lvalue globalenv e m lhs in
+        if type_of_fundef fd = typeof a then
+          (Callstate(fd,vargs,Kcall(Some (v3, t3),f,e,k),m),l1@l2@l3)
+        else assert false (*Signature mismatches*)
+  | State(f,Ssequence(s1,s2),k,e,m) -> (State(f,s1,Kseq(s2,k),e,m),[])
+  | State(f,Sskip,Kseq(s,k),e,m) -> (State(f,s,k,e,m),[])
+  | State(f,Scontinue,Kseq(s,k),e,m) -> (State(f,Scontinue,k,e,m),[])
+  | State(f,Sbreak,Kseq(s,k),e,m) -> (State(f,Sbreak,k,e,m),[])
+  | State(f,Sifthenelse(a,s1,s2),k,e,m) ->
+      let (v1,l1) = eval_expr globalenv e m a in
+        if is_true v1 then (State(f,s1,k,e,m),l1)
+        else if is_false v1 then (State(f,s2,k,e,m),l1)
+        else assert false (*Wrong condition guard*)
+  | State(f,Swhile(a,s),k,e,m) ->
+      let (v1,l1) = eval_expr globalenv e m a in
+        if is_false v1 then (State(f,Sskip,k,e,m),l1)
+        else if is_true v1 then (State(f,s,Kwhile(a,s,k),e,m),l1)
+        else assert false (*Wrong condition guard*)
+  | State(f,Sskip,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
+  | State(f,Scontinue,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
+  | State(f,Sbreak,Kwhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
+  | State(f,Sdowhile(a,s),k,e,m) -> (State(f,s,Kdowhile(a,s,k),e,m),[])
+  | State(f,Sskip,Kdowhile(a,s,k),e,m) ->
+      let (v1,l1) = eval_expr globalenv e m a in
+        if is_false v1 then (State(f,Sskip,k,e,m),l1)
+        else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
+        else assert false (*Wrong condition guard*)
+  | State(f,Scontinue,Kdowhile(a,s,k),e,m) ->
+      let (v1,l1) = eval_expr globalenv e m a in
+        if is_false v1 then (State(f,Sskip,k,e,m),l1)
+        else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
+        else assert false (*Wrong condition guard*)
+  | State(f,Sbreak,Kdowhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
+  | State(f,Sfor(a1,a2,a3,s),k,e,m) when a1<>Sskip ->
+      (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
+  | State(f,Sfor(Sskip,a2,a3,s),k,e,m) ->
+      let (v1,l1) = eval_expr globalenv e m a2 in
+      if is_false v1 then (State(f,Sskip,k,e,m),l1)
+      else if is_true v1 then (State(f,s,Kfor2(a2,a3,s,k),e,m),l1)
+      else assert false (*Wrong condition guard*)
+  | State(f,Sskip,Kfor2(a2,a3,s,k),e,m) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
+  | State(f,Scontinue,Kfor2(a2,a3,s,k),e,m) ->
+      (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
+  | State(f,Sbreak,Kfor2(a2,a3,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
+  | State(f,Sskip,Kfor3(a2,a3,s,k),e,m) ->
+      (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
+  | State(f,Sreturn None,k,e,m) when f.fn_return = Tvoid ->
+      let m' = free_list m (blocks_of_env e) in
+        (Returnstate(Value.undef,(call_cont k),m'),[])
+  | State(f,Sreturn (Some a),k,e,m) when f.fn_return<>Tvoid ->
+      let (v1,l1) = eval_expr globalenv e m a
+      and m' = free_list m (blocks_of_env e) in
+        (Returnstate(fst v1,call_cont k,m'),l1)
+  | State(f,Sskip,k,e,m) when f.fn_return = Tvoid && is_call_cont k ->
+      let m' = free_list m (blocks_of_env e) in
+        (Returnstate(Value.undef,k,m'),[])
+  | State(f,Sswitch(a,sl),k,e,m) ->
+      let (n,l) = (match eval_expr globalenv e m a with
+                     | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll)
+                     | _ -> assert false (*Wrong switch index*)
+      ) in
+        (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
+  | State(f,Sskip,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
+  | State(f,Sbreak,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
+  | State(f,Scontinue,Kswitch k,e,m) -> (State(f,Scontinue,k,e,m),[])
+  | State(f,Slabel(lbl,s),k,e,m) -> (State(f,s,k,e,m),[])
+  | State(f,Scost(lbl,s),k,e,m) -> (State(f,s,k,e,m),[lbl])
+  | State(f,Sgoto lbl,k,e,m) ->
+      (match find_label lbl f.fn_body (call_cont k) with
+         | Some (s',k') -> (State(f,s',k',e,m),[])
+         | None -> assert false (*Label does not exist*))
+  | Callstate(Internal f,vargs,k,m) ->
+      let (m',e) = bind_parameters m f.fn_params vargs f.fn_vars in
+        (State(f,f.fn_body,k,e,m'),[])
+  | Callstate(External(id,targs,tres),vargs,k,m)
+      when List.length targs = List.length vargs ->
+      (interpret_external vargs k m id,[])
+      let ((v1,t1),l1) = eval_expr localenv m e1 in
+      let addr = address_of_value (get_offset v1 id t1) in
+      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
+    | Ecost (lbl,e1) ->
+      let (v1,l1) = eval_expr localenv m e1 in
+      (v1,lbl::l1)
+    | Ecall _ -> assert false (* only used by the annotation process *)
+    | Ecast (cty,exp) ->
+      let ((v,ty),l1) = eval_expr localenv m exp in
+      ((eval_cast (v,ty,cty),tt),l1)
+and eval_lvalue localenv m (Expr (e,t)) = match e with
+  | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
+  | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
+  | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
+  | Evar id -> ((find_symbol localenv m id,t),[])
+  | Ederef ee ->
+    let ((v,_),l1) = eval_expr localenv m ee in
+    ((address_of_value v,t),l1)
+  | Efield (ee,id) ->
+    let ((v,tt),l1) = eval_expr localenv m ee in
+    let v' = get_offset v id tt in
+    ((address_of_value v', t), l1)
+  | Ecost (lbl,ee) ->
+    let (v,l) = eval_lvalue localenv m ee in
+    (v,lbl::l)
+  | Ecall _ -> assert false (* only used in the annotation process *)
+let eval_exprlist lenv mem es =
+  let f (vs, cost_lbls) e =
+    let ((v, _), cost_lbls') = eval_expr lenv mem e in
+    (vs @ [v], cost_lbls @ cost_lbls') in
+  List.fold_left f ([], []) es
+let bind (mem, lenv) (x, ty) v =
+  let (mem, addr) = Mem.alloc mem (sizeof ty) in
+  let mem = Mem.store mem (sizeof ty) addr v in
+  let lenv = LocalEnv.add x addr lenv in
+  (mem, lenv)
+let bind_var (mem, lenv) (x, ty) = bind (mem, lenv) (x, ty) Value.undef
+let init_fun_env mem params args vars =
+  let lenv = LocalEnv.empty in
+  let (mem, lenv) =
+    try List.fold_left2 bind (mem, lenv) params args
+    with Invalid_argument _ -> error "wrong size of arguments." in
+  List.fold_left bind_var (mem, lenv) vars
+let assign m v ty ptr = Mem.store m (size_of_ctype ty) ptr v
+let free_local_env mem lenv =
+  let f _ addr mem = Mem.free mem addr in
+  LocalEnv.fold f lenv mem
+let condition v a_true a_false =
+  if Value.is_false v then a_false
+  else if Value.is_true v then a_true
+  else error "undefined condition guard value."
+let eval_stmt f k e m s = match s, k with
+  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
+  | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
+  | Sskip, Kdowhile(a,s,k) ->
+    let ((v1, _),l1) = eval_expr e m a in
+    let a_false = (State(f,Sskip,k,e,m),l1) in
+    let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
+    condition v1 a_true a_false
+  | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
+  | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
+  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
+  | Sskip, Kcall _ ->
+    let m' = free_local_env m e in
+    (Returnstate(Value.undef,k,m'),[])
+  | Sassign(a1, a2), _ ->
+    let ((v1,t1),l1) = (eval_lvalue e m a1) in
+    let ((v2,t2),l2) = eval_expr e m a2 in
+    (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
+  | Scall(None,a,al), _ ->
+    let ((v1,_),l1) = eval_expr e m a in
+    let fd = Mem.find_fun_def m (address_of_value v1) in
+    let (vargs,l2) = eval_exprlist e m al in
+    (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
+  | Scall(Some lhs,a,al), _ ->
+    let ((v1,_),l1) = eval_expr e m a in
+    let fd = Mem.find_fun_def m (address_of_value v1) in
+    let (vargs,l2) = eval_exprlist e m al in
+    let (vt3,l3) = eval_lvalue e m lhs in
+    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3)
+  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[])
+  | Sifthenelse(a,s1,s2), _ ->
+    let ((v1,_),l1) = eval_expr e m a in
+    let a_true = (State(f,s1,k,e,m),l1) in
+    let a_false = (State(f,s2,k,e,m),l1) in
+    condition v1 a_true a_false
+  | Swhile(a,s), _ ->
+    let ((v1,_),l1) = eval_expr e m a in
+    let a_false = (State(f,Sskip,k,e,m),l1) in
+    let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in
+    condition v1 a_true a_false
+  | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
+  | Sfor(Sskip,a2,a3,s), _ ->
+    let ((v1,_),l1) = eval_expr e m a2 in
+    let a_false = (State(f,Sskip,k,e,m),l1) in
+    let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
+    condition v1 a_true a_false
+  | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
+  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[])
+  | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
+  | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
+  | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[])
+  | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[])
+  | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[])
+  | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
+  | Scontinue, Kdowhile(a,s,k) ->
+    let ((v1,_),l1) = eval_expr e m a in
+    let a_false = (State(f,Sskip,k,e,m),l1) in
+    let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
+    condition v1 a_true a_false
+  | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
+  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[])
+  | Sreturn None, _ ->
+    let m' = free_local_env m e in
+    (Returnstate(Value.undef,(call_cont k),m'),[])
+  | Sreturn (Some a), _ ->
+    let ((v1,_),l1) = eval_expr e m a  in
+    let m' = free_local_env m e in
+    (Returnstate(v1,call_cont k,m'),l1)
+  | Sswitch(a,sl), _ ->
+    let ((v,_),l) = eval_expr e m a in
+    let n = Value.to_int v in
+    (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
+  | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[])
+  | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl])
+  | Sgoto lbl, _ ->
+    let (s', k') = find_label lbl f.fn_body (call_cont k) in
+    (State(f,s',k',e,m),[])
+  | _ -> assert false (* should be impossible *)
+module InterpretExternal = Primitive.Interpret (Mem)
+let interpret_external k mem f args =
+  let (mem', v) = match InterpretExternal.t mem f args with
+    | (mem', InterpretExternal.V v) -> (mem', v)
+    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
+  Returnstate (v, k, mem')
+let step_call args cont mem = function
+  | Internal f ->
+    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
+    State (f, f.fn_body, cont, e, mem')
+  | External(id,targs,tres) when List.length targs = List.length args ->
+    interpret_external cont mem id args
+  | External(id,_,_) ->
+    error ("wrong size of arguments when calling external " ^ id ^ ".")
+let step = function
+  | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
+  | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
   | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
   | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) ->
+      let m' = assign m v ty vv in
+        (State(f,Sskip,k,e,m'),[])
+  | st ->
+      Printf.eprintf "Error: no transition for %s\n" (string_of_state st);
+      assert false
+let init_to_data = function
+    let m' = assign m v ty vv in
+    (State(f,Sskip,k,e,m'),[])
+  | _ -> error "state malformation."
+let data_of_init_data = function
   | Init_int8 i         -> Data_int8 i
   | Init_int16 i        -> Data_int16 i
   | Init_int32 i        -> Data_int32 i
   | Init_float32 f      -> assert false (* Not supported *)
   | Init_float64 f      -> assert false (* Not supported *)
+  | Init_float32 f      -> error_float ()
+  | Init_float64 f      -> error_float ()
   | Init_space i        -> Data_reserve i
+  | Init_addrof (_,_)   -> assert false (*TODO*)
+let alloc_datas m ((_,lst),ty) =
+  let store_data (m,ptr) = function (*FIXME signed or unsigned ?*)
+    | Init_int8  i -> (Mem.store m Memory.MQ_int8signed ptr (Value.of_int i)
+                       ,Value.add ptr (Value.of_int 1))
+    | Init_int16 i -> (Mem.store m Memory.MQ_int16signed ptr (Value.of_int i)
+                       ,Value.add ptr (Value.of_int 2))
+    | Init_int32 i -> (Mem.store m Memory.MQ_int32 ptr (Value.of_int i)
+                       ,Value.add ptr (Value.of_int 4))
+    | Init_float32 _ -> assert false (*Not supported*)
+    | Init_float64 _ -> assert false (*Not supported*)
+    | Init_space n -> (m,Value.add ptr (Value.of_int n))
+    | Init_addrof (_,_) -> assert false (*TODO*)
+  in let (m2,ptr) = (Mem.alloc m (sizeof ty))
+  in (fst (List.fold_left store_data (m2,ptr) lst),ptr)
+let initmem_clight prog =
+  let alloc_funct i (g,f) (id,fct) =
+    Hashtbl.add g id (Value.of_int (-i-1));
+    Valtbl.add f (Value.of_int (-i-1)) fct;
+    (g,f)
+  and alloc_var (m,g) v =
+    let (m',ptr) = alloc_datas m v in
+      if is_struct (snd v) then
+        let (m2,ptr2) = Mem.alloc m' (Mem.ptr_size) in
+        let m3 = Mem.store m2 Mem.mq_of_ptr ptr2 ptr in
+        Hashtbl.add g (fst (fst v)) ptr2;(m3,g)
+      else
+        ( (Hashtbl.add g (fst (fst v)) ptr);(m',g) )
+  in let (m,g) =
+    List.fold_left alloc_var (Mem.empty,Hashtbl.create 13) prog.prog_vars
+  in let (g2,f) =
+    MiscPottier.foldi alloc_funct (g,Valtbl.create 13) prog.prog_funct
+  in
+    (m,(g2,f))
+  | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *)
+let init_mem prog =
+  let f_var mem ((x, init_datas), ty) =
+    Mem.add_var mem x (List.map data_of_init_data init_datas) in
+  let mem = List.fold_left f_var Mem.empty prog.prog_vars in
+  let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
+  List.fold_left f_fun_def mem prog.prog_funct
 let compute_result v =
 …
   else IntValue.Int8.zero
+let interpret debug prog = match prog.prog_main with
+  | None -> (IntValue.Int8.zero, [])
+  | Some main ->
+      let (m,g) = initmem_clight prog in
+      let first_state = (Callstate(find_funct_id g main,[],Kstop,m),[]) in
+      let rec exec trace = function
+        | (Returnstate(v,Kstop,m),l) ->
+(*
+            if debug then (
+              print_string ("Result: "^(Value.to_string v));
+              print_string ("\nMemory dump: \n");
+              Mem.print m
+            );
+*)
+          let (res, cost_labels) as trace = (compute_result v, l@trace) in
+          if debug then
+            Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ;
+          trace
+        | (State(_,Sskip,Kstop,_,m),l) -> (*Implicit return in main*)
+(*
+            if debug then (
+              print_string ("Result: (implicit return)");
+              print_string ("\nMemory dump: \n");
+              Mem.print m
+            );
+*)
+          let (res, cost_labels) as trace = (IntValue.Int8.zero, l@trace) in
+          if debug then
+            Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ;
+          trace
+        | (state,l) ->
+(*
+            if debug then print_string ((string_of_state state)^"\n");
+*)
+            exec (l@trace) (next_step g state)
+      in
+(*
+      if debug then print_string "> --- Interpret Clight --- <\n";
+*)
+      exec [] first_state
+let rec exec debug trace (state, l) =
+  let cost_labels = l @ trace in
+  let print_and_return_result res =
+    if debug then Printf.printf "Result = %s\n%!"
+      (IntValue.Int8.to_string res) ;
+    (res, cost_labels) in
+  if debug then print_state state ;
+  match state with
+    | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
+      print_and_return_result (compute_result v)
+    | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
+      print_and_return_result IntValue.Int8.zero
+    | state -> exec debug cost_labels (step state)
+let interpret debug prog =
+  if debug then Printf.printf "*** Clight ***\n\n%!" ;
+  match prog.prog_main with
+    | None -> (IntValue.Int8.zero, [])
+    | Some main ->
+      let mem = init_mem prog in
+      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
+      exec debug [] first_state

Deliverables/D2.2/8051/src/clight/clightInterpret.mli

r486	r740
3	3	can also print debug informations. *)
4	4
	5	(** [interpret debug p] returns the trace of execution of program [p]. *)
	6
5	7	val interpret: bool -> Clight.program -> AST.trace

Deliverables/D2.2/8051/src/clight/clightParser.ml

-                      r486
+                      r740
 let process file =
+  let tmp_file = Filename.temp_file "cparser" ".i"
+  let tmp_file1 = Filename.temp_file "cparser1" ".c"
+  and tmp_file2 = Filename.temp_file "cparser2" ".i"
   and prepro_opts = [] in
+  (* Add CerCo's primitives *)
+  let _ =
+    try
+      let oc = open_out tmp_file1 in
+      output_string oc Primitive.prototypes ;
+      close_out oc
+    with Sys_error _ -> failwith "Error adding primitive prototypes." in
+  let rc = Sys.command
+    (Printf.sprintf "cat %s >> %s"
+       (Filename.quote file) (Filename.quote tmp_file1)) in
+  if rc <> 0 then (
+    Misc.SysExt.safe_remove tmp_file1;
+    failwith "Error adding primitive prototypes."
+  );
   (* Preprocessing *)
 …
     (Printf.sprintf "gcc -E -U__GNUC__ %s %s > %s"
        (String.concat " " (List.map Filename.quote prepro_opts))
        (Filename.quote file) (Filename.quote tmp_file)) in
+       (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
   if rc <> 0 then (
+    Misc.SysExt.safe_remove tmp_file; failwith "Error calling gcc."
+    Misc.SysExt.safe_remove tmp_file1;
+    Misc.SysExt.safe_remove tmp_file2;
+    failwith "Error calling gcc."
   );
   (* C to Cil *)
+  let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file in
+  Misc.SysExt.safe_remove tmp_file;
+  let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
+  Misc.SysExt.safe_remove tmp_file1;
+  Misc.SysExt.safe_remove tmp_file2;
   match r with
     | None -> failwith "Error during C parsing."

Deliverables/D2.2/8051/src/clight/clightToCminor.ml

-                      r624
+                      r740
 open Cminor
 open Clight
+let error_prefix = "Cminor to RTLabs"
+let error = Error.global_error error_prefix
+let error_float () = error "float not supported."
 (*For internal use*)
 …
 let ptr_size = Driver.CminorMemory.ptr_size
 let alignment = Driver.CminorMemory.alignment
-let ptr_mq = Memory.MQ_pointer
 let fresh_tmp variables =
 …
   | _           -> Sig_int
 let rec mq_of_ty = function
+let rec size_of_ty = function
   | Tvoid               -> assert false
   | Tfloat _            -> assert false (*Not supported*)
   | Tfunction (_,_)     -> assert false (*Not supported*)
   | Tint (I8,Signed)    -> Memory.MQ_int8signed
   | Tint (I8,Unsigned)  -> Memory.MQ_int8unsigned
   | Tint (I16,Signed)   -> Memory.MQ_int16signed
   | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned
+  | Tint (I8,Signed)    -> 1
+  | Tint (I8,Unsigned)  -> 1
+  | Tint (I16,Signed)   -> 2
+  | Tint (I16,Unsigned) -> 2
   (*FIXME MQ_int32 : signed or unsigned ? *)
   | Tint (I32,Signed)   -> Memory.MQ_int32
   | Tint (I32,Unsigned) ->  Memory.MQ_int32
+  | Tint (I32,Signed)   -> 4
+  | Tint (I32,Unsigned) -> 4
   | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
+  | Tcomp_ptr _         -> ptr_mq
+  | Tcomp_ptr _         -> ptr_size
+let size_of_intsize = function
+  | I8 -> 1
+  | I16 -> 2
+  | I32 -> 4
+let quantity_of_ty = function
+  | Tvoid               -> assert false (* do not use on this argument *)
+  | Tint (size,_)       -> Memory.QInt (size_of_intsize size)
+  | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
+  | Tfunction (_,_)
+  | Tcomp_ptr _         -> Memory.QPtr
+  | Tfloat _            -> error_float ()
 let init_to_data l = List.map (
 …
       Op2 (Op_addp,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t))))
   | (Tint(_,_),Tpointer t)      ->
       Op2 (Op_addp,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))),e2)
+      Op2 (Op_addp,e2,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))))
   | (Tarray (t,_),Tint(_,_))    ->
       Op2 (Op_addp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
 …
   | (Tpointer t,Tint(_,_))      ->
       Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
-  | (Tint(_,_),Tpointer t)      ->
-      Op2 (Op_subp,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))),e2)
   | (Tarray (t,_),Tint(_,_))    ->
       Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
-  | (Tint(_,_),Tarray(t,_))     ->
-      Op2 (Op_subp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
   | _                           -> assert false (*Type error*)
 …
 let translate_div e1 e2 = function
-(*
   | (Tint(_,Signed),Tint(_,Signed))     -> Op2 (Op_div,e1,e2)
-*)
-  (* TODO: temporary hack! *)
-  | (Tint(_,Signed),Tint(_,Signed))     -> Op2 (Op_divu,e1,e2)
   | (Tint(_,Unsigned),Tint(_,Unsigned)) -> Op2 (Op_divu,e1,e2)
   | (Tfloat _,Tfloat _)                 -> assert false (*Not supported*)
 …
 let make_cast e = function
   | (Tint(_,_),Tint(I8,Signed)) when int_size>8     -> Op1 (Op_cast8signed,e)
   | (Tint(_,_),Tint(I8,Unsigned)) when int_size>8   -> Op1 (Op_cast8unsigned,e)
   | (Tint(_,_),Tint(I16,Signed)) when int_size>16   -> Op1 (Op_cast16signed,e)
   | (Tint(_,_),Tint(I16,Unsigned)) when int_size>16 -> Op1 (Op_cast16unsigned,e)
+  | (Tint(I8,Signed),Tint(_,_))    -> Op1 (Op_cast8signed,e)
+  | (Tint(I8,Unsigned),Tint(_,_))  -> Op1 (Op_cast8unsigned,e)
+  | (Tint(I16,Signed),Tint(_,_))   -> Op1 (Op_cast16signed,e)
+  | (Tint(I16,Unsigned),Tint(_,_)) -> Op1 (Op_cast16unsigned,e)
   | _ -> e
 …
            | (Local,_)          -> Id id
            | (Stack o,ty) when is_struct ty     -> Cst (Cst_stackoffset o)
+           | (Stack o,_)        -> Mem (mq_of_ty c,Cst (Cst_stackoffset o))
+           | (Stack o,_)        ->
+             Mem (quantity_of_ty c,Cst (Cst_stackoffset o))
            | (Param,_)          -> Id id
            | (Global,ty) when is_struct ty -> Cst (Cst_addrsymbol id)
+           | (Global,_)         -> Mem (mq_of_ty c,Cst (Cst_addrsymbol id))
+           | (Global,_)         ->
+             Mem (quantity_of_ty c,Cst (Cst_addrsymbol id))
         ) with Not_found -> assert false)
     | Ederef e when is_ptr_to_struct (get_type e) ->
         translate_expr variables e
     | Ederef e          -> Mem (mq_of_ty c,translate_expr variables e)
+    | Ederef e          -> Mem (quantity_of_ty c,translate_expr variables e)
     | Eaddrof se        ->  (
         match se with
 …
            | Tstruct(_,lst) ->
                (try
                   Mem (mq_of_ty (List.assoc id lst)
+                  Mem (quantity_of_ty (List.assoc id lst)
                        ,Op2(Op_add
                             ,translate_expr variables e
 …
            | Tunion(_,lst) ->
                (try
                   Mem (mq_of_ty (List.assoc id lst), translate_expr variables e)
+                  Mem (quantity_of_ty (List.assoc id lst), translate_expr variables e)
                 with Not_found -> assert false (*field does not exists*)
+               )
 …
       (try (match Hashtbl.find variables v with
          | (Local,_)            -> St_assign (v,translate_expr variables e)
          | (Stack o,_)          -> St_store (mq_of_ty t
+         | (Stack o,_)          -> St_store (quantity_of_ty t
                                              ,Cst (Cst_stackoffset o)
                                              ,translate_expr variables e)
          | (Param,_)            -> St_assign (v,translate_expr variables e)
          | (Global,_)           -> St_store (mq_of_ty t
+         | (Global,_)           -> St_store (quantity_of_ty t
                                              ,Cst (Cst_addrsymbol v)
                                              ,translate_expr variables e)
       ) with Not_found -> assert false)
   | Expr (Ederef ee,t)          -> St_store (mq_of_ty t
+  | Expr (Ederef ee,t)          -> St_store (quantity_of_ty t
                                              ,translate_expr variables ee
                                              ,translate_expr variables e)
 …
       (match ee with
          | Expr (_,Tstruct(_,lst)) ->
              St_store (mq_of_ty t
+             St_store (quantity_of_ty t
                        ,Op2(Op_add,translate_expr variables ee
                             ,Cst(Cst_int (get_offset_struct 0 id lst )))
                        ,translate_expr variables e)
          | Expr (_,Tunion(_,_)) -> St_store (mq_of_ty t
+         | Expr (_,Tunion(_,_)) -> St_store (quantity_of_ty t
                                              ,translate_expr variables ee
                                              ,translate_expr variables e)
 …
                          St_seq (
                            st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
                            ,St_store (mq_of_ty tt,Cst (Cst_stackoffset o),Id tmp)
+                           ,St_store (quantity_of_ty tt,Cst (Cst_stackoffset o),Id tmp)
+                         )
                    | (Global,_) ->
 …
                          St_seq (
                            st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
                            ,St_store (mq_of_ty tt,Cst (Cst_addrsymbol v),Id tmp)
+                           ,St_store (quantity_of_ty tt,Cst (Cst_addrsymbol v),Id tmp)
+                         )
                 ) with Not_found -> assert false )
 …
 let translate p =
-  (* TODO: Clight32 to Clight8 transformation *)
-(*
   let p = Clight32ToClight8.translate p in
-*)
-  (* <DEBUG> *)
-(*
-  Printf.printf "%s\n%!" (ClightPrinter.print_program p) ;
-*)
-  (* </DEBUG> *)
   let globals = List.map (fun p -> (fst (fst p),snd p) ) p.prog_vars in
   let p =
 …
      Cminor.functs = List.map (translate_funct globals ) p.prog_funct;
      Cminor.main = p.prog_main } in
+  (* TODO: find a better solution to get the pointers in the result. *)
   CminorPointers.fill p

Deliverables/D2.2/8051/src/cminor/cminor.mli

-                      r486
+                      r740
   | Op1 of AST.op1 * expression
   | Op2 of AST.op2 * expression * expression
   | Mem of Memory.memory_q * expression          (* Memory read *)
+  | Mem of Memory.quantity * expression          (* Memory read *)
   | Cond of expression * expression * expression (* Ternary expression *)
   | Exp_cost of CostLabel.t * expression         (* Labelled expression *)
 …
   | St_skip
   | St_assign of AST.ident * expression
   | St_store of Memory.memory_q * expression * expression
+  | St_store of Memory.quantity * expression * expression
   (* Function call. Parameters are an optional variable to store the

Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml

-                      r640
+                      r740
 let increment cost_id incr =
   let cost = Cminor.Cst (AST.Cst_addrsymbol cost_id) in
   let load = Cminor.Mem (Memory.MQ_int32, cost) in
+  let load = Cminor.Mem (Memory.QInt 4, cost) in
   let incr = Cminor.Op2 (AST.Op_add, load, Cminor.Cst (AST.Cst_int incr)) in
   Cminor.St_store (Memory.MQ_int32, cost, incr)
+  Cminor.St_store (Memory.QInt 4, cost, incr)

Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml

-                      r619
+                      r740
 module Mem = Driver.CminorMemory
 module Value = Mem.Value
+module Valtbl = Hashtbl.Make(Value)
+let print_hashtbl h name =
+  print_string ("Hashtbl "^name^":\n");
+  Hashtbl.iter (fun a _ -> print_string (" - "^a^"\n") ) h
+(* Type definition *)
+type local_env = (ident,Value.t) Hashtbl.t
+module LocalEnv = Map.Make(String)
+type local_env = Value.t LocalEnv.t
+type memory = Cminor.function_def Mem.memory
+let error_prefix = "Cminor interpret"
+let error s = Error.global_error error_prefix s
+let warning s = Error.warning error_prefix s
+let error_float () = error "float not supported."
+(* Helpers *)
+let value_of_address = List.hd
+let address_of_value v = [v]
+(* State of execution *)
 type continuation =
 …
   | Ct_endblock of continuation
   | Ct_returnto of
       ident option*internal_function*Value.t*local_env*continuation
+      ident option*internal_function*Value.address*local_env*continuation
 type state =
     State_regular of
       internal_function*statement*continuation*Value.t*local_env*(function_def Mem.memory)
+      internal_function*statement*continuation*Value.address*local_env*(function_def Mem.memory)
   | State_call of function_def*Value.t list*continuation*(function_def Mem.memory)
   | State_return of Value.t*continuation*(function_def Mem.memory)
+(* Local environment abstraction *)
+let get_local_value e id =
+  try Hashtbl.find e id
+  with Not_found -> assert false (*Wrong ident*)
+let set_local_value e id v = Hashtbl.add e id v
+(* Create_local_env :
+* constructs the local environement from effective parameters. *)
+let create_local_env arg params vars =
+  let h = Hashtbl.create 11 in
+  if List.length params = List.length arg then
+    (
+      for i=1 to (List.length params) do
+        Hashtbl.add h (List.nth params (i-1)) (List.nth arg (i-1))
+      done;
+      for i=1 to (List.length vars) do
+        Hashtbl.add h (List.nth vars (i-1)) Value.undef
+      done;
+      h
+    )
+  else assert false (*Wrong number of parameters*)
+(* Pretty Printing and debug *)
+let string_of_cont = function
+    Ct_stop -> "stop"
+  | Ct_cont(s1,_) -> (CminorPrinter.string_of_statement s1)^"::cont"
+  | Ct_endblock(_) -> "endblock"
+  | Ct_returnto(_,_,_,_,_) -> "returnto"
+let string_of_state = function
+    State_regular(_,s,c,_,_,_) ->
+      "State_regular { "
+      ^(CminorPrinter.string_of_statement s)^" - "^(string_of_cont c)^" }"
+  | State_call(F_ext(e),v,c,_) ->
+      "State_call { extern "
+      ^e.ef_tag
+      ^"("
+      ^(String.concat "," (List.map (fun vv -> Value.to_string vv) v))
+      ^") - "
+      ^(string_of_cont c)^" }"
+  | State_call(F_int(i),v,c,_) ->
+      "State_call { function("
+      ^(String.concat "," (List.map (fun vv -> Value.to_string vv) v))
+      ^") - "
+      ^(string_of_cont c)^" }"
+  | State_return(v,c,_) ->
+      "State_return { "^(Value.to_string v)^" - "^(string_of_cont c)^" }"
+(* Global environment abstraction *)
+(* Symbol : returns the block corresponding to the identifier
+* id in the global environement g *)
+let symbol g id = let (id_b,b_fd) = g in
+try Hashtbl.find id_b id
+with Not_found -> assert false
+(* Funct : returns the definition of the function located in block b *)
+let funct g b = let (id_b,b_fd) = g in
+try Valtbl.find b_fd b
+with Not_found -> assert false
+let string_of_local_env lenv =
+  let f x v s = s ^ x ^ " = " ^ (Value.to_string v) ^ "  " in
+  LocalEnv.fold f lenv ""
+let string_of_expr = CminorPrinter.print_expression
+let string_of_args args =
+  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
+let rec string_of_statement = function
+  | St_skip -> "skip"
+  | St_assign (x, e) -> x ^ " = " ^ (string_of_expr e)
+  | St_store (q, e1, e2) ->
+    Printf.sprintf "%s[%s] = %s"
+      (Memory.string_of_quantity q) (string_of_expr e1) (string_of_expr e2)
+  | St_call (None, f, args, _)
+  | St_tailcall (f, args, _) -> (string_of_expr f) ^ (string_of_args args)
+  | St_call (Some x, f, args, _) ->
+    x ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
+  | St_seq _ -> "sequence"
+  | St_ifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
+  | St_loop _ -> "loop"
+  | St_block _ -> "block"
+  | St_exit n -> "exit " ^ (string_of_int n)
+  | St_switch (e, _, _) -> "switch (" ^ (string_of_expr e) ^ ")"
+  | St_return None -> "return"
+  | St_return (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
+  | St_label (lbl, _) -> "label " ^ lbl
+  | St_goto lbl -> "goto " ^ lbl
+  | St_cost (lbl, _) -> "cost " ^ lbl
+let print_state = function
+  | State_regular (_, stmt, _, sp, lenv, mem) ->
+    Printf.printf "Local environment:\n%s\n\nMemory:%s\nStack pointer: %s\n\nRegular state: %s\n\n%!"
+      (string_of_local_env lenv)
+      (Mem.to_string mem)
+      (Value.to_string (value_of_address sp))
+      (string_of_statement stmt)
+  | State_call (_, args, _, mem) ->
+    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
+      (Mem.to_string mem)
+      (MiscPottier.string_of_list " " Value.to_string args)
+  | State_return (v, _, mem) ->
+    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
+      (Mem.to_string mem)
+      (Value.to_string v)
+(* Global and local environment management *)
+let init_local_env args params vars =
+  let f_param lenv x v = LocalEnv.add x v lenv in
+  let f_var lenv x = LocalEnv.add x Value.undef lenv in
+  let lenv = List.fold_left2 f_param LocalEnv.empty params args in
+  List.fold_left f_var lenv vars
+let find_fundef f mem =
+  let addr = Mem.find_global mem f in
+  Mem.find_fun_def mem addr
 (* Expression evaluation *)
+let eval_constant global_env stack = function
+    Cst_int i           -> Value.of_int i
+  | Cst_float _         -> assert false
+  | Cst_addrsymbol id   -> symbol global_env id
+  | Cst_stackoffset o   -> stack
+let eval_unop arg = function
+    Op_cast8unsigned    -> Value.cast8unsigned arg
+  | Op_cast8signed      -> Value.cast8signed arg
+  | Op_cast16unsigned   -> Value.cast16unsigned arg
+  | Op_cast16signed     -> Value.cast16signed arg
+  | Op_negint           -> Value.negint arg
+  | Op_notbool          -> Value.notbool arg
+  | Op_notint           -> Value.notint arg
+  | Op_negf             -> assert false (*Not supported*)
+  | Op_absf             -> assert false (*Not supported*)
+  | Op_singleoffloat    -> assert false (*Not supported*)
+  | Op_intoffloat       -> assert false (*Not supported*)
+  | Op_intuoffloat      -> assert false (*Not supported*)
+  | Op_floatofint       -> assert false (*Not supported*)
+  | Op_floatofintu      -> assert false (*Not supported*)
+  | Op_id               -> arg
+  | Op_ptrofint         -> assert false (*Not supported*)
+  | Op_intofptr         -> assert false (*Not supported*)
+let eval_binop arg1 arg2 = function
+    Op_add              -> Value.add arg1 arg2
+  | Op_sub              -> Value.sub arg1 arg2
+  | Op_mul              -> Value.mul arg1 arg2
+  | Op_div              -> Value.div arg1 arg2
+  | Op_divu             -> Value.divu arg1 arg2
+  | Op_mod              -> Value.modulo arg1 arg2
+  | Op_modu             -> Value.modulou arg1 arg2
+  | Op_and              -> Value.and_op arg1 arg2
+  | Op_or               -> Value.or_op arg1 arg2
+  | Op_xor              -> Value.xor arg1 arg2
+  | Op_shl              -> Value.shl arg1 arg2
+  | Op_shr              -> Value.shr arg1 arg2
+  | Op_shru             -> Value.shru arg1 arg2
+  | Op_addf             -> assert false (*Not supported*)
+  | Op_subf             -> assert false (*Not supported*)
+  | Op_mulf             -> assert false (*Not supported*)
+  | Op_divf             -> assert false (*Not supported*)
+  | Op_cmp(Cmp_eq)      -> Value.cmp_eq arg1 arg2
+  | Op_cmp(Cmp_ne)      -> Value.cmp_ne arg1 arg2
+  | Op_cmp(Cmp_gt)      -> Value.cmp_gt arg1 arg2
+  | Op_cmp(Cmp_ge)      -> Value.cmp_ge arg1 arg2
+  | Op_cmp(Cmp_lt)      -> Value.cmp_lt arg1 arg2
+  | Op_cmp(Cmp_le)      -> Value.cmp_le arg1 arg2
+  | Op_cmpu(Cmp_eq)     -> Value.cmp_eq_u arg1 arg2
+  | Op_cmpu(Cmp_ne)     -> Value.cmp_ne_u arg1 arg2
+  | Op_cmpu(Cmp_gt)     -> Value.cmp_gt_u arg1 arg2
+  | Op_cmpu(Cmp_ge)     -> Value.cmp_ge_u arg1 arg2
+  | Op_cmpu(Cmp_lt)     -> Value.cmp_lt_u arg1 arg2
+  | Op_cmpu(Cmp_le)     -> Value.cmp_le_u arg1 arg2
+  | Op_cmpf(_)          -> assert false (*Not supported*)
+  | Op_addp             -> Value.add arg1 arg2
+  | Op_subp             -> Value.sub arg1 arg2
+  | Op_cmpp(Cmp_eq)      -> Value.cmp_eq arg1 arg2
+  | Op_cmpp(Cmp_ne)      -> Value.cmp_ne arg1 arg2
+  | Op_cmpp(Cmp_gt)      -> Value.cmp_gt arg1 arg2
+  | Op_cmpp(Cmp_ge)      -> Value.cmp_ge arg1 arg2
+  | Op_cmpp(Cmp_lt)      -> Value.cmp_lt arg1 arg2
+  | Op_cmpp(Cmp_le)      -> Value.cmp_le arg1 arg2
+let rec eval_expression global_env stack local_env memory = function
+    Id(str) -> (get_local_value local_env str,[])
+  | Cst(c) -> (eval_constant global_env stack c,[])
+let eval_constant stack m = function
+  | Cst_int i -> Value.of_int i
+  | Cst_float _ -> error_float ()
+  | Cst_addrsymbol id when Mem.mem_global m id ->
+    value_of_address (Mem.find_global m id)
+  | Cst_addrsymbol id -> error ("unknown global variable " ^ id ^ ".")
+  | Cst_stackoffset o -> Value.add (value_of_address stack) (Value.of_int o)
+let eval_unop = function
+  | Op_negf
+  | Op_absf
+  | Op_singleoffloat
+  | Op_intoffloat
+  | Op_intuoffloat
+  | Op_floatofint
+  | Op_floatofintu -> error_float ()
+  | Op_cast8unsigned    -> Value.cast8unsigned
+  | Op_cast8signed      -> Value.cast8signed
+  | Op_cast16unsigned   -> Value.cast16unsigned
+  | Op_cast16signed     -> Value.cast16signed
+  | Op_negint           -> Value.negint
+  | Op_notbool          -> Value.notbool
+  | Op_notint           -> Value.notint
+  | Op_id               -> (fun v -> v)
+  | Op_ptrofint         -> assert false (*Not supported yet*)
+  | Op_intofptr         -> assert false (*Not supported yet*)
+let eval_binop = function
+  | Op_add
+  | Op_addp             -> Value.add
+  | Op_sub
+  | Op_subp             -> Value.sub
+  | Op_mul              -> Value.mul
+  | Op_div              -> Value.div
+  | Op_divu             -> Value.divu
+  | Op_mod              -> Value.modulo
+  | Op_modu             -> Value.modulou
+  | Op_and              -> Value.and_op
+  | Op_or               -> Value.or_op
+  | Op_xor              -> Value.xor
+  | Op_shl              -> Value.shl
+  | Op_shr              -> Value.shr
+  | Op_shru             -> Value.shru
+  | Op_addf
+  | Op_subf
+  | Op_mulf
+  | Op_divf
+  | Op_cmpf _           -> error_float ()
+  | Op_cmp(Cmp_eq)
+  | Op_cmpp(Cmp_eq)     -> Value.cmp_eq
+  | Op_cmp(Cmp_ne)
+  | Op_cmpp(Cmp_ne)     -> Value.cmp_ne
+  | Op_cmp(Cmp_gt)
+  | Op_cmpp(Cmp_gt)     -> Value.cmp_gt
+  | Op_cmp(Cmp_ge)
+  | Op_cmpp(Cmp_ge)     -> Value.cmp_ge
+  | Op_cmp(Cmp_lt)
+  | Op_cmpp(Cmp_lt)     -> Value.cmp_lt
+  | Op_cmp(Cmp_le)
+  | Op_cmpp(Cmp_le)     -> Value.cmp_le
+  | Op_cmpu(Cmp_eq)     -> Value.cmp_eq_u
+  | Op_cmpu(Cmp_ne)     -> Value.cmp_ne_u
+  | Op_cmpu(Cmp_gt)     -> Value.cmp_gt_u
+  | Op_cmpu(Cmp_ge)     -> Value.cmp_ge_u
+  | Op_cmpu(Cmp_lt)     -> Value.cmp_lt_u
+  | Op_cmpu(Cmp_le)     -> Value.cmp_le_u
+let rec eval_expression stack local_env memory = function
+  | Id x when LocalEnv.mem x local_env -> (LocalEnv.find x local_env,[])
+  | Id x -> error ("unknown local variable " ^ x ^ ".")
+  | Cst(c) -> (eval_constant stack memory c,[])
   | Op1(op,arg) ->
       let (v,l) = eval_expression global_env stack local_env memory arg in
       (eval_unop v op,l)
+    let (v,l) = eval_expression stack local_env memory arg in
+    (eval_unop op v,l)
   | Op2(op,arg1,arg2) ->
       let (v1,l1) = eval_expression global_env stack local_env memory arg1
       and (v2,l2) = eval_expression global_env stack local_env memory arg2 in
         (eval_binop v1 v2 op,l1@l2)
   | Mem(k,a) ->
       let (v,l) = (eval_expression global_env stack local_env memory a) in
         (Mem.load memory k v,l)
+    let (v1,l1) = eval_expression stack local_env memory arg1 in
+    let (v2,l2) = eval_expression stack local_env memory arg2 in
+    (eval_binop op v1 v2,l1@l2)
+  | Mem(q,a) ->
+    let (v,l) = eval_expression stack local_env memory a in
+    (Mem.loadq memory q (address_of_value v),l)
   | Cond(a1,a2,a3) ->
+      let (v1,l1) = eval_expression global_env stack local_env memory a1 in
+        if Value.is_true v1 then
+          let (v2,l2) = eval_expression global_env stack local_env memory a2 in
+            (v2,l1@l2)
+        else if Value.is_false v1 then
+          let (v2,l2) = eval_expression global_env stack local_env memory a3 in
+            (v2,l1@l2)
+        else assert false (*A boolean value is expected*)
+    let (v1,l1) = eval_expression stack local_env memory a1 in
+    if Value.is_true v1 then
+      let (v2,l2) = eval_expression stack local_env memory a2 in
+      (v2,l1@l2)
+    else
+      if Value.is_false v1 then
+        let (v3,l3) = eval_expression stack local_env memory a3 in
+        (v3,l1@l3)
+      else error "undefined conditional value."
   | Exp_cost(lbl,e) ->
+      let (v,l) = eval_expression global_env stack local_env memory e in
+        (v,l@[lbl])
+    let (v,l) = eval_expression stack local_env memory e in
+    (v,l@[lbl])
+let eval_exprlist sp lenv mem es =
+  let f (vs, cost_lbls) e =
+    let (v, cost_lbls') = eval_expression sp lenv mem e in
+    (vs @ [v], cost_lbls @ cost_lbls') in
+  List.fold_left f ([], []) es
 (* State transition *)
 …
     | Some(v) -> v
+(*FIXME To move in AST*)
+let string_of_sig sign =
+  let rec tmp = function
+    | [] -> ""
+    | Sig_int::l -> "int "^(tmp l)
+    | Sig_float::l -> "float "^(tmp l)
+    | Sig_ptr::l -> "ptr "^(tmp l)
+  in
+    match sign.res with
+      | Type_void -> (tmp sign.args)^" -> void"
+      | Type_ret Sig_int ->(tmp sign.args)^" -> int"
+      | Type_ret Sig_float ->(tmp sign.args)^" -> float"
+      | Type_ret Sig_ptr ->(tmp sign.args)^" -> ptr"
+let call_state global_env sigma e m a1 params sgn cont =
+  let (f,l) = eval_expression global_env sigma e m a1 in
+    match funct global_env f with
+      | F_int(fi) ->
+          if fi.f_sig = sgn then (
+            let tmp = List.map (eval_expression global_env sigma e m) params in
+              (State_call(F_int(fi),(List.map fst tmp),cont,m),
+               l@(List.flatten (List.map snd tmp)))
+          ) else (
+            Printf.eprintf "Error: signature (%s) different from (%s) \n"
+              (string_of_sig fi.f_sig)
+              (string_of_sig sgn);
+            assert false) (*Signatures mismatche*)
+      | F_ext(fe) ->
+          if fe.ef_sig = sgn then (
+          let tmp = List.map (eval_expression global_env sigma e m) params in
+            (State_call(F_ext(fe), (List.map fst tmp) ,cont,m),
+             l@(List.flatten (List.map snd tmp)))
+           ) else (
+             Printf.eprintf "Error: signature (%s) different from (%s) \n"
+               (string_of_sig fe.ef_sig)
+               (string_of_sig sgn);
+             assert false) (*Signatures mismatche*)
+let interpret_external f v k m =
+  try match f.ef_tag with
+    | "scan_int" ->
+        let res = Value.of_int (int_of_string (read_line ())) in
+          State_return (res, k, m)
+    | "print_int" ->
+        Printf.printf "%d" (Value.to_int (List.hd v)) ;
+        State_return (Value.zero, k, m)
+    | "print_intln" ->
+        Printf.printf "%d\n" (Value.to_int (List.hd v)) ;
+        State_return (Value.zero, k, m)
+    | "alloc" | "malloc" ->
+        let (m',vv) = Mem.alloc m (Value.to_int (List.hd v)) in
+          State_return (vv, k, m')
+    | "exit"  ->
+        State_return (List.hd v,Ct_stop,m)
+    | s ->
+        Printf.eprintf "Error: unknown external function: %s\n" s;
+        assert false (*Unknown external function*)
+  with
+      Failure _ -> assert false (*Wrong number of arguments*)
+let state_transition state global_env = match state with
+    (* Transition semantics for Cminor, part 1: statements *)
+    State_regular(f,St_skip,Ct_cont(s,k),sigma,e,m) ->
+      (State_regular(f, s, k, sigma, e, m),[])
+  | State_regular(f,St_skip,Ct_endblock(k),sigma,e,m) ->
+      (State_regular(f, St_skip, k, sigma, e, m),[])
+  | State_regular(f,St_assign(str,exp),k,sigma,e,m) ->
+      let (v,l) = eval_expression global_env sigma e m exp in
+        set_local_value e str v;
+        (State_regular(f, St_skip, k, sigma, e, m),l)
+  | State_regular(f,St_store(q,a1,a2),k,sigma,e,m) ->
+      let (v1,l1) = eval_expression global_env sigma e m a1 in
+      let (v2,l2) = eval_expression global_env sigma e m a2 in
+        (State_regular(f, St_skip, k, sigma, e, Mem.store m q v1 v2),l1@l2)
+  | State_regular(f,St_seq(s1,s2),k,sigma,e,m) ->
+      (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
+  | State_regular(f,St_ifthenelse(exp,s1,s2),k,sigma,e,m) ->
+      let (v,l) = eval_expression global_env sigma e m exp in
+        if Value.is_true v then (State_regular(f,s1,k,sigma,e,m),l)
+        else if Value.is_false v then (State_regular(f,s2,k,sigma,e,m),l)
+        else (
+          Printf.eprintf "Error: %s is not a boolean.\n" (Value.to_string v);
+          assert false (*boolean value expected*))
+  | State_regular(f,St_loop(s),k,sigma,e,m) ->
+      (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
+  | State_regular(f,St_block(s),k,sigma,e,m) ->
+      (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
+  | State_regular(f,St_exit(n),Ct_cont(s,k),sigma,e,m) ->
+      (State_regular(f,(St_exit n),k,sigma,e,m),[])
+  | State_regular(f,St_exit(n),Ct_endblock(k),sigma,e,m) when n=0 ->
+      (State_regular(f,St_skip,k,sigma,e,m),[])
+  | State_regular(f,St_exit(n),Ct_endblock(k),sigma,e,m) when (n>0) ->
+      (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
+  | State_regular(f,St_switch(exp,lst,def),k,sigma,e,m) ->
+      let (v,l) = eval_expression global_env sigma e m exp in
+        (try (State_regular
+                (f, St_exit (List.assoc (Value.to_int v) lst),k, sigma, e, m),l)
+         with Not_found ->
+           (State_regular (f, St_exit def, k, sigma, e, m),l) )
+  | State_regular(f,St_label(_,s),k,sigma,e,m) ->
+      (State_regular(f,s,k,sigma,e,m),[])
+  | State_regular(f,St_cost(lbl,s),k,sigma,e,m) ->
+      (State_regular(f,s,k,sigma,e,m),[lbl])
+  | State_regular(f,St_goto(lbl),k,sigma,e,m) ->
+      let (s2,k2) = findlabel lbl f.f_body (callcont k)
+      in (State_regular(f,s2,k2,sigma,e,m),[])
+  (* Transition semantics for Cminor, part 2:
+  * functions, initial states, final states *)
+  | State_regular(f,St_call(id,a1,params,sgn),k,sigma,e,m) ->
+      call_state global_env sigma e m a1 params sgn (Ct_returnto(id,f,sigma,e,k))
+  | State_regular(f,St_tailcall(a1,params,sgn),k,sigma,e,m) ->
+      call_state global_env sigma e m a1 params sgn (callcont k)
+  | State_regular(f,St_skip,Ct_returnto(p1,p2,p3,p4,p5),sigma,e,m)
+      when f.f_sig.res = Type_void ->
+      (State_return (Value.undef,Ct_returnto(p1,p2,p3,p4,p5),Mem.free m sigma),[])
+  | State_regular(f,St_skip,Ct_stop,sigma,e,m) when f.f_sig.res = Type_void ->
+      (State_return (Value.undef,Ct_stop,Mem.free m sigma),[])
+  | State_regular(f,St_return(_),k,sigma,e,m)  when f.f_sig.res = Type_void ->
+      (State_return (Value.undef,callcont k,Mem.free m sigma),[])
+  | State_regular(f,St_return(Some(a)),k,sigma,e,m)
+      when f.f_sig.res != Type_void ->
+      let (v,l) = eval_expression global_env sigma e m a in
+let call_state sigma e m f params cont =
+  let (addr,l1) = eval_expression sigma e m f in
+  let fun_def = Mem.find_fun_def m (address_of_value addr) in
+  let (args,l2) = eval_exprlist sigma e m params in
+  (State_call(fun_def,args,cont,m),l1@l2)
+let eval_stmt f k sigma e m s = match s, k with
+  | St_skip,Ct_cont(s,k) -> (State_regular(f, s, k, sigma, e, m),[])
+  | St_skip,Ct_endblock(k) -> (State_regular(f, St_skip, k, sigma, e, m),[])
+  | St_skip, (Ct_returnto _ as k) ->
+    (State_return (Value.undef,k,Mem.free m sigma),[])
+  | St_skip,Ct_stop ->
+    (State_return (Value.undef,Ct_stop,Mem.free m sigma),[])
+  | St_assign(x,exp),_ ->
+    let (v,l) = eval_expression sigma e m exp in
+    let e = LocalEnv.add x v e in
+    (State_regular(f, St_skip, k, sigma, e, m),l)
+  | St_store(q,a1,a2),_ ->
+    let (v1,l1) = eval_expression sigma e m a1 in
+    let (v2,l2) = eval_expression sigma e m a2 in
+    let m = Mem.storeq m q (address_of_value v1) v2 in
+    (State_regular(f, St_skip, k, sigma, e, m),l1@l2)
+  | St_call(xopt,f',params,_),_ ->
+    call_state sigma e m f' params (Ct_returnto(xopt,f,sigma,e,k))
+  | St_tailcall(f',params,_),_ ->
+    call_state sigma e m f' params (callcont k)
+  | St_seq(s1,s2),_ -> (State_regular(f, s1, Ct_cont(s2, k), sigma, e, m),[])
+  | St_ifthenelse(exp,s1,s2),_ ->
+    let (v,l) = eval_expression sigma e m exp in
+    let next_stmt =
+      if Value.is_true v then s1
+      else
+        if Value.is_false v then s2
+        else error "undefined conditional value." in
+      (State_regular(f,next_stmt,k,sigma,e,m),l)
+  | St_loop(s),_ -> (State_regular(f,s,Ct_cont((St_loop s),k),sigma,e,m),[])
+  | St_block(s),_ -> (State_regular(f,s,(Ct_endblock k),sigma,e,m),[])
+  | St_exit(n),Ct_cont(s,k) -> (State_regular(f,(St_exit n),k,sigma,e,m),[])
+  | St_exit(0),Ct_endblock(k) -> (State_regular(f,St_skip,k,sigma,e,m),[])
+  | St_exit(n),Ct_endblock(k) ->
+    (State_regular(f,(St_exit (n-1)),k,sigma,e,m),[])
+  | St_label(_,s),_ -> (State_regular(f,s,k,sigma,e,m),[])
+  | St_goto(lbl),_ ->
+    let (s2,k2) = findlabel lbl f.f_body (callcont k) in
+    (State_regular(f,s2,k2,sigma,e,m),[])
+  | St_switch(exp,lst,def),_ ->
+    let (v,l) = eval_expression sigma e m exp in
+    if Value.is_int v then
+      try
+        let i = Value.to_int v in
+        let nb_exit =
+          if List.mem_assoc i lst then List.assoc i lst
+          else def in
+        (State_regular(f, St_exit nb_exit,k, sigma, e, m),l)
+      with _ -> error "int value too big."
+    else error "undefined switch value."
+  | St_return(None),_ ->
+    (State_return (Value.undef,callcont k,Mem.free m sigma),[])
+  | St_return(Some(a)),_ ->
+      let (v,l) = eval_expression sig

Context Navigation

Legend:

Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml

Deliverables/D2.2/8051/src/ASM/I8051.ml

Deliverables/D2.2/8051/src/ASM/I8051.mli

Deliverables/D2.2/8051/src/ERTL/ERTL.mli

Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

Deliverables/D2.2/8051/src/LIN/LINInterpret.ml

Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

Deliverables/D2.2/8051/src/RTL/RTL.mli

Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli

Deliverables/D2.2/8051/src/RTLabs/RTLabsInterpret.ml

Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.mli

Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

Deliverables/D2.2/8051/src/acc.ml

Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml

Deliverables/D2.2/8051/src/clight/clightCasts.ml

Deliverables/D2.2/8051/src/clight/clightCasts.mli

Deliverables/D2.2/8051/src/clight/clightFold.mli

Deliverables/D2.2/8051/src/clight/clightInterpret.ml

Deliverables/D2.2/8051/src/clight/clightInterpret.mli

Deliverables/D2.2/8051/src/clight/clightParser.ml

Deliverables/D2.2/8051/src/clight/clightToCminor.ml

Deliverables/D2.2/8051/src/cminor/cminor.mli

Deliverables/D2.2/8051/src/cminor/cminorAnnotator.ml

Deliverables/D2.2/8051/src/cminor/cminorInterpret.ml