Ignore:
Timestamp:
Apr 4, 2011, 5:18:15 PM (9 years ago)
Author:
ayache
Message:

New memory model and bug fixes in 8051 branch. Added primitive operations in interpreters from Clight to LIN.

Location:
Deliverables/D2.2/8051/src/clight
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/clight/clight32ToClight8.ml

    r619 r740  
    203203
    204204let translate p =
     205  (* TODO: restore below *)
     206(*
    205207  let (p, unop_assoc, binop_assoc) = Runtime.add p in
    206208  let p = ClightCasts.simplify p in
     
    212214  (* TODO: do the translation *)
    213215  p
     216*)
     217  ClightCasts.simplify p
  • Deliverables/D2.2/8051/src/clight/clightCasts.ml

    r624 r740  
    33
    44    Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char]
    5     will be transformed into [x + y]. *)
     5    will be transformed into [x + y]. Primitive operations are thus supposed to
     6    be polymorphic, but working only on homogene types. *)
    67
    78let f_ctype ctype _ = ctype
    89
     10(*
    911let f_expr = ClightFold.expr_fill_subs
    1012
     
    6567                  (Clight.Expr (_,
    6668                                Clight.Tint (Clight.I8, signedness2)) as e1)),
    67                _)),
     69               _)),sub_ctypes_res sub_exprs_res
    6870         _) :: _ when signedness1 = signedness2 ->
    6971      Clight.Ebinop (binop,
     
    7274                     e1)
    7375    | _ -> ClightFold.expr_descr_fill_subs e sub_ctypes_res sub_exprs_res
     76*)
    7477
    75 let f_statement = ClightFold.statement_fill_subs
     78let simplify_exp ctype_opt e = e (* TODO *)
     79
     80let f_expr e _ _ = e
     81
     82let f_expr_descr e _ _ =  e
     83
     84let f_statement stmt _ sub_stmts_res =
     85  let sub_exprs = match stmt with
     86    | _ -> assert false in
     87  ClightFold.statement_fill_subs stmt sub_exprs sub_stmts_res
    7688
    7789let simplify_stmt = ClightFold.statement f_ctype f_expr f_expr_descr f_statement
     
    8597  (id, fundef')
    8698
    87 let simplify p =
     99let simplify p = p
     100(* (* TODO: below *)
    88101  { p with Clight.prog_funct = List.map simplify_funct p.Clight.prog_funct }
     102*)
  • Deliverables/D2.2/8051/src/clight/clightCasts.mli

    r619 r740  
    33
    44    Example: [(char) ((int)x + (int)y)] where [x] and [y] are of type [char]
    5     will be transformed into [x + y]. *)
     5    will be transformed into [x + y]. Primitive operations are thus supposed to
     6    be polymorphic, but working only on homogene types. *)
    67
    78val simplify : Clight.program -> Clight.program
  • Deliverables/D2.2/8051/src/clight/clightFold.mli

    r619 r740  
    77val ctype : (Clight.ctype -> 'a list -> 'a) -> Clight.ctype -> 'a
    88
    9 val expr : (Clight.expr_descr -> 'a list -> 'b list -> 'c) ->
    10            (Clight.ctype -> 'a list -> 'a) ->
    11            (Clight.expr -> 'c list -> 'a list -> 'b) ->
    12            Clight.expr ->
    13            'b
     9val expr_fill_subs :
     10  Clight.expr -> Clight.ctype list -> Clight.expr_descr list ->
     11  Clight.expr
    1412
    15 val expr_descr : (Clight.ctype -> 'a list -> 'a) ->
    16                  (Clight.expr -> 'b list -> 'a list -> 'c) ->
    17                  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
    18                  Clight.expr_descr ->
    19                  'b
     13val expr :
     14  (Clight.ctype -> 'a list -> 'a) ->
     15  (Clight.expr -> 'a list -> 'b list -> 'c) ->
     16  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
     17  Clight.expr ->
     18  'c
    2019
    21 (*
    22 (* In [statement_left f_expr f_stmt stmt], [f_stmt]'s second argument is the
    23    list of [expression_left f_expr]'s results on [stmt]'s sub-expressions, and
    24    [f_stmt]'s third argument is the list of [statement_left]'s results
    25    on [stmt]'s sub-statements. The results are computed from left to right
    26    following their appearance order in the [Cminor.statement] type. *)
     20val expr_descr_fill_subs :
     21  Clight.expr_descr -> Clight.ctype list -> Clight.expr list ->
     22  Clight.expr_descr
    2723
    28 val statement_left : (Cminor.expression -> 'a list -> 'a) ->
    29                      (Cminor.statement -> 'a list -> 'b list -> 'b) ->
    30                      Cminor.statement ->
    31                      'b
    32 *)
     24val expr_descr :
     25  (Clight.ctype -> 'a list -> 'a) ->
     26  (Clight.expr -> 'a list -> 'b list -> 'c) ->
     27  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
     28  Clight.expr_descr ->
     29  'b
     30
     31val statement_fill_subs :
     32  Clight.statement -> Clight.expr list -> Clight.statement list ->
     33  Clight.statement
     34
     35val statement :
     36  (Clight.ctype -> 'a list -> 'a) ->
     37  (Clight.expr -> 'a list -> 'b list -> 'c) ->
     38  (Clight.expr_descr -> 'a list -> 'c list -> 'b) ->
     39  (Clight.statement -> 'c list -> 'd list -> 'd) ->
     40  Clight.statement ->
     41  'd
  • Deliverables/D2.2/8051/src/clight/clightInterpret.ml

    r630 r740  
    11module Mem = Driver.ClightMemory
    22module Value = Driver.ClightMemory.Value
    3 module Valtbl = Hashtbl.Make(Value)
     3module LocalEnv = Map.Make(String)
     4type localEnv = Value.address LocalEnv.t
     5type memory = Clight.fundef Mem.memory
    46
    57open Clight
    68open AST
    79
    8 let warning msg = print_string ("Warning: "^msg^" (clightInterpret.ml)\n")
    9 
    10 type localEnv = (ident,Value.t) Hashtbl.t
     10
     11let error_prefix = "Clight interpret"
     12let error s = Error.global_error error_prefix s
     13let warning s = Error.warning error_prefix s
     14let error_float () = error "float not supported."
     15
     16
     17(* Helpers *)
     18
     19let value_of_address = List.hd
     20let address_of_value v = [v]
     21
     22
     23(* State of execution *)
    1124
    1225type continuation =
     
    1831  | Kfor3 of expr*statement*statement*continuation
    1932  | Kswitch of continuation
    20   | Kcall of (Value.t*ctype) option*cfunction*localEnv*continuation
     33  | Kcall of (Value.address*ctype) option*cfunction*localEnv*continuation
    2134
    2235type state =
    23   | State of cfunction*statement*continuation*localEnv*(fundef Mem.memory)
    24   | Callstate of fundef*Value.t list*continuation*(fundef Mem.memory)
    25   | Returnstate of Value.t*continuation*(fundef Mem.memory)
    26 
    27 (* ctype functions *)
    28 
    29 let rec sizeof = function
    30   | Tvoid               -> 0
    31   | Tint (I8,_)         -> 1
    32   | Tint (I16,_)        -> 2
    33   | Tint (I32,_)        -> 4
    34   | Tfloat _            -> assert false (* Not supported *)
    35   | Tpointer _          -> Mem.ptr_size
    36   | Tarray (t,s)        -> s*(sizeof t)                   
    37   | Tfunction (_,_)     -> assert false (* Not supported *)
    38   | Tstruct (_,lst)     ->
    39       List.fold_left
    40         (fun n (_,ty) -> (fun a b -> a+b) n (sizeof ty)) 0 lst
    41   | Tunion (_,lst)      ->
    42       List.fold_left
    43         (fun n (_,ty)   ->
    44            let sz = (sizeof ty) in (if n>sz then n else sz)
    45         ) 0 lst
    46   | Tcomp_ptr _         -> Mem.ptr_size
    47 
    48 let rec mq_of_ty = function
    49   | Tvoid               -> assert false
    50   | Tint (I8,Signed)    -> Memory.MQ_int8signed
    51   | Tint (I8,Unsigned)  -> Memory.MQ_int8unsigned
    52   | Tint (I16,Signed)   -> Memory.MQ_int16signed
    53   | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned
    54   (*FIXME MQ_int32 : signed or unsigned ?*)
    55   | Tint (I32,Signed)   -> Memory.MQ_int32
    56   | Tint (I32,Unsigned) -> Memory.MQ_int32
    57   | Tfloat _            -> assert false (* Not supported *)
    58   | Tpointer _          -> Mem.mq_of_ptr
    59   | Tarray (c,s)        -> Mem.mq_of_ptr
    60   | Tfunction (_,_)     -> assert false (* Not supported *)
    61   | Tstruct (_,_)       -> Mem.mq_of_ptr
    62   | Tunion (_,_)        -> Mem.mq_of_ptr
    63   | Tcomp_ptr _         -> Mem.mq_of_ptr
    64 
    65 (* Pretty printing for Clight states *)
    66 
    67 let string_s = function
    68   | Sskip                               -> "skip"
    69   | Sassign (Expr (Evar id,_),_)        -> "assign "^id
    70   | Sassign (_,_)                       -> "assign"
    71   | Scall (_,_,_)                       -> "call"
    72   | Ssequence (_,_)                     -> "seq"
    73   | Sifthenelse (_,_,_)                 -> "ifthenelse"
    74   | Swhile (_,_)                        -> "while"
    75   | Sdowhile (_,_)                      -> "dowhile"
    76   | Sfor (_,_,_,_)                      -> "for"
    77   | Sbreak                              -> "break"
    78   | Scontinue                           -> "continue"
    79   | Sreturn _                           -> "return"
    80   | Sswitch (_,_)                       -> "switch"
    81   | Slabel (_,_)                        -> "label"
    82   | Sgoto _                             -> "goto"
    83   | Scost (_,_)                         -> "cost"
    84 
    85 let string_f = function
    86   | Internal _          -> "func"
    87   | External (id,_,_)   -> id
    88 
    89 let string_c = function
    90   | Kstop               -> "stop"
    91   | Kseq (_,_)          -> "seq"
    92   | Kwhile (_,_,_)      -> "while"
    93   | Kdowhile (_,_,_)    -> "dowhile"
    94   | Kfor2 (_,_,_,_)     -> "for2"
    95   | Kfor3 (_,_,_,_)     -> "for3"
    96   | Kswitch _           -> "switch"
    97   | Kcall (_,_,_,_)     -> "call"
    98 
    99 let string_of_state = function
    100   | State (_,s,c,_,_) -> "Regular("^(string_s s)^","^(string_c c)^")"
    101   | Callstate (f,_,c,_) -> "Call("^(string_f f)^","^(string_c c)^")"
    102   | Returnstate (v,c,_) ->
    103       "Return("^(Value.to_string v)^","^(string_c c)^")"
    104 
    105 (* Global and local environment management *)
    106 
    107 let find_funct_id g id =
    108   try Valtbl.find (snd g) (Hashtbl.find (fst g) id)
    109   with Not_found -> assert false
    110 
    111 let find_funct g v =
    112   try Valtbl.find (snd g) (fst v)
    113   with Not_found -> assert false
    114 
    115 let find_symbol globalenv localenv id =
    116   try Hashtbl.find localenv id
    117   with Not_found -> (
    118     try Hashtbl.find (fst globalenv) id
    119     with Not_found ->
    120      Printf.eprintf "Error: cannot find symbol %s\n" id;
    121       assert false
    122   )
     36  | State of cfunction*statement*continuation*localEnv*memory
     37  | Callstate of fundef*Value.t list*continuation*memory
     38  | Returnstate of Value.t*continuation*memory
     39
     40let string_of_unop = function
     41  | Onotbool -> "!"
     42  | Onotint -> "~"
     43  | Oneg -> "-"
     44
     45let string_of_binop = function
     46  | Oadd -> "+"
     47  | Osub -> "-"
     48  | Omul -> "*"
     49  | Odiv -> "/"
     50  | Omod -> "%"
     51  | Oand -> "&"
     52  | Oor  -> "|"
     53  | Oxor -> "^"
     54  | Oshl -> "<<"
     55  | Oshr -> ">>"
     56  | Oeq -> "=="
     57  | One -> "!="
     58  | Olt -> "<"
     59  | Ogt -> ">"
     60  | Ole -> "<="
     61  | Oge -> ">="
     62
     63let string_of_signedness = function
     64  | Signed -> "signed"
     65  | Unsigned -> "unsigned"
     66
     67let string_of_sized_int = function
     68  | I8 -> "char"
     69  | I16 -> "short"
     70  | I32 -> "int"
     71
     72let rec string_of_ctype = function
     73  | Tvoid -> "void"
     74  | Tint (size, sign) ->
     75    (string_of_signedness sign) ^ " " ^ (string_of_sized_int size)
     76  | Tfloat _ -> error_float ()
     77  | Tpointer ty -> (string_of_ctype ty) ^ "*"
     78  | Tarray (ty, _) -> (string_of_ctype ty) ^ "[]"
     79  | Tfunction _ -> assert false (* do not cast to a function type *)
     80  | Tstruct (id, _)
     81  | Tunion (id, _) -> id
     82  | Tcomp_ptr id -> id ^ "*"
     83
     84let rec string_of_expr (Expr (e, _)) = string_of_expr_descr e
     85and string_of_expr_descr = function
     86  | Econst_int i -> string_of_int i
     87  | Econst_float _ -> error_float ()
     88  | Evar x -> x
     89  | Ederef e -> "*(" ^ (string_of_expr e) ^ ")"
     90  | Eaddrof e -> "&(" ^ (string_of_expr e) ^ ")"
     91  | Eunop (unop, e) -> (string_of_unop unop) ^ "(" ^ (string_of_expr e) ^ ")"
     92  | Ebinop (binop, e1, e2) ->
     93    "(" ^ (string_of_expr e1) ^ ")" ^ (string_of_binop binop) ^
     94    "(" ^ (string_of_expr e2) ^ ")"
     95  | Ecast (ty, e) ->
     96    "(" ^ (string_of_ctype ty) ^ ") (" ^ (string_of_expr e) ^ ")"
     97  | Econdition (e1, e2, e3) ->
     98    "(" ^ (string_of_expr e1) ^ ") ? (" ^ (string_of_expr e2) ^
     99    ") : (" ^ (string_of_expr e3) ^ ")"
     100  | Eandbool (e1, e2) ->
     101    "(" ^ (string_of_expr e1) ^ ") && (" ^ (string_of_expr e2) ^ ")"
     102  | Eorbool (e1, e2) ->
     103    "(" ^ (string_of_expr e1) ^ ") || (" ^ (string_of_expr e2) ^ ")"
     104  | Esizeof ty -> "sizeof(" ^ (string_of_ctype ty) ^ ")"
     105  | Efield (e, field) -> "(" ^ (string_of_expr e) ^ ")." ^ field
     106  | Ecost (cost_lbl, e) -> "/* " ^ cost_lbl ^ " */ " ^ (string_of_expr e)
     107  | Ecall (f, arg, e) ->
     108    "(" ^ f ^ "(" ^ (string_of_expr arg) ^ "), " ^ (string_of_expr e) ^ ")"
     109
     110let string_of_args args =
     111  "(" ^ (MiscPottier.string_of_list ", " string_of_expr args) ^ ")"
     112
     113let rec string_of_statement = function
     114  | Sskip -> "skip"
     115  | Sassign (e1, e2) -> (string_of_expr e1) ^ " = " ^ (string_of_expr e2)
     116  | Scall (None, f, args) -> (string_of_expr f) ^ (string_of_args args)
     117  | Scall (Some e, f, args) ->
     118    (string_of_expr e) ^ " = " ^ (string_of_expr f) ^ (string_of_args args)
     119  | Ssequence _ -> "sequence"
     120  | Sifthenelse (e, _, _) -> "if (" ^ (string_of_expr e) ^ ")"
     121  | Swhile (e, _) -> "while (" ^ (string_of_expr e) ^ ")"
     122  | Sdowhile _ -> "dowhile"
     123  | Sfor (s, _, _, _) -> "for (" ^ (string_of_statement s) ^ "; ...)"
     124  | Sbreak -> "break"
     125  | Scontinue -> "continue"
     126  | Sreturn None -> "return"
     127  | Sreturn (Some e) -> "return (" ^ (string_of_expr e) ^ ")"
     128  | Sswitch (e, _) -> "switch (" ^ (string_of_expr e) ^ ")"
     129  | Slabel (lbl, _) -> "label " ^ lbl
     130  | Sgoto lbl -> "goto " ^ lbl
     131  | Scost (lbl, _) -> "cost " ^ lbl
     132
     133let string_of_local_env lenv =
     134  let f x addr s =
     135    s ^ x ^ " = " ^ (Value.to_string (value_of_address addr)) ^ "  " in
     136  LocalEnv.fold f lenv ""
     137
     138let print_state = function
     139  | State (_, stmt, _, lenv, mem) ->
     140    Printf.printf "Local environment:\n%s\n\nMemory:%s\nRegular state: %s\n\n%!"
     141      (string_of_local_env lenv)
     142      (Mem.to_string mem)
     143      (string_of_statement stmt)
     144  | Callstate (_, args, _, mem) ->
     145    Printf.printf "Memory:%s\nCall state\n\nArguments:\n%s\n\n%!"
     146      (Mem.to_string mem)
     147      (MiscPottier.string_of_list " " Value.to_string args)
     148  | Returnstate (v, _, mem) ->
     149    Printf.printf "Memory:%s\nReturn state: %s\n\n%!"
     150      (Mem.to_string mem)
     151      (Value.to_string v)
     152
    123153
    124154(* Continuations and labels *)
    125155
    126156let rec call_cont = function
    127   | Kseq (_,k)          -> call_cont k
    128   | Kwhile (_,_,k)      -> call_cont k
    129   | Kdowhile (_,_,k)    -> call_cont k
    130   | Kfor2 (_,_,_,k)     -> call_cont k
    131   | Kfor3 (_,_,_,k)     -> call_cont k
    132   | Kswitch k           -> call_cont k
    133   | k                   -> k
    134 
    135 let is_call_cont = function
    136   | Kstop | Kcall (_,_,_,_) -> true
    137   | _ -> false
     157  | Kseq (_,k) | Kwhile (_,_,k) | Kdowhile (_,_,k)
     158  | Kfor2 (_,_,_,k) | Kfor3 (_,_,_,k) | Kswitch k -> call_cont k
     159  | k -> k
    138160
    139161let rec seq_of_labeled_statement = function
    140162  | LSdefault s -> s
    141163  | LScase (c,s,sl') -> Ssequence (s,(seq_of_labeled_statement sl'))
     164
     165let rec find_label1 lbl s k = match s with
     166   | Ssequence (s1,s2) ->
     167      (match find_label1 lbl s1 (Kseq (s2,k)) with
     168      | Some sk -> Some sk
     169      | None -> find_label1 lbl s2 k
     170      )
     171  | Sifthenelse (a,s1,s2) ->
     172      (match find_label1 lbl s1 k with
     173      | Some sk -> Some sk
     174      | None -> find_label1 lbl s2 k
     175      )
     176  | Swhile (a,s1) -> find_label1 lbl s1 (Kwhile(a,s1,k))
     177  | Sdowhile (a,s1) -> find_label1 lbl s1 (Kdowhile(a,s1,k))
     178  | Sfor (a1,a2,a3,s1) ->
     179      (match find_label1 lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
     180      | Some sk -> Some sk
     181      | None ->
     182          (match find_label1 lbl s1 (Kfor2(a2,a3,s1,k)) with
     183          | Some sk -> Some sk
     184          | None -> find_label1 lbl a3 (Kfor3(a2,a3,s1,k))
     185          ))
     186  | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
     187  | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label1 lbl s' k
     188  | Scost (_,s') -> find_label1 lbl s' k
     189  | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak
     190  | Scontinue | Sreturn _ | Sgoto _ -> None
     191           
     192and find_label_ls lbl sl k =  match sl with
     193  | LSdefault s -> find_label1 lbl s k
     194  | LScase (_,s,sl') ->
     195      (match find_label1 lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
     196      | Some sk -> Some sk
     197      | None -> find_label_ls lbl sl' k
     198      )
     199
     200let find_label lbl s k = match find_label1 lbl s k with
     201  | Some res -> res
     202  | _ -> assert false (* should be impossible *)
    142203
    143204let rec select_switch i = function
     
    146207  | LScase (_,_,sl') -> select_switch i sl'
    147208
    148 let rec find_label lbl s k = match s with
    149    | Ssequence (s1,s2) ->
    150       (match find_label lbl s1 (Kseq (s2,k)) with
    151       | Some sk -> Some sk
    152       | None -> find_label lbl s2 k
    153       )
    154   | Sifthenelse (a,s1,s2) ->
    155       (match find_label lbl s1 k with
    156       | Some sk -> Some sk
    157       | None -> find_label lbl s2 k
    158       )
    159   | Swhile (a,s1) -> find_label lbl s1 (Kwhile(a,s1,k))
    160   | Sdowhile (a,s1) -> find_label lbl s1 (Kdowhile(a,s1,k))
    161   | Sfor (a1,a2,a3,s1) ->
    162       (match find_label lbl a1 (Kseq ((Sfor(Sskip,a2,a3,s1)),k)) with
    163       | Some sk -> Some sk
    164       | None ->
    165           (match find_label lbl s1 (Kfor2(a2,a3,s1,k)) with
    166           | Some sk -> Some sk
    167           | None -> find_label lbl a3 (Kfor3(a2,a3,s1,k))
    168           ))
    169   | Sswitch (e,sl) -> find_label_ls lbl sl (Kswitch k)
    170   | Slabel (lbl',s') -> if lbl=lbl' then Some(s', k) else find_label lbl s' k
    171   | Scost (_,s') -> find_label lbl s' k
    172   | Sskip | Sassign (_,_) | Scall (_,_,_) | Sbreak
    173   | Scontinue | Sreturn _ | Sgoto _ -> None
    174            
    175 and find_label_ls lbl sl k =  match sl with
    176   | LSdefault s -> find_label lbl s k
    177   | LScase (_,s,sl') ->
    178       (match find_label lbl s (Kseq((seq_of_labeled_statement sl'),k)) with
    179       | Some sk -> Some sk
    180       | None -> find_label_ls lbl sl' k
    181       )
     209
     210(* ctype functions *)
     211
     212let rec sizeof = function
     213  | Tint (I8, _)  -> 1
     214  | Tint (I16, _) -> 2
     215  | Tint (I32, _) -> 4
     216  | Tfloat _ -> error_float ()
     217  | Tcomp_ptr _ -> Mem.ptr_size
     218  | Tpointer _ -> Mem.ptr_size
     219  | Tarray (ty, n) -> n * (sizeof ty)
     220  | Tstruct (_, fields) ->
     221    let sizes = List.map sizeof (List.map snd fields) in
     222    snd (Mem.align 0 sizes)
     223  | Tunion (_, fields) ->
     224    MiscPottier.max_list (List.map sizeof (List.map snd fields))
     225  | _ -> assert false (* do not use on these arguments *)
     226
     227let size_of_ctype = function
     228  | Tint (I8, _)  -> 1
     229  | Tint (I16, _) -> 2
     230  | Tint (I32, _) -> 4
     231  | Tfloat _ -> error_float ()
     232  | Tcomp_ptr _
     233  | Tpointer _
     234  | Tarray _
     235  | Tstruct _
     236  | Tunion _ -> Mem.ptr_size
     237  | _ -> assert false (* do not use on these arguments *)
     238
     239let is_function_type = function
     240  | Tfunction _ -> true
     241  | _ -> false
     242
     243let is_array_type = function
     244  | Tarray _ -> true
     245  | _ -> false
     246
     247let is_complex_type = function
     248  | Tstruct _ | Tunion _ -> true
     249  | _ -> false
     250
     251let is_big_type t = (is_array_type t) || (is_complex_type t)
     252
     253let dest_type = function
     254  | Tpointer ty | Tarray (ty, _) -> ty
     255  | _ -> assert false (* do not use on these arguments *)
     256
     257
     258(* Global and local environment management *)
     259
     260let find_local x lenv =
     261  if LocalEnv.mem x lenv then LocalEnv.find x lenv
     262  else error ("Unknown local variable " ^ x ^ ".")
     263
     264let find_global x mem =
     265  if Mem.mem_global mem x then Mem.find_global mem x
     266  else error ("Unknown global variable " ^ x ^ ".")
     267
     268let find_symbol lenv mem x =
     269  if LocalEnv.mem x lenv then LocalEnv.find x lenv
     270  else
     271    if Mem.mem_global mem x then Mem.find_global mem x
     272    else error ("Unknown variable " ^ x ^ ".")
     273
     274let find_fundef f mem =
     275  let addr = Mem.find_global mem f in
     276  Mem.find_fun_def mem addr
     277
    182278
    183279(* Interpret *)
    184280
    185 let is_int_type = function
    186   | Tint (_,_)    -> true
    187   | _ -> false
    188 let is_float_type = function
    189   | Tfloat _  -> true
    190   | _ -> false
    191 let is_pointer_type = function
    192   | Tpointer _ | Tarray (_,_) | Tstruct (_,_)
    193   | Tunion (_,_) | Tcomp_ptr _ -> true
    194   | _ -> false
    195 
    196 let eval_cast = function
    197   (* no cast *)
    198   | (e,a,b) when a=b                            -> e
     281let int_of_intsize = function
     282  | I8 -> 8
     283  | I16 -> 16
     284  | I32 -> 32
     285
     286let choose_cast signedness n m v =
     287  let f = match signedness with
     288    | Signed -> Value.sign_ext
     289    | Unsigned -> Value.zero_ext in
     290  f v n m
     291
     292let eval_cast = function
    199293  (* Cast Integer *)
    200   | (v,_,Tint(I8,Signed))                       -> Value.cast8signed v
    201   | (v,_,Tint(I8,Unsigned))                     -> Value.cast8unsigned v
    202   | (v,_,Tint(I16,Signed))                      -> Value.cast16signed v
    203   | (v,_,Tint(I16,Unsigned))                    -> Value.cast16unsigned v
    204   | (v,_,Tint(I32,Signed)) when Value.is_int v  -> v
    205   | (v,_,Tint(I32,Unsigned)) when Value.is_int v-> v (*FIXME*)
    206   (* Cast float*)
    207   | (v,_,Tfloat _)                              -> assert false(*Not supported*)
    208   (* Cast pointeur *)
    209   | (v,Tarray(_,_),Tpointer _)                  -> v
    210   | (v,Tpointer _,Tarray(_,_))                  -> v
    211   | (v,Tpointer _,Tpointer _)                   -> v
    212   | (v,Tarray (_,_),Tarray(_,_))                -> v
    213   | (v,Tstruct(a,b),Tpointer (Tstruct(c,d))) when a=c && b=d -> v (*FIXME is it correct ?*)
    214   | (v,Tpointer (Tstruct(a,b)),Tstruct(c,d)) when a=c && b=d -> v (*FIXME is it correct ?*)
    215   | (v,Tunion(a,b),Tpointer (Tunion(c,d))) when a=c && b=d -> v (*FIXME is it correct ?*)
    216   | (v,Tpointer (Tunion(a,b)),Tunion(c,d)) when a=c && b=d -> v (*FIXME is it correct ?*)
    217   (* error *)
    218   | (e,_,_)                                     ->
    219       warning "eval_cast";e (*Value.undef*)
    220 
    221 let eval_unop (v,t) = function 
    222   | Onotbool when is_int_type t -> Value.notbool v
    223   | Onotint when is_int_type t  -> Value.notint v
    224   | Oneg when is_int_type t     -> Value.negint v
    225   | Oneg when is_float_type t   -> assert false (*Not supported*)
    226   | _                           -> assert false (*Type error*)
    227 
    228 let get_subtype = function
    229   | Tarray(t,_) -> t
    230   | Tpointer t -> t
    231   | _ -> assert false (*Misuse of get_subtype*)
    232 
    233 let eval_add = function
    234   (*Integer*)
    235   | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 -> 
    236       let v = Value.add v1 v2 in
    237         (match t1 with
    238            | Tint(I8,Signed)    -> Value.cast8signed v
    239            | Tint(I8,Unsigned)  -> Value.cast8unsigned v
    240            | Tint(I16,Signed)   -> Value.cast16signed v
    241            | Tint(I16,Unsigned) -> Value.cast16unsigned v
    242            | Tint(I32,Signed)   -> v
    243            | Tint(I32,Unsigned) -> v (*FIXME*)
    244            | _                  -> assert false (*Prevented by is_int_type*))
    245   (*Float*)
    246   | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 ->
    247       assert false (*Not supported*)
    248   (*Pointer*)
    249   | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
    250       Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
    251   | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 ->
    252       Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
    253   (*Error*)
    254   | _ -> assert false (*Type error*)
    255 
    256 let eval_sub = function
    257   (*Integer*)
    258   | ((v1,t1) , (v2,t2)) when t1=t2 && is_int_type t1 ->
    259       let v = Value.sub v1 v2 in
    260         (match t1 with
    261            | Tint(I8,Signed)    -> Value.cast8signed v
    262            | Tint(I8,Unsigned)  -> Value.cast8unsigned v
    263            | Tint(I16,Signed)   -> Value.cast16signed v
    264            | Tint(I16,Unsigned) -> Value.cast16unsigned v
    265            | Tint(I32,Signed)   -> v
    266            | Tint(I32,Unsigned) -> v (*FIXME*)
    267            | _                  -> assert false (*Prevented by is_int_type*))
    268   (*Float*)
    269   | ((v1,t1) , (v2,t2)) when t1=t2 && is_float_type t1 ->
    270       assert false (*Not supported*)
    271   (*Pointer*)
    272   | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
    273       Value.sub v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
    274   (*Error*)
    275   | _ -> assert false (*Type error*)
    276 
    277 let eval_mul = function
    278   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 ->
    279       let v = Value.mul v1 v2 in
    280         (match t1 with
    281            | Tint(I8,Signed)    -> Value.cast8signed v
    282            | Tint(I8,Unsigned)  -> Value.cast8unsigned v
    283            | Tint(I16,Signed)   -> Value.cast16signed v
    284            | Tint(I16,Unsigned) -> Value.cast16unsigned v
    285            | Tint(I32,Signed)   -> v
    286            | Tint(I32,Unsigned) -> v (*FIXME*)
    287            | _                  -> assert false (*Prevented by is_int_type*))   
    288   | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 ->
    289       assert false (*Not supported*)
    290   | _ -> assert false (*Type error*)
    291 
    292 let eval_mod = function
    293   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 ->
    294       Value.modulo v1 v2
    295   | _ -> assert false (*Type error*)
    296 
    297 let eval_div = function
    298   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.div v1 v2
    299   | ((v1,t1),(v2,t2)) when t1=t2 && is_float_type t1 ->
    300       assert false (*Not supported*)
    301   | _ -> assert false (*Type error*)
    302 
    303 let eval_and = function
    304   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.and_op v1 v2
    305   | _ -> assert false (*Type error*)
    306 
    307 let eval_or = function
    308   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.or_op v1 v2
    309   | _ -> assert false (*Type error*)
    310 
    311 let eval_xor = function
    312   | ((v1,t1),(v2,t2)) when t1=t2 && is_int_type t1 -> Value.xor v1 v2
    313   | _ -> assert false (*Type error*)
    314 
    315 let eval_shl = function         
    316   | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shl v1 v2
    317   | _ -> assert false (*Type error*)
    318 
    319 let eval_shr = function         
    320   | ((v1,t1),(v2,t2)) when is_int_type t2 && is_int_type t1 -> Value.shr v1 v2
    321   | _ -> assert false (*Type error*)
    322 
    323 let eval_eq = function
    324   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_eq v1 v2
    325   | _ -> assert false (*Type error*)
    326            
    327 let eval_ne = function
    328   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ne v1 v2
    329   | _ -> assert false (*Type error*)
    330 
    331 let eval_lt = function
    332   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_lt v1 v2
    333   | _ -> assert false (*Type error*)
    334 
    335 let eval_gt = function
    336   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_gt v1 v2
    337   | _ -> assert false (*Type error*)
    338 
    339 let eval_le = function
    340   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_le v1 v2
    341   | _ -> assert false (*Type error*)
    342 
    343 let eval_ge = function
    344   | ((v1,t1),(v2,t2)) when t1=t2 -> Value.cmp_ge v1 v2
    345   | _ -> assert false (*Type error*)
    346 
    347 let eval_binop e1 e2 = function
    348   | Oadd -> eval_add (e1,e2)
    349   | Osub -> eval_sub (e1,e2)
    350   | Omul -> eval_mul (e1,e2)
    351   | Odiv -> eval_div (e1,e2)
    352   | Omod -> eval_mod (e1,e2)
    353   | Oand -> eval_and (e1,e2)
    354   | Oor -> eval_or (e1,e2)
    355   | Oxor-> eval_xor (e1,e2)
    356   | Oshl-> eval_shl (e1,e2)
    357   | Oshr-> eval_shr (e1,e2)
    358   | Oeq -> eval_eq (e1,e2)
    359   | One -> eval_ne (e1,e2)
    360   | Olt -> eval_lt (e1,e2)
    361   | Ogt -> eval_gt (e1,e2)
    362   | Ole -> eval_le (e1,e2)
    363   | Oge -> eval_ge (e1,e2)
    364 
    365 let rec get_offset_struct v id = function
    366   | [] -> assert false (*Wrong id*)
    367   | (fi,_)::_ when fi=id -> v
    368   | (_,ty)::ll -> get_offset_struct
    369                     (Value.add v (Value.of_int (sizeof ty))) id ll
    370 
    371 let is_true (v,_) = Value.is_true v
    372 
    373 let is_false (v,_) = Value.is_false v
    374 
    375 let rec eval_expr globalenv localenv m e = let Expr (ee,tt) = e in
     294  | (v,Tint(isize,signedness),Tint(isize',_)) ->
     295    choose_cast signedness (int_of_intsize isize) (int_of_intsize isize') v
     296  | (v,_,_) -> v
     297
     298let eval_unop = function 
     299  | Onotbool -> Value.notbool
     300  | Onotint -> Value.notint
     301  | Oneg -> Value.negint
     302
     303let eval_add (v1,t1) (v2,t2) = match t1, t2 with
     304  | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
     305    let v = Value.mul (Value.of_int (sizeof ty)) v2 in
     306    Value.add v1 v
     307  | Tint _, Tpointer ty | Tint _, Tarray (ty, _) ->
     308    let v = Value.mul (Value.of_int (sizeof ty)) v1 in
     309    Value.add v2 v
     310  | _ -> Value.add v1 v2
     311
     312let eval_sub (v1,t1) (v2,t2) = match t1, t2 with
     313  | Tpointer ty, Tint _ | Tarray (ty, _), Tint _ ->
     314    let v = Value.mul (Value.of_int (sizeof ty)) v2 in
     315    Value.sub v1 v
     316  | _ -> Value.sub v1 v2
     317
     318let choose_signedness op_signed op_unsigned v1 v2 t =
     319  let op = match t with
     320    | Tint (_, Signed) -> op_signed
     321    | Tint (_, Unsigned) -> op_unsigned
     322    | _ -> op_unsigned in
     323  op v1 v2
     324
     325let eval_binop ret_ctype ((v1,t1) as e1) ((v2,t2) as e2) op =
     326  let v = match op with
     327    | Oadd -> eval_add e1 e2
     328    | Osub -> eval_sub e1 e2
     329    | Omul -> Value.mul v1 v2
     330    | Odiv -> choose_signedness Value.div Value.divu v1 v2 t1
     331    | Omod -> choose_signedness Value.modulo Value.modulou v1 v2 t1
     332    | Oand -> Value.and_op v1 v2
     333    | Oor -> Value.or_op v1 v2
     334    | Oxor -> Value.xor v1 v2
     335    | Oshl-> Value.shl v1 v2
     336    | Oshr-> Value.shr v1 v2
     337    | Oeq -> choose_signedness Value.cmp_eq Value.cmp_eq_u v1 v2 t1
     338    | One -> choose_signedness Value.cmp_ne Value.cmp_ne_u v1 v2 t1
     339    | Olt -> choose_signedness Value.cmp_lt Value.cmp_lt_u v1 v2 t1
     340    | Ole -> choose_signedness Value.cmp_le Value.cmp_le_u v1 v2 t1
     341    | Ogt -> choose_signedness Value.cmp_gt Value.cmp_gt_u v1 v2 t1
     342    | Oge -> choose_signedness Value.cmp_ge Value.cmp_ge_u v1 v2 t1 in
     343  eval_cast (v, t1, ret_ctype)
     344
     345let rec get_offset_struct v id fields =
     346  let sizes = List.map (fun (_, ty) -> sizeof ty) fields in
     347  let (offsets, _) = Mem.align 0 sizes in
     348  let rec select = function
     349    | (x, _) :: _, off :: _ when x = id -> off
     350    | _ :: fields, _ :: offsets -> select (fields, offsets)
     351    | _ -> assert false (* should be impossible *) in
     352  let off = Value.of_int (select (fields, offsets)) in
     353  Value.add v off
     354
     355let get_offset v id = function
     356  | Tstruct (_, fields) -> get_offset_struct v id fields
     357  | Tunion _ -> v
     358  | _ -> assert false (* do not use on these arguments *)
     359
     360let is_true (v, _) = Value.is_true v
     361let is_false (v, _) = Value.is_false v
     362
     363let rec eval_expr localenv m (Expr (ee, tt)) =
    376364  match ee with
    377     | Econst_int i ->
    378         let v = (match tt with
    379                    | Tint(I8,Signed) -> Value.cast8signed (Value.of_int i)
    380                    | Tint(I8,Unsigned) -> Value.cast8unsigned (Value.of_int i)
    381                    | Tint(I16,Signed) -> Value.cast16signed (Value.of_int i)
    382                    | Tint(I16,Unsigned) -> Value.cast16unsigned (Value.of_int i)
    383                    | Tint(I32,Signed) -> Value.of_int i
    384                    | Tint(I32,Unsigned) -> Value.of_int i (*FIXME*)
    385                    | _ -> assert false (*Type error*))
    386       in ((v,tt),[])
    387     | Econst_float _ -> assert false (*Not supported *)
    388     | Evar id   ->
    389         (match tt with
    390            | Tfunction (_,_) -> ((find_symbol globalenv localenv id,tt),[])
    391            | _ ->
    392                ((Mem.load m (mq_of_ty tt) (find_symbol globalenv localenv id),tt),[])
    393         )
    394     | Ederef exp -> let ((v1,t1),l1) = eval_expr globalenv localenv m exp in
    395         ((Mem.load m (mq_of_ty tt) v1,tt),l1)
    396     | Eaddrof exp -> eval_lvalue globalenv localenv m exp
     365    | Econst_int i ->
     366      let v = eval_cast (Value.of_int i, Tint(I32, Signed), tt) in
     367      ((v, tt),[])
     368    | Econst_float _ -> error_float ()
     369    | Evar id when is_function_type tt || is_big_type tt ->
     370      let v = value_of_address (find_symbol localenv m id) in
     371      ((v, tt), [])
     372    | Evar id ->
     373      let addr = find_symbol localenv m id in
     374      let v = Mem.load m (size_of_ctype tt) addr in
     375      ((v, tt), [])
     376    | Ederef e when is_function_type tt || is_big_type tt ->
     377      let ((v1,_),l1) = eval_expr localenv m e in
     378      ((v1,tt),l1)
     379    | Ederef e ->
     380      let ((v1,_),l1) = eval_expr localenv m e in
     381      let addr = address_of_value v1 in
     382      let v = Mem.load m (size_of_ctype tt) addr in
     383      ((v,tt),l1)
     384    | Eaddrof exp ->
     385      let ((addr,_),l) = eval_lvalue localenv m exp in
     386      ((value_of_address addr,tt),l)
     387    | Ebinop (op,exp1,exp2) -> 
     388      let (v1,l1) = eval_expr localenv m exp1 in
     389      let (v2,l2) = eval_expr localenv m exp2 in
     390      ((eval_binop tt v1 v2 op,tt),l1@l2)
    397391    | Eunop (op,exp) ->
    398         let (v1,l1) = eval_expr globalenv localenv m exp in
    399           ((eval_unop v1 op,tt),l1)
    400     | Ebinop (op,exp1,exp2) -> 
    401         let (v1,l1) = eval_expr globalenv localenv m exp1
    402         and (v2,l2) = eval_expr globalenv localenv m exp2 in
    403           ((eval_binop v1 v2 op,tt),l1@l2)
    404     | Ecast (cty,exp) ->
    405         let ((v,ty),l1) = eval_expr globalenv localenv m exp in
    406           ((eval_cast (v,ty,cty),tt),l1)
     392      let ((v1,_),l1) = eval_expr localenv m exp in
     393      ((eval_unop op v1,tt),l1)
    407394    | Econdition (e1,e2,e3) ->
    408         let (v1,l1) = eval_expr globalenv localenv m e1 in
    409           if is_true v1 then
    410             let (v2,l2) = eval_expr globalenv localenv m e2 in
    411               (v2,l1@l2)
    412           else if is_false v1 then
    413             let (v2,l2) = eval_expr globalenv localenv m e3 in
    414               (v2,l1@l2)
    415           else ((Value.undef,tt),l1)
     395      let (v1,l1) = eval_expr localenv m e1 in
     396      if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     397      else
     398        if is_false v1 then let (v3,l3) = eval_expr localenv m e3 in (v3,l1@l3)
     399      else (v1,l1)
    416400    | Eandbool (e1,e2) ->
    417         let (v1,l1) = eval_expr globalenv localenv m e1 in
    418           if is_true v1 then (
    419             let (v2,l2) = eval_expr globalenv localenv m e2 in
    420               if is_true v2 then
    421                 ((Value.val_true,tt),l1@l2)
    422               else (
    423                 if is_false v2 then ((Value.val_false,tt),l1@l2)
    424                 else ((Value.undef,tt),l1@l2)
    425               )) else (
    426                 if is_false v1 then ((Value.val_false,tt),l1)
    427                 else ((Value.undef,tt),l1))
     401      let (v1,l1) = eval_expr localenv m e1 in
     402      if is_true v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     403      else (v1,l1)
    428404    | Eorbool (e1,e2) ->
    429         let (v1,l1) = eval_expr globalenv localenv m e1 in
    430           if is_false v1 then (
    431             let (v2,l2) = eval_expr globalenv localenv m e2 in
    432               if is_true v2 then ((Value.val_true,tt),l1@l2)
    433               else (
    434                 if is_false v2 then ((Value.val_false,tt),l1@l2)
    435                 else ((Value.undef,tt),l1@l2)
    436           )) else (
    437             if is_true v1 then ((Value.val_true,tt),l1)
    438             else ((Value.undef,tt),l1))
     405      let (v1,l1) = eval_expr localenv m e1 in
     406      if is_false v1 then let (v2,l2) = eval_expr localenv m e2 in (v2,l1@l2)
     407      else (v1,l1)
    439408    | Esizeof cty -> ((Value.of_int (sizeof cty),tt),[])
    440409    | Efield (e1,id) ->
    441         let (v1,l1) = eval_expr globalenv localenv m e1 in
    442         (match v1 with
    443            | (v,Tstruct(_,lst)) when List.mem (id,tt) lst ->
    444                ((Mem.load m (mq_of_ty tt) (get_offset_struct v id lst),tt),l1)
    445            | (v,Tunion(_,lst)) when List.mem (id,tt) lst ->
    446                ((Mem.load m (mq_of_ty tt) v,tt),l1)
    447            | _ -> ((Value.undef,tt),l1)
    448         )
    449     | Ecost (lbl,e1) -> let (v1,l1) = eval_expr globalenv localenv m e1 in
    450         (v1,lbl::l1)
    451     | Ecall _ -> assert false (*For annotations only*)
    452 
    453 and eval_lvalue globalenv localenv m expr =
    454   let Expr (e,t) = expr in match e with
    455     | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
    456     | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
    457     | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
    458     | Efield (ee,id) -> let (v1,l1) = eval_expr globalenv localenv m ee in
    459         (match v1 with
    460            | (v,Tstruct(_,lst)) when List.mem (id,t) lst ->
    461                ((get_offset_struct v id lst,t),l1)
    462            | (v,Tunion(_,lst)) when List.mem (id,t) lst -> ((v,t),l1)
    463            | _ -> ((Value.undef,t),l1)
    464         )
    465     | Evar id -> ((find_symbol globalenv localenv id,t),[])
    466     | Ederef ee -> let ((v,_),l1) = eval_expr globalenv localenv m ee in
    467         ((v,t),l1)
    468     | Ecost (lbl,ee) -> let (v,l) = eval_lvalue globalenv localenv m ee in
    469         (v,lbl::l)
    470     | Ecall _ -> assert false (*For annotation only*)
    471 
    472 let eval_exprlist globalenv localenv m l =
    473   let rec eval_exprlist_rec vl ll = function
    474     | [] -> (vl,ll)
    475     | e::lst ->
    476         let (vl0,ll0) = eval_exprlist_rec vl ll lst
    477         and ((v,_),t) = eval_expr globalenv localenv m e in
    478         (v::vl0,t@ll0)
    479   in eval_exprlist_rec [] [] l
    480 
    481 let is_struct = function
    482   | Tarray (_,_) | Tunion (_,_) | Tstruct (_,_) -> true
    483   | _ -> false
    484 
    485 let bind_parameters m param_l arg_l var_l =
    486  let bind (m,e) (id,ty) arg =
    487    if is_struct ty then (
    488      assert (arg=Value.undef); (*a parameter can't be a struct/union/array*)
    489      let (m2,ptr2) = Mem.alloc m (sizeof ty)
    490      in let (m3,ptr3) = Mem.alloc m2 (Mem.ptr_size)
    491      in let m4 = Mem.store m3 (Mem.mq_of_ptr) ptr3 ptr2
    492      in (m4, (Hashtbl.add e id ptr3;e) ))
    493    else
    494      let (m2,ptr) = Mem.alloc m (sizeof ty) in
    495      let m3 = Mem.store m2 (mq_of_ty ty) ptr arg
    496      in (m3, (Hashtbl.add e id ptr;e) )
    497  in
    498    List.fold_left
    499      (fun a b -> bind a b Value.undef)
    500      (try List.fold_left2 bind (m,Hashtbl.create 13) param_l arg_l
    501      with (Invalid_argument _) -> assert false)
    502      var_l
    503 
    504 let assign m v ty ptr = Mem.store m (mq_of_ty ty) ptr v
    505 
    506 
    507 let type_of_fundef = function
    508   | Internal f -> Tfunction (List.map snd f.fn_params,f.fn_return)
    509   | External (_,p,t) -> Tfunction (p,t)
    510 
    511 let rec free_list m = function
    512   | [] -> m
    513   | v::l -> free_list (Mem.free m v) l
    514 
    515 let blocks_of_env e =
    516   let l = ref [] in
    517     Hashtbl.iter (fun _ b -> l:=b::(!l)) e;!l
    518 
    519 let typeof e = let Expr (_,t) = e in t
    520 
    521 let interpret_external vargs k m = function
    522     | "scan_int" ->
    523           Returnstate (Value.of_int (int_of_string (read_line ())), k, m)
    524     | "print_int" when List.length vargs = 1 ->
    525         Printf.printf "%d" (Value.to_int (List.hd vargs)) ;
    526         Returnstate (Value.zero, k, m)
    527     | "print_intln" when List.length vargs = 1 ->
    528         Printf.printf "%d\n" (Value.to_int (List.hd vargs)) ;
    529         Returnstate (Value.zero, k, m)
    530     | "malloc" | "alloc" when List.length vargs = 1 ->
    531         let (m',vv) = Mem.alloc m (Value.to_int (List.hd vargs)) in
    532           Returnstate (vv, k, m')
    533    | "exit"  when List.length vargs = 1 -> Returnstate(List.hd vargs,Kstop,m)
    534    | s -> Printf.eprintf "Error: unknown external function: %s\n" s;
    535           assert false (*Unknown external function*)
    536 
    537 let next_step globalenv = function
    538     | State(f,Sassign(a1,a2),k,e,m) ->
    539         let ((v1,t1),l1) = (eval_lvalue globalenv e m a1)
    540         and ((v2,t2),l2) = eval_expr globalenv e m a2
    541         in (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
    542     | State(f,Scall(None,a,al),k,e,m) ->
    543         let (v1,l1) = eval_expr globalenv e m a in
    544         let fd = find_funct globalenv v1
    545         and (vargs,l2) = (eval_exprlist globalenv e m al) in
    546           if type_of_fundef fd = typeof a
    547           then (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
    548           else assert false (*Signature mismatches*)
    549   | State(f,Scall(Some lhs,a,al),k,e,m) ->
    550       let (v1,l1) = eval_expr globalenv e m a in
    551       let fd = find_funct globalenv v1
    552       and (vargs,l2) = (eval_exprlist globalenv e m al)
    553       and ((v3,t3),l3) = eval_lvalue globalenv e m lhs in
    554         if type_of_fundef fd = typeof a then
    555           (Callstate(fd,vargs,Kcall(Some (v3, t3),f,e,k),m),l1@l2@l3)
    556         else assert false (*Signature mismatches*)
    557   | State(f,Ssequence(s1,s2),k,e,m) -> (State(f,s1,Kseq(s2,k),e,m),[])
    558   | State(f,Sskip,Kseq(s,k),e,m) -> (State(f,s,k,e,m),[])
    559   | State(f,Scontinue,Kseq(s,k),e,m) -> (State(f,Scontinue,k,e,m),[])
    560   | State(f,Sbreak,Kseq(s,k),e,m) -> (State(f,Sbreak,k,e,m),[])
    561   | State(f,Sifthenelse(a,s1,s2),k,e,m) ->
    562       let (v1,l1) = eval_expr globalenv e m a in
    563         if is_true v1 then (State(f,s1,k,e,m),l1)
    564         else if is_false v1 then (State(f,s2,k,e,m),l1)
    565         else assert false (*Wrong condition guard*)
    566   | State(f,Swhile(a,s),k,e,m) ->
    567       let (v1,l1) = eval_expr globalenv e m a in
    568         if is_false v1 then (State(f,Sskip,k,e,m),l1)
    569         else if is_true v1 then (State(f,s,Kwhile(a,s,k),e,m),l1)
    570         else assert false (*Wrong condition guard*)
    571   | State(f,Sskip,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
    572   | State(f,Scontinue,Kwhile(a,s,k),e,m) -> (State(f,Swhile(a,s),k,e,m),[])
    573   | State(f,Sbreak,Kwhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
    574   | State(f,Sdowhile(a,s),k,e,m) -> (State(f,s,Kdowhile(a,s,k),e,m),[])
    575   | State(f,Sskip,Kdowhile(a,s,k),e,m) ->
    576       let (v1,l1) = eval_expr globalenv e m a in
    577         if is_false v1 then (State(f,Sskip,k,e,m),l1)
    578         else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
    579         else assert false (*Wrong condition guard*)
    580   | State(f,Scontinue,Kdowhile(a,s,k),e,m) ->
    581       let (v1,l1) = eval_expr globalenv e m a in
    582         if is_false v1 then (State(f,Sskip,k,e,m),l1)
    583         else if is_true v1 then (State(f,Sdowhile(a,s),k,e,m),l1)
    584         else assert false (*Wrong condition guard*)
    585   | State(f,Sbreak,Kdowhile(a,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
    586   | State(f,Sfor(a1,a2,a3,s),k,e,m) when a1<>Sskip ->
    587       (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
    588   | State(f,Sfor(Sskip,a2,a3,s),k,e,m) ->
    589       let (v1,l1) = eval_expr globalenv e m a2 in
    590       if is_false v1 then (State(f,Sskip,k,e,m),l1)
    591       else if is_true v1 then (State(f,s,Kfor2(a2,a3,s,k),e,m),l1)
    592       else assert false (*Wrong condition guard*)
    593   | State(f,Sskip,Kfor2(a2,a3,s,k),e,m) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    594   | State(f,Scontinue,Kfor2(a2,a3,s,k),e,m) ->
    595       (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
    596   | State(f,Sbreak,Kfor2(a2,a3,s,k),e,m) -> (State(f,Sskip,k,e,m),[])
    597   | State(f,Sskip,Kfor3(a2,a3,s,k),e,m) ->
    598       (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
    599   | State(f,Sreturn None,k,e,m) when f.fn_return = Tvoid ->
    600       let m' = free_list m (blocks_of_env e) in
    601         (Returnstate(Value.undef,(call_cont k),m'),[])
    602   | State(f,Sreturn (Some a),k,e,m) when f.fn_return<>Tvoid ->
    603       let (v1,l1) = eval_expr globalenv e m a
    604       and m' = free_list m (blocks_of_env e) in
    605         (Returnstate(fst v1,call_cont k,m'),l1)
    606   | State(f,Sskip,k,e,m) when f.fn_return = Tvoid && is_call_cont k ->
    607       let m' = free_list m (blocks_of_env e) in
    608         (Returnstate(Value.undef,k,m'),[])
    609   | State(f,Sswitch(a,sl),k,e,m) ->
    610       let (n,l) = (match eval_expr globalenv e m a with
    611                      | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll)
    612                      | _ -> assert false (*Wrong switch index*)
    613       ) in
    614         (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
    615   | State(f,Sskip,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
    616   | State(f,Sbreak,Kswitch k,e,m) -> (State(f,Sskip,k,e,m),[])
    617   | State(f,Scontinue,Kswitch k,e,m) -> (State(f,Scontinue,k,e,m),[])
    618   | State(f,Slabel(lbl,s),k,e,m) -> (State(f,s,k,e,m),[])
    619   | State(f,Scost(lbl,s),k,e,m) -> (State(f,s,k,e,m),[lbl])
    620   | State(f,Sgoto lbl,k,e,m) ->
    621       (match find_label lbl f.fn_body (call_cont k) with
    622          | Some (s',k') -> (State(f,s',k',e,m),[])
    623          | None -> assert false (*Label does not exist*))
    624   | Callstate(Internal f,vargs,k,m) ->
    625       let (m',e) = bind_parameters m f.fn_params vargs f.fn_vars in
    626         (State(f,f.fn_body,k,e,m'),[])
    627   | Callstate(External(id,targs,tres),vargs,k,m)
    628       when List.length targs = List.length vargs ->
    629       (interpret_external vargs k m id,[])
     410      let ((v1,t1),l1) = eval_expr localenv m e1 in
     411      let addr = address_of_value (get_offset v1 id t1) in
     412      ((Mem.load m (size_of_ctype tt) addr, tt), l1)
     413    | Ecost (lbl,e1) ->
     414      let (v1,l1) = eval_expr localenv m e1 in
     415      (v1,lbl::l1)
     416    | Ecall _ -> assert false (* only used by the annotation process *)
     417    | Ecast (cty,exp) ->
     418      let ((v,ty),l1) = eval_expr localenv m exp in
     419      ((eval_cast (v,ty,cty),tt),l1)
     420
     421and eval_lvalue localenv m (Expr (e,t)) = match e with
     422  | Econst_int _ | Econst_float _ | Eaddrof _ | Eunop (_,_) | Ebinop (_,_,_)
     423  | Ecast (_,_) | Econdition (_,_,_) | Eandbool (_,_)  | Eorbool (_,_)
     424  | Esizeof _ -> assert false (*Not allowed in left side of assignement*)
     425  | Evar id -> ((find_symbol localenv m id,t),[])
     426  | Ederef ee ->
     427    let ((v,_),l1) = eval_expr localenv m ee in
     428    ((address_of_value v,t),l1)
     429  | Efield (ee,id) ->
     430    let ((v,tt),l1) = eval_expr localenv m ee in
     431    let v' = get_offset v id tt in
     432    ((address_of_value v', t), l1)
     433  | Ecost (lbl,ee) ->
     434    let (v,l) = eval_lvalue localenv m ee in
     435    (v,lbl::l)
     436  | Ecall _ -> assert false (* only used in the annotation process *)
     437
     438let eval_exprlist lenv mem es =
     439  let f (vs, cost_lbls) e =
     440    let ((v, _), cost_lbls') = eval_expr lenv mem e in
     441    (vs @ [v], cost_lbls @ cost_lbls') in
     442  List.fold_left f ([], []) es
     443
     444
     445let bind (mem, lenv) (x, ty) v =
     446  let (mem, addr) = Mem.alloc mem (sizeof ty) in
     447  let mem = Mem.store mem (sizeof ty) addr v in
     448  let lenv = LocalEnv.add x addr lenv in
     449  (mem, lenv)
     450
     451let bind_var (mem, lenv) (x, ty) = bind (mem, lenv) (x, ty) Value.undef
     452
     453let init_fun_env mem params args vars =
     454  let lenv = LocalEnv.empty in
     455  let (mem, lenv) =
     456    try List.fold_left2 bind (mem, lenv) params args
     457    with Invalid_argument _ -> error "wrong size of arguments." in
     458  List.fold_left bind_var (mem, lenv) vars
     459
     460let assign m v ty ptr = Mem.store m (size_of_ctype ty) ptr v
     461
     462
     463let free_local_env mem lenv =
     464  let f _ addr mem = Mem.free mem addr in
     465  LocalEnv.fold f lenv mem
     466
     467let condition v a_true a_false =
     468  if Value.is_false v then a_false
     469  else if Value.is_true v then a_true
     470  else error "undefined condition guard value."
     471
     472let eval_stmt f k e m s = match s, k with
     473  | Sskip, Kseq(s,k) -> (State(f,s,k,e,m),[])
     474  | Sskip, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
     475  | Sskip, Kdowhile(a,s,k) ->
     476    let ((v1, _),l1) = eval_expr e m a in
     477    let a_false = (State(f,Sskip,k,e,m),l1) in
     478    let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
     479    condition v1 a_true a_false
     480  | Sskip, Kfor3(a2,a3,s,k) -> (State(f,Sfor(Sskip,a2,a3,s),k,e,m),[])
     481  | Sskip, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
     482  | Sskip, Kswitch k -> (State(f,Sskip,k,e,m),[])
     483  | Sskip, Kcall _ ->
     484    let m' = free_local_env m e in
     485    (Returnstate(Value.undef,k,m'),[])
     486  | Sassign(a1, a2), _ ->
     487    let ((v1,t1),l1) = (eval_lvalue e m a1) in
     488    let ((v2,t2),l2) = eval_expr e m a2 in
     489    (State(f,Sskip,k,e,assign m v2 t1 v1),l1@l2)
     490  | Scall(None,a,al), _ ->
     491    let ((v1,_),l1) = eval_expr e m a in
     492    let fd = Mem.find_fun_def m (address_of_value v1) in
     493    let (vargs,l2) = eval_exprlist e m al in
     494    (Callstate(fd,vargs,Kcall(None,f,e,k),m),l1@l2)
     495  | Scall(Some lhs,a,al), _ ->
     496    let ((v1,_),l1) = eval_expr e m a in
     497    let fd = Mem.find_fun_def m (address_of_value v1) in
     498    let (vargs,l2) = eval_exprlist e m al in
     499    let (vt3,l3) = eval_lvalue e m lhs in
     500    (Callstate(fd,vargs,Kcall(Some vt3,f,e,k),m),l1@l2@l3)
     501  | Ssequence(s1,s2), _ -> (State(f,s1,Kseq(s2,k),e,m),[])
     502  | Sifthenelse(a,s1,s2), _ ->
     503    let ((v1,_),l1) = eval_expr e m a in
     504    let a_true = (State(f,s1,k,e,m),l1) in
     505    let a_false = (State(f,s2,k,e,m),l1) in
     506    condition v1 a_true a_false
     507  | Swhile(a,s), _ ->
     508    let ((v1,_),l1) = eval_expr e m a in
     509    let a_false = (State(f,Sskip,k,e,m),l1) in
     510    let a_true = (State(f,s,Kwhile(a,s,k),e,m),l1) in
     511    condition v1 a_true a_false
     512  | Sdowhile(a,s), _ -> (State(f,s,Kdowhile(a,s,k),e,m),[])
     513  | Sfor(Sskip,a2,a3,s), _ ->
     514    let ((v1,_),l1) = eval_expr e m a2 in
     515    let a_false = (State(f,Sskip,k,e,m),l1) in
     516    let a_true = (State(f,s,Kfor2(a2,a3,s,k),e,m),l1) in
     517    condition v1 a_true a_false
     518  | Sfor(a1,a2,a3,s), _ -> (State(f,a1,Kseq(Sfor(Sskip,a2,a3,s),k),e,m),[])
     519  | Sbreak, Kseq(s,k) -> (State(f,Sbreak,k,e,m),[])
     520  | Sbreak, Kwhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
     521  | Sbreak, Kdowhile(_,_,k) -> (State(f,Sskip,k,e,m),[])
     522  | Sbreak, Kfor2(_,_,_,k) -> (State(f,Sskip,k,e,m),[])
     523  | Sbreak, Kswitch k -> (State(f,Sskip,k,e,m),[])
     524  | Scontinue, Kseq(_,k) -> (State(f,Scontinue,k,e,m),[])
     525  | Scontinue, Kwhile(a,s,k) -> (State(f,Swhile(a,s),k,e,m),[])
     526  | Scontinue, Kdowhile(a,s,k) ->
     527    let ((v1,_),l1) = eval_expr e m a in
     528    let a_false = (State(f,Sskip,k,e,m),l1) in
     529    let a_true = (State(f,Sdowhile(a,s),k,e,m),l1) in
     530    condition v1 a_true a_false
     531  | Scontinue, Kfor2(a2,a3,s,k) -> (State(f,a3,Kfor3(a2,a3,s,k),e,m),[])
     532  | Scontinue, Kswitch k -> (State(f,Scontinue,k,e,m),[])
     533  | Sreturn None, _ ->
     534    let m' = free_local_env m e in
     535    (Returnstate(Value.undef,(call_cont k),m'),[])
     536  | Sreturn (Some a), _ ->
     537    let ((v1,_),l1) = eval_expr e m a  in
     538    let m' = free_local_env m e in
     539    (Returnstate(v1,call_cont k,m'),l1)
     540  | Sswitch(a,sl), _ ->
     541    let ((v,_),l) = eval_expr e m a in
     542    let n = Value.to_int v in
     543    (State(f,(seq_of_labeled_statement (select_switch n sl)),Kswitch k,e,m),l)
     544  | Slabel(lbl,s), _ -> (State(f,s,k,e,m),[])
     545  | Scost(lbl,s), _ -> (State(f,s,k,e,m),[lbl])
     546  | Sgoto lbl, _ ->
     547    let (s', k') = find_label lbl f.fn_body (call_cont k) in
     548    (State(f,s',k',e,m),[])
     549  | _ -> assert false (* should be impossible *)
     550
     551
     552module InterpretExternal = Primitive.Interpret (Mem)
     553
     554let interpret_external k mem f args =
     555  let (mem', v) = match InterpretExternal.t mem f args with
     556    | (mem', InterpretExternal.V v) -> (mem', v)
     557    | (mem', InterpretExternal.A addr) -> (mem', value_of_address addr) in
     558  Returnstate (v, k, mem')
     559
     560let step_call args cont mem = function
     561  | Internal f ->
     562    let (mem', e) = init_fun_env mem f.fn_params args f.fn_vars in
     563    State (f, f.fn_body, cont, e, mem')
     564  | External(id,targs,tres) when List.length targs = List.length args ->
     565    interpret_external cont mem id args
     566  | External(id,_,_) ->
     567    error ("wrong size of arguments when calling external " ^ id ^ ".")
     568
     569let step = function
     570  | State(f,stmt,k,e,m) -> eval_stmt f k e m stmt
     571  | Callstate(fun_def,vargs,k,m) -> (step_call vargs k m fun_def,[])
    630572  | Returnstate(v,Kcall(None,f,e,k),m) -> (State(f,Sskip,k,e,m),[])
    631573  | Returnstate(v,Kcall((Some(vv, ty)),f,e,k),m) ->
    632       let m' = assign m v ty vv in
    633         (State(f,Sskip,k,e,m'),[])
    634   | st ->
    635       Printf.eprintf "Error: no transition for %s\n" (string_of_state st);
    636       assert false
    637 
    638 let init_to_data = function
     574    let m' = assign m v ty vv in
     575    (State(f,Sskip,k,e,m'),[])
     576  | _ -> error "state malformation."
     577
     578
     579let data_of_init_data = function
    639580  | Init_int8 i         -> Data_int8 i
    640581  | Init_int16 i        -> Data_int16 i
    641582  | Init_int32 i        -> Data_int32 i
    642   | Init_float32 f      -> assert false (* Not supported *)
    643   | Init_float64 f      -> assert false (* Not supported *)
     583  | Init_float32 f      -> error_float ()
     584  | Init_float64 f      -> error_float ()
    644585  | Init_space i        -> Data_reserve i
    645   | Init_addrof (_,_)   -> assert false (*TODO*)
    646 
    647 let alloc_datas m ((_,lst),ty) =
    648   let store_data (m,ptr) = function (*FIXME signed or unsigned ?*)
    649     | Init_int8  i -> (Mem.store m Memory.MQ_int8signed ptr (Value.of_int i)
    650                        ,Value.add ptr (Value.of_int 1))
    651     | Init_int16 i -> (Mem.store m Memory.MQ_int16signed ptr (Value.of_int i)
    652                        ,Value.add ptr (Value.of_int 2))
    653     | Init_int32 i -> (Mem.store m Memory.MQ_int32 ptr (Value.of_int i)
    654                        ,Value.add ptr (Value.of_int 4))
    655     | Init_float32 _ -> assert false (*Not supported*)
    656     | Init_float64 _ -> assert false (*Not supported*)
    657     | Init_space n -> (m,Value.add ptr (Value.of_int n))
    658     | Init_addrof (_,_) -> assert false (*TODO*)
    659   in let (m2,ptr) = (Mem.alloc m (sizeof ty))
    660   in (fst (List.fold_left store_data (m2,ptr) lst),ptr)
    661 
    662 let initmem_clight prog =
    663   let alloc_funct i (g,f) (id,fct) =
    664     Hashtbl.add g id (Value.of_int (-i-1));
    665     Valtbl.add f (Value.of_int (-i-1)) fct;
    666     (g,f)
    667   and alloc_var (m,g) v =
    668     let (m',ptr) = alloc_datas m v in
    669       if is_struct (snd v) then
    670         let (m2,ptr2) = Mem.alloc m' (Mem.ptr_size) in
    671         let m3 = Mem.store m2 Mem.mq_of_ptr ptr2 ptr in
    672         Hashtbl.add g (fst (fst v)) ptr2;(m3,g)
    673       else
    674         ( (Hashtbl.add g (fst (fst v)) ptr);(m',g) )
    675   in let (m,g) =
    676     List.fold_left alloc_var (Mem.empty,Hashtbl.create 13) prog.prog_vars
    677   in let (g2,f) =
    678     MiscPottier.foldi alloc_funct (g,Valtbl.create 13) prog.prog_funct
    679   in
    680     (m,(g2,f))
     586  | Init_addrof (x,off) -> assert false (* TODO: need the size of [x]'s cells *)
     587
     588let init_mem prog =
     589  let f_var mem ((x, init_datas), ty) =
     590    Mem.add_var mem x (List.map data_of_init_data init_datas) in
     591  let mem = List.fold_left f_var Mem.empty prog.prog_vars in
     592  let f_fun_def mem (f, def) = Mem.add_fun_def mem f def in
     593  List.fold_left f_fun_def mem prog.prog_funct
    681594
    682595let compute_result v =
     
    684597  else IntValue.Int8.zero
    685598
    686 let interpret debug prog = match prog.prog_main with
    687   | None -> (IntValue.Int8.zero, [])
    688   | Some main ->
    689       let (m,g) = initmem_clight prog in
    690       let first_state = (Callstate(find_funct_id g main,[],Kstop,m),[]) in
    691       let rec exec trace = function
    692         | (Returnstate(v,Kstop,m),l) ->
    693 (*
    694             if debug then (
    695               print_string ("Result: "^(Value.to_string v));
    696               print_string ("\nMemory dump: \n");
    697               Mem.print m
    698             );
    699 *)
    700           let (res, cost_labels) as trace = (compute_result v, l@trace) in
    701           if debug then
    702             Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ;
    703           trace
    704         | (State(_,Sskip,Kstop,_,m),l) -> (*Implicit return in main*)
    705 (*
    706             if debug then (
    707               print_string ("Result: (implicit return)");
    708               print_string ("\nMemory dump: \n");
    709               Mem.print m
    710             );
    711 *)
    712           let (res, cost_labels) as trace = (IntValue.Int8.zero, l@trace) in
    713           if debug then
    714             Printf.printf "Clight: %s\n%!" (IntValue.Int8.to_string res) ;
    715           trace
    716         | (state,l) ->
    717 (*
    718             if debug then print_string ((string_of_state state)^"\n");
    719 *)
    720             exec (l@trace) (next_step g state)
    721       in
    722 (*
    723       if debug then print_string "> --- Interpret Clight --- <\n";
    724 *)
    725       exec [] first_state
     599let rec exec debug trace (state, l) =
     600  let cost_labels = l @ trace in
     601  let print_and_return_result res =
     602    if debug then Printf.printf "Result = %s\n%!"
     603      (IntValue.Int8.to_string res) ;
     604    (res, cost_labels) in
     605  if debug then print_state state ;
     606  match state with
     607    | Returnstate(v,Kstop,_) -> (* Explicit return in main *)
     608      print_and_return_result (compute_result v)
     609    | State(_,Sskip,Kstop,_,_) -> (* Implicit return in main *)
     610      print_and_return_result IntValue.Int8.zero
     611    | state -> exec debug cost_labels (step state)
     612
     613let interpret debug prog =
     614  if debug then Printf.printf "*** Clight ***\n\n%!" ;
     615  match prog.prog_main with
     616    | None -> (IntValue.Int8.zero, [])
     617    | Some main ->
     618      let mem = init_mem prog in
     619      let first_state = (Callstate (find_fundef main mem,[],Kstop,mem),[]) in
     620      exec debug [] first_state
  • Deliverables/D2.2/8051/src/clight/clightInterpret.mli

    r486 r740  
    33    can also print debug informations.  *)
    44
     5(** [interpret debug p] returns the trace of execution of program [p]. *)
     6
    57val interpret: bool -> Clight.program -> AST.trace
  • Deliverables/D2.2/8051/src/clight/clightParser.ml

    r486 r740  
    11let process file =
    2   let tmp_file = Filename.temp_file "cparser" ".i"
     2  let tmp_file1 = Filename.temp_file "cparser1" ".c"
     3  and tmp_file2 = Filename.temp_file "cparser2" ".i"
    34  and prepro_opts = [] in
     5
     6  (* Add CerCo's primitives *)
     7  let _ =
     8    try
     9      let oc = open_out tmp_file1 in
     10      output_string oc Primitive.prototypes ;
     11      close_out oc
     12    with Sys_error _ -> failwith "Error adding primitive prototypes." in
     13  let rc = Sys.command
     14    (Printf.sprintf "cat %s >> %s"
     15       (Filename.quote file) (Filename.quote tmp_file1)) in
     16  if rc <> 0 then (
     17    Misc.SysExt.safe_remove tmp_file1;
     18    failwith "Error adding primitive prototypes."
     19  );
    420
    521  (* Preprocessing *)
     
    824    (Printf.sprintf "gcc -E -U__GNUC__ %s %s > %s"
    925       (String.concat " " (List.map Filename.quote prepro_opts))
    10        (Filename.quote file) (Filename.quote tmp_file)) in
     26       (Filename.quote tmp_file1) (Filename.quote tmp_file2)) in
    1127  if rc <> 0 then (
    12     Misc.SysExt.safe_remove tmp_file; failwith "Error calling gcc."
     28    Misc.SysExt.safe_remove tmp_file1;
     29    Misc.SysExt.safe_remove tmp_file2;
     30    failwith "Error calling gcc."
    1331  );
    1432
    1533  (* C to Cil *)
    16   let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file in
    17   Misc.SysExt.safe_remove tmp_file;
     34  let r = Cparser.Parse.preprocessed_file "CSf" file tmp_file2 in
     35  Misc.SysExt.safe_remove tmp_file1;
     36  Misc.SysExt.safe_remove tmp_file2;
    1837  match r with
    1938    | None -> failwith "Error during C parsing."
  • Deliverables/D2.2/8051/src/clight/clightToCminor.ml

    r624 r740  
    22open Cminor
    33open Clight
     4
     5
     6let error_prefix = "Cminor to RTLabs"
     7let error = Error.global_error error_prefix
     8let error_float () = error "float not supported."
     9
    410
    511(*For internal use*)
     
    1420let ptr_size = Driver.CminorMemory.ptr_size
    1521let alignment = Driver.CminorMemory.alignment
    16 let ptr_mq = Memory.MQ_pointer
    1722
    1823let fresh_tmp variables =
     
    3641  | _           -> Sig_int
    3742
    38 let rec mq_of_ty = function
     43let rec size_of_ty = function
    3944  | Tvoid               -> assert false
    4045  | Tfloat _            -> assert false (*Not supported*)
    4146  | Tfunction (_,_)     -> assert false (*Not supported*)
    42   | Tint (I8,Signed)    -> Memory.MQ_int8signed
    43   | Tint (I8,Unsigned)  -> Memory.MQ_int8unsigned
    44   | Tint (I16,Signed)   -> Memory.MQ_int16signed
    45   | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned
     47  | Tint (I8,Signed)    -> 1
     48  | Tint (I8,Unsigned)  -> 1
     49  | Tint (I16,Signed)   -> 2
     50  | Tint (I16,Unsigned) -> 2
    4651  (*FIXME MQ_int32 : signed or unsigned ? *)
    47   | Tint (I32,Signed)   -> Memory.MQ_int32
    48   | Tint (I32,Unsigned) ->  Memory.MQ_int32
     52  | Tint (I32,Signed)   -> 4
     53  | Tint (I32,Unsigned) -> 4
    4954  | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
    50   | Tcomp_ptr _         -> ptr_mq
     55  | Tcomp_ptr _         -> ptr_size
     56
     57let size_of_intsize = function
     58  | I8 -> 1
     59  | I16 -> 2
     60  | I32 -> 4
     61
     62let quantity_of_ty = function
     63  | Tvoid               -> assert false (* do not use on this argument *)
     64  | Tint (size,_)       -> Memory.QInt (size_of_intsize size)
     65  | Tpointer _ | Tarray (_,_) | Tstruct (_,_) | Tunion (_,_)
     66  | Tfunction (_,_)
     67  | Tcomp_ptr _         -> Memory.QPtr
     68  | Tfloat _            -> error_float ()
    5169
    5270let init_to_data l = List.map (
     
    103121      Op2 (Op_addp,e1, Op2 (Op_mul,e2,Cst (Cst_int (size_of_ctype t))))
    104122  | (Tint(_,_),Tpointer t)      ->
    105       Op2 (Op_addp,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))),e2)
     123      Op2 (Op_addp,e2,Op2 (Op_mul,e1,Cst (Cst_int (size_of_ctype t))))
    106124  | (Tarray (t,_),Tint(_,_))    ->
    107125      Op2 (Op_addp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
     
    115133  | (Tpointer t,Tint(_,_))      ->
    116134      Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    117   | (Tint(_,_),Tpointer t)      ->
    118       Op2 (Op_subp,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))),e2)
    119135  | (Tarray (t,_),Tint(_,_))    ->
    120136      Op2 (Op_subp,e1,Op2 (Op_mul,e2,(Cst (Cst_int (size_of_ctype t)))))
    121   | (Tint(_,_),Tarray(t,_))     ->
    122       Op2 (Op_subp,e2,Op2 (Op_mul,e1,(Cst (Cst_int (size_of_ctype t)))))
    123137  | _                           -> assert false (*Type error*)
    124138
     
    129143
    130144let translate_div e1 e2 = function
    131 (*
    132145  | (Tint(_,Signed),Tint(_,Signed))     -> Op2 (Op_div,e1,e2)
    133 *)
    134   (* TODO: temporary hack! *)
    135   | (Tint(_,Signed),Tint(_,Signed))     -> Op2 (Op_divu,e1,e2)
    136146  | (Tint(_,Unsigned),Tint(_,Unsigned)) -> Op2 (Op_divu,e1,e2)
    137147  | (Tfloat _,Tfloat _)                 -> assert false (*Not supported*)
     
    157167
    158168let make_cast e = function
    159   | (Tint(_,_),Tint(I8,Signed)) when int_size>8     -> Op1 (Op_cast8signed,e)
    160   | (Tint(_,_),Tint(I8,Unsigned)) when int_size>8   -> Op1 (Op_cast8unsigned,e)
    161   | (Tint(_,_),Tint(I16,Signed)) when int_size>16   -> Op1 (Op_cast16signed,e)
    162   | (Tint(_,_),Tint(I16,Unsigned)) when int_size>16 -> Op1 (Op_cast16unsigned,e)
     169  | (Tint(I8,Signed),Tint(_,_))    -> Op1 (Op_cast8signed,e)
     170  | (Tint(I8,Unsigned),Tint(_,_))  -> Op1 (Op_cast8unsigned,e)
     171  | (Tint(I16,Signed),Tint(_,_))   -> Op1 (Op_cast16signed,e)
     172  | (Tint(I16,Unsigned),Tint(_,_)) -> Op1 (Op_cast16unsigned,e)
    163173  | _ -> e
    164174
     
    191201           | (Local,_)          -> Id id
    192202           | (Stack o,ty) when is_struct ty     -> Cst (Cst_stackoffset o)
    193            | (Stack o,_)        -> Mem (mq_of_ty c,Cst (Cst_stackoffset o))
     203           | (Stack o,_)        ->
     204             Mem (quantity_of_ty c,Cst (Cst_stackoffset o))
    194205           | (Param,_)          -> Id id
    195206           | (Global,ty) when is_struct ty -> Cst (Cst_addrsymbol id)
    196            | (Global,_)         -> Mem (mq_of_ty c,Cst (Cst_addrsymbol id))
     207           | (Global,_)         ->
     208             Mem (quantity_of_ty c,Cst (Cst_addrsymbol id))
    197209        ) with Not_found -> assert false)
    198210    | Ederef e when is_ptr_to_struct (get_type e) ->
    199211        translate_expr variables e
    200     | Ederef e          -> Mem (mq_of_ty c,translate_expr variables e)
     212    | Ederef e          -> Mem (quantity_of_ty c,translate_expr variables e)
    201213    | Eaddrof se        ->  (
    202214        match se with
     
    248260           | Tstruct(_,lst) ->
    249261               (try
    250                   Mem (mq_of_ty (List.assoc id lst)
     262                  Mem (quantity_of_ty (List.assoc id lst)
    251263                       ,Op2(Op_add
    252264                            ,translate_expr variables e
     
    258270           | Tunion(_,lst) ->
    259271               (try
    260                   Mem (mq_of_ty (List.assoc id lst), translate_expr variables e)
     272                  Mem (quantity_of_ty (List.assoc id lst), translate_expr variables e)
    261273                with Not_found -> assert false (*field does not exists*)
    262274               )
     
    270282      (try (match Hashtbl.find variables v with
    271283         | (Local,_)            -> St_assign (v,translate_expr variables e)
    272          | (Stack o,_)          -> St_store (mq_of_ty t
     284         | (Stack o,_)          -> St_store (quantity_of_ty t
    273285                                             ,Cst (Cst_stackoffset o)
    274286                                             ,translate_expr variables e)
    275287         | (Param,_)            -> St_assign (v,translate_expr variables e)
    276          | (Global,_)           -> St_store (mq_of_ty t
     288         | (Global,_)           -> St_store (quantity_of_ty t
    277289                                             ,Cst (Cst_addrsymbol v)
    278290                                             ,translate_expr variables e)
    279291      ) with Not_found -> assert false)
    280   | Expr (Ederef ee,t)          -> St_store (mq_of_ty t
     292  | Expr (Ederef ee,t)          -> St_store (quantity_of_ty t
    281293                                             ,translate_expr variables ee
    282294                                             ,translate_expr variables e)
     
    284296      (match ee with
    285297         | Expr (_,Tstruct(_,lst)) ->
    286              St_store (mq_of_ty t
     298             St_store (quantity_of_ty t
    287299                       ,Op2(Op_add,translate_expr variables ee
    288300                            ,Cst(Cst_int (get_offset_struct 0 id lst )))
    289301                       ,translate_expr variables e)
    290          | Expr (_,Tunion(_,_)) -> St_store (mq_of_ty t
     302         | Expr (_,Tunion(_,_)) -> St_store (quantity_of_ty t
    291303                                             ,translate_expr variables ee
    292304                                             ,translate_expr variables e)
     
    319331                         St_seq (
    320332                           st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
    321                            ,St_store (mq_of_ty tt,Cst (Cst_stackoffset o),Id tmp)
     333                           ,St_store (quantity_of_ty tt,Cst (Cst_stackoffset o),Id tmp)
    322334                         )
    323335                   | (Global,_) ->
     
    325337                         St_seq (
    326338                           st_call (Some tmp) (Type_ret (ctype_to_sig_type tt))
    327                            ,St_store (mq_of_ty tt,Cst (Cst_addrsymbol v),Id tmp)
     339                           ,St_store (quantity_of_ty tt,Cst (Cst_addrsymbol v),Id tmp)
    328340                         )
    329341                ) with Not_found -> assert false )
     
    526538
    527539let translate p =
    528   (* TODO: Clight32 to Clight8 transformation *)
    529 (*
    530540  let p = Clight32ToClight8.translate p in
    531 *)
    532   (* <DEBUG> *)
    533 (*
    534   Printf.printf "%s\n%!" (ClightPrinter.print_program p) ;
    535 *)
    536   (* </DEBUG> *)
    537541  let globals = List.map (fun p -> (fst (fst p),snd p) ) p.prog_vars in
    538542  let p =
     
    540544     Cminor.functs = List.map (translate_funct globals ) p.prog_funct;
    541545     Cminor.main = p.prog_main } in
     546  (* TODO: find a better solution to get the pointers in the result. *)
    542547  CminorPointers.fill p
Note: See TracChangeset for help on using the changeset viewer.