Changeset 619 for Deliverables/D2.2/8051


Ignore:
Timestamp:
Mar 2, 2011, 3:27:41 PM (10 years ago)
Author:
ayache
Message:

Update of D2.2 from Paris.

Location:
Deliverables/D2.2/8051
Files:
8 added
54 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D2.2/8051/README

    r530 r619  
    55  the CIL parser[1], Xavier Leroy's translation from C to Clight, and
    66  an existing back-end compiler for a register transfer language to a
    7   subset of the MIPS assembly language[2] or the 8051 microprocessor
    8   family. The current version is configured to output 8051 code.
     7  subset of the MIPS assembly language[2].
    98
    109  We wrote 3 compiler passes: one from Clight to Cminor, another from
    1110  Cminor to an abstract register transfer language (RTLabs), and a
    12   last one from RTLabs to an RTL that uses either MIPS or 8051 instructions.
    13   We extended interpreters for the intermediate languages to output a
     11  last one from RTLabs to an RTL that uses MIPS instructions. We
     12  extended interpreters for the intermediate languages to output a
    1413  list of labels which denote key control points of the program that
    1514  have been crossed during the interpretation. These labels are the

  • Deliverables/D2.2/8051/distributed_files

    r486 r619  
    854854./src/ASM/printOps.ml
    855855./src/ASM/printOps.mli
     856./src/ASM/Pretty.ml
     857./src/ASM/Pretty.mli
    856858./src/ASM/Util.ml
    857859./src/clight

  • Deliverables/D2.2/8051/myocamlbuild_config.ml

    r486 r619  
    1 let parser_lib = "/home/ayache/Work/Source/CerCo/experiments/compiler/branches/8051/lib"
     1let parser_lib = "/home/ayache/Downloads/Bol/Deliverables/D2.2/8051/lib"

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

    r486 r619  
    113113type preamble = (string * int) list
    114114
     115(* has_main currently unused *)
     116type 'a pretty_program =
     117    { ppreamble   : preamble ;
     118      pexit_label : string ;
     119      pcode       : 'a list ;
     120      phas_main   : bool }
     121
    115122type program =
    116     { preamble   : preamble ;
    117       exit_label : Label.t ;
    118       code       : labelled_instruction list ;
    119       has_main   : bool }
     123    { code        : BitVectors.byte list ;
     124      cost_labels : string BitVectors.WordMap.t ;
     125      exit_addr   : BitVectors.word ;
     126      has_main    : bool }

  • Deliverables/D2.2/8051/src/ASM/ASMCosts.ml

    r486 r619  
    11
    22let error_prefix = "ASMCosts"
    3 let error s = Error.global_error error_prefix s
    4 let warning s = Error.warning error_prefix s
     3let warning s = prerr_endline (error_prefix ^ s)
    54
    65
    76type instruction_nature =
    8   | Cost of CostLabel.t
    9   | Goto of Label.t | Branch of Label.t
    10   | Direct_fun_call of Label.t | Return
     7  | Goto of BitVectors.word | Branch of BitVectors.word
     8  | Direct_fun_call of BitVectors.word | Return
    119  | Other
    1210
    13 let inst_nature = function
    14   | `Cost lbl -> Cost lbl
    15   | `Call lbl -> Direct_fun_call lbl
    16   | `Jmp lbl -> Goto lbl
    17   | `WithLabel (`JC (`Label lbl))
    18   | `WithLabel (`JNC (`Label lbl))
    19   | `WithLabel (`JB (_, `Label lbl))
    20   | `WithLabel (`JNB (_, `Label lbl))
    21   | `WithLabel (`JBC (_, `Label lbl))
    22   | `WithLabel (`JZ (`Label lbl))
    23   | `WithLabel (`JNZ (`Label lbl))
    24   | `WithLabel (`CJNE (_, `Label lbl))
    25   | `WithLabel (`DJNZ (_, `Label lbl)) -> Branch lbl
     11let inst_nature pc = function
     12  | `LCALL (`ADDR16 addr16) -> Direct_fun_call addr16
     13  | `ACALL (`ADDR11 addr11) ->
     14    Direct_fun_call (Physical.addr16_of_addr11 pc addr11)
     15  | `LJMP (`ADDR16 addr16) -> Goto addr16
     16  | `AJMP (`ADDR11 addr11) -> Goto (Physical.addr16_of_addr11 pc addr11)
     17  | `SJMP (`REL addr) ->
     18      let _, addr = BitVectors.half_add pc (BitVectors.sign_extension addr) in
     19       Goto addr
     20  | `JMP idptr -> Other (* Indirect jump; precondition: every possible
     21                           destination should start with its own label *)
     22  | `JC addr
     23  | `JNC addr
     24  | `JB (_,addr)
     25  | `JNB (_,addr)
     26  | `JBC (_,addr)
     27  | `JZ addr
     28  | `JNZ addr
     29  | `CJNE (_,addr)
     30  | `DJNZ (_,addr) ->
     31      let `REL addr = addr in
     32      let _, addr = BitVectors.half_add pc (BitVectors.sign_extension addr) in
     33       Branch addr
    2634  | `RET -> Return
    2735  | _ -> Other
    2836
    2937
    30 let pc_of_label p =
    31   let f pc map = function
    32     | `Label lab -> StringTools.Map.add lab pc map
    33     | _ -> map
    34   in
    35   MiscPottier.foldi f StringTools.Map.empty p.ASM.code
    36 
    37 
    38 let inst_cost = function
    39   | `Cost _ | `Label _ -> 0
    40   | _ -> 1
    41 
    42 
    43 let block_cost pc_of_label p =
    44   let rec aux pc =
    45     if pc >= List.length p.ASM.code then 0
     38(* TODO: do not consider the very first instruction as ending the block since it
     39   contains the cost label whose cost we are trying to compute! *)
     40let block_cost mem costs =
     41  let rec aux oldpc =
     42    if BitVectors.WordMap.mem oldpc costs then 0
    4643    else
    47       let inst = List.nth p.ASM.code pc in
    48       let cost = match inst_nature inst with
    49         | Cost _ | Return -> 0
    50         | Goto lbl ->
    51           let pc = StringTools.Map.find lbl pc_of_label in
    52           aux pc
    53         | Branch lbl ->
    54           let pc1 = pc + 1 in
    55           let pc2 = StringTools.Map.find lbl pc_of_label in
    56           let cost1 = aux pc1 in
    57           let cost2 = aux pc2 in
    58           let cost = max cost1 cost2 in
    59           if cost1 <> cost2 then
    60             warning
    61               (Printf.sprintf
     44      let inst,pc,inst_cost = ASMInterpret.fetch mem oldpc in
     45      let cost = match inst_nature oldpc inst with
     46        | Return -> 0
     47        | Goto pc -> aux pc
     48        | Branch pc2 ->
     49          let pc1 =
     50            snd (BitVectors.half_add pc (BitVectors.vect_of_int 1 `Sixteen)) in
     51          let cost1 = aux pc1 in
     52          let cost2 = aux pc2 in
     53          if cost1 <> cost2 then
     54            warning
     55              (Printf.sprintf
    6256                 "Warning: branching to %s has cost %d; continuing has cost %d.\n"
    63               lbl cost2 cost1) ;
    64           cost
    65         | _ -> aux (pc+1)
     57                 "*fixme*"(*pc2*) cost2 cost1) ;
     58        max cost1 cost2
     59      | _ -> aux pc
    6660    in
    67     cost + inst_cost inst
     61     cost + inst_cost
    6862  in
    6963  aux
    7064
    7165
    72 let rec init_function p pc =
    73   let inst = List.nth p.ASM.code pc in
    74   match inst_nature inst with
    75     | Cost lbl -> (lbl, 0, pc+1)
    76     | _ ->
    77       let (lbl, cost, pc) = init_function p (pc+1) in
    78       (lbl, cost + (inst_cost inst), pc)
     66let traverse_code mem p =
     67  let rec aux pc code =
     68    let _,newpc,_ = ASMInterpret.fetch mem pc in
     69    match code with
     70      | [] -> CostLabel.Map.empty
     71      | _::tl when BitVectors.WordMap.mem pc p.ASM.cost_labels ->
     72        let lbl = BitVectors.WordMap.find pc p.ASM.cost_labels in
     73        let cost = block_cost mem p.ASM.cost_labels pc in
     74        let costs_mapping = aux newpc tl in
     75        CostLabel.Map.add lbl cost costs_mapping
     76      | _::tl -> aux newpc tl
     77  in
     78  aux (BitVectors.zero `Sixteen) p.ASM.code
    7979
    8080
    81 let traverse_code pc_of_label p =
    82   let rec aux pc =
    83     if pc >= List.length p.ASM.code then CostLabel.Map.empty
    84     else
    85       match inst_nature (List.nth p.ASM.code pc) with
    86         | Cost lbl ->
    87           let cost = block_cost pc_of_label p (pc+1) in
    88           let costs_mapping = aux (pc+1) in
    89           CostLabel.Map.add lbl cost costs_mapping
    90         | _ -> aux (pc+1)
     81let first_cost_label mem costs =
     82  let rec aux oldpc =
     83    try (BitVectors.WordMap.find oldpc costs, 0)
     84    with
     85      | Not_found ->
     86        let inst,pc,inst_cost = ASMInterpret.fetch mem oldpc in
     87        match inst_nature oldpc inst with
     88          | Direct_fun_call pc ->
     89            let (lbl, cost) = aux pc in
     90            (lbl, inst_cost + cost)
     91          | Return
     92          | Goto _
     93          | Branch _ ->
     94            assert false (* no such instructions before calling main *)
     95          | Other ->
     96            let (lbl, cost) = aux pc in
     97            (lbl, inst_cost + cost)
    9198  in
    92   aux 0
     99  aux (BitVectors.zero `Sixteen)
    93100
    94101
    95 let first_cost_label pc_of_label p =
    96   let rec aux pc =
    97     if pc >= List.length p.ASM.code then assert false (* should not happen *)
    98     else
    99       match inst_nature (List.nth p.ASM.code pc) with
    100         | Cost lbl -> lbl
    101         | Direct_fun_call lbl -> aux (StringTools.Map.find lbl pc_of_label)
    102         | _ -> aux (pc+1)
    103   in
    104   aux 0
    105 
    106 let initialize_cost pc_of_label p costs_mapping =
    107   let lbl = first_cost_label pc_of_label p in
     102let initialize_cost mem costs costs_mapping =
     103  let (lbl, cost) = first_cost_label mem costs in
    108104  let old_cost =
    109     if CostLabel.Map.mem lbl costs_mapping then
    110       CostLabel.Map.find lbl costs_mapping
    111     else 0 in
    112   let init = 1 (* cost of the preamble *) in
    113   let new_cost = old_cost + init in
     105    assert (CostLabel.Map.mem lbl costs_mapping) ;
     106    CostLabel.Map.find lbl costs_mapping in
     107  let new_cost = old_cost + cost in
    114108  CostLabel.Map.add lbl new_cost costs_mapping
    115109
    116110
    117111let compute p =
    118   let pc_of_label = pc_of_label p in
    119   let costs_mapping = traverse_code pc_of_label p in
    120   if p.ASM.has_main then initialize_cost pc_of_label p costs_mapping
     112  let mem = ASMInterpret.load_code_memory p.ASM.code in
     113  let costs_mapping = traverse_code mem p in
     114  if p.ASM.has_main then initialize_cost mem p.ASM.cost_labels costs_mapping
    121115  else costs_mapping

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

    r486 r619  
    22open Physical;;
    33open ASM;;
    4 open ASMPrinter;;
    54open IntelHex;;
    65open Util;;
    … …  
    5655      (* let _ = prerr_endline <*> string_of_line $ line in *)
    5756      (time + 1),debug_continuation)
    58 
    59 module IntMap = Map.Make(struct type t = int let compare = compare end);;
    60 type costs = CostLabel.t IntMap.t
    61 
     57   
    6258(* no differentiation between internal and external code memory *)
    6359type status =
    6460{
    6561  (* Memory *)
    66   code_memory: WordMap.map;        (* can be reduced *)
     62  code_memory: Physical.WordMap.map;        (* can be reduced *)
    6763  low_internal_ram: Byte7Map.map;
    6864  high_internal_ram: Byte7Map.map;
    69   external_ram: WordMap.map;
     65  external_ram: Physical.WordMap.map;
    7066
    7167  (* Program counter *)
    … …  
    134130  es_running: bool;
    135131
    136   exit_pc: word option;
    137   costs: costs;
     132  exit_addr   : BitVectors.word;
     133  cost_labels : string BitVectors.WordMap.t
    138134}
    139135
    … …  
    225221
    226222let initialize = {
    227   code_memory = WordMap.empty;
     223  code_memory = Physical.WordMap.empty;
    228224  low_internal_ram = Byte7Map.empty;
    229225  high_internal_ram = Byte7Map.empty;
    230   external_ram = WordMap.empty;
     226  external_ram = Physical.WordMap.empty;
    231227 
    232228  pc = zero `Sixteen;
    … …  
    287283  es_running = false;
    288284
    289   costs = IntMap.empty;
    290   exit_pc = None;
     285  exit_addr = BitVectors.zero `Sixteen;
     286  cost_labels = BitVectors.WordMap.empty
    291287}
    292288
    … …  
    387383  let next pc =
    388384    let _carry, res = half_add pc (vect_of_int 1 `Sixteen) in
    389     res, WordMap.find pc pmem
     385    res, Physical.WordMap.find pc pmem
    390386  in
    391387  let pc,instr = next pc in
    … …  
    693689       let pc,b2 = next pc in
    694690         `XRL(`U2(`DIRECT b1, `DATA b2)), pc, 2
    695    | _,_ -> assert false
     691   | (true,false,true,false),(false,true,false,true) ->
     692       (* undefined opcode *) assert false
    696693;;
    697694
    … …  
    927924;;
    928925
    929 let fold_lefti f =
    930  let rec aux i acc =
    931   function
    932      [] -> acc
    933    | he::tl -> aux (i+1) (f i acc he) tl
    934  in
    935   aux 0
    936 ;;
    937 
    938 let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty
    939 
    940 let load_mem mem exit_pc costs status =
    941   { status with code_memory = mem ;
    942                 exit_pc = exit_pc ;
    943                 costs = costs }
    944 let load l exit_pc costs = load_mem (load_code_memory l) exit_pc costs
    945 
    946 module StringMap = Map.Make(String);;
    947 
     926let load_code_memory = MiscPottier.foldi (fun i mem v -> Physical.WordMap.add (vect_of_int i `Sixteen) v mem) Physical.WordMap.empty
     927
     928let load_mem mem status = { status with code_memory = mem }
     929let load l = load_mem (load_code_memory l)
    948930
    949931let assembly_jump addr_of =
    … …  
    965947   (fun (datalabels,addr) (name,size) ->
    966948     let addr16 = vect_of_int addr `Sixteen in
    967       StringMap.add name addr16 datalabels, addr+size
    968    ) (StringMap.empty,0) p.ASM.preamble
     949      StringTools.Map.add name addr16 datalabels, addr+size
     950   ) (StringTools.Map.empty,0) p.ASM.ppreamble
    969951 in
    970  let pc,labels,costs =
     952 let pc,exit_addr,labels,costs =
    971953  List.fold_left
    972    (fun (pc,labels,costs) i ->
     954   (fun (pc,exit_addr,labels,costs) i ->
    973955     match i with
    974         `Label s -> pc, StringMap.add s pc labels, costs
    975       | `Cost s -> pc, labels, IntMap.add pc s costs
    976       | `Mov (_,_) -> pc, labels, costs
     956        `Label s when s = p.ASM.pexit_label ->
     957          pc, pc, StringTools.Map.add s pc labels, costs
     958      | `Label s ->
     959          pc, exit_addr, StringTools.Map.add s pc labels, costs
     960      | `Cost s -> pc, exit_addr, labels, BitVectors.WordMap.add pc s costs
     961      | `Mov (_,_) -> pc, exit_addr, labels, costs
    977962      | `Jmp _
    978       | `Call _ -> pc + 3, labels, costs  (*CSC: very stupid: always expand to worst opcode *)
     963      | `Call _ ->
     964        (snd (half_add pc (BitVectors.vect_of_int 3 `Sixteen))),
     965        exit_addr, labels, costs
     966      (*CSC: very stupid: always expand to worst opcode *)
    979967      | `WithLabel i ->
    980           let fake_addr _ = `REL (zero `Eight) in
    981           let fake_jump = assembly_jump fake_addr i in
    982           let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
    983            assert (fake_jump = i');
    984            (pc + int_of_vect pc',labels, costs)
     968        let fake_addr _ = `REL (zero `Eight) in
     969        let fake_jump = assembly_jump fake_addr i in
     970        let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
     971        assert (fake_jump = i');
     972        (snd (half_add pc pc'), exit_addr, labels, costs)
    985973      | #instruction as i ->
    986974        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
    987975         assert (i = i');
    988          (pc + int_of_vect pc',labels, costs)
    989    ) (0,StringMap.empty,IntMap.empty) p.ASM.code
     976         (snd (half_add pc pc'),exit_addr,labels, costs)
     977   )
     978    (BitVectors.zero `Sixteen,BitVectors.zero `Sixteen,
     979     StringTools.Map.empty, BitVectors.WordMap.empty) p.ASM.pcode
    990980 in
    991   if pc >= 65536 then
    992    raise CodeTooLarge
    993   else
    994       List.flatten (List.map
    995          (function
    996             `Label _
    997           | `Cost _ -> []
    998           | `WithLabel i ->
    999               let addr_of (`Label s) =
    1000                let addr = StringMap.find s labels in
    1001                (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *)
    1002                 assert (addr < 256);
    1003                 `REL (vect_of_int addr `Eight)
    1004               in
    1005                assembly1 (assembly_jump addr_of i)
    1006           | `Mov (`DPTR,s) ->
    1007               let addrr16 = StringMap.find s datalabels in
    1008                assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
    1009           | `Jmp s ->
    1010               let pc_offset = StringMap.find s labels in
    1011                 assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen)))
    1012           | `Call s ->
    1013               let pc_offset = StringMap.find s labels in
    1014                 assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen)))
    1015           | #instruction as i -> assembly1 i) p.ASM.code),
    1016     vect_of_int (StringMap.find p.ASM.exit_label labels) `Sixteen,
    1017     costs
     981 let code =
     982  List.flatten (List.map
     983     (function
     984        `Label _
     985      | `Cost _ -> []
     986      | `WithLabel i ->
     987          let addr_of (`Label s) =
     988           let addr = StringTools.Map.find s labels in
     989            (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *)
     990            `REL (assert false) (*addr*)
     991          in
     992           assembly1 (assembly_jump addr_of i)
     993      | `Mov (`DPTR,s) ->
     994          let addrr16 = StringTools.Map.find s datalabels in
     995           assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
     996      | `Jmp s ->
     997          let pc_offset = StringTools.Map.find s labels in
     998            assembly1 (`LJMP (`ADDR16 pc_offset))
     999      | `Call s ->
     1000          let pc_offset = StringTools.Map.find s labels in
     1001            assembly1 (`LCALL (`ADDR16 pc_offset ))
     1002      | #instruction as i -> assembly1 i) p.ASM.pcode) in
     1003 { ASM.code = code ; ASM.cost_labels = costs ;
     1004   ASM.exit_addr = exit_addr ; ASM.has_main = p.ASM.phas_main }
    10181005;;
    10191006
    … …  
    10481035          assert false for now. Try to understand what DEC really does *)
    10491036       let cry,addr = half_add dpr (mk_word (vect_of_int 0 `Eight) status.acc) in
    1050          WordMap.find addr status.external_ram
     1037         Physical.WordMap.find addr status.external_ram
    10511038  | `A_PC ->
    10521039       (* CSC: what is the right behaviour in case of overflow?
    10531040          assert false for now *)
    10541041       let cry,addr = half_add status.pc (mk_word (vect_of_int 0 `Eight) status.acc) in
    1055          WordMap.find addr status.external_ram
     1042         Physical.WordMap.find addr status.external_ram
    10561043  | `EXT_INDIRECT b ->
    10571044         let addr = get_register status (false,false,b) in
    1058            WordMap.find (mk_word (zero `Eight) addr) status.external_ram
     1045           Physical.WordMap.find (mk_word (zero `Eight) addr) status.external_ram
    10591046  | `EXT_IND_DPTR ->
    10601047       let dpr = mk_word status.dph status.dpl in
    1061          WordMap.find dpr status.external_ram
     1048         Physical.WordMap.find dpr status.external_ram
    10621049;;
    10631050
    … …  
    11311118      let dpr = mk_word status.dph status.dpl in
    11321119      { status with external_ram =
    1133           WordMap.add dpr v status.external_ram }
     1120          Physical.WordMap.add dpr v status.external_ram }
    11341121    | `EXT_INDIRECT b ->
    11351122      let addr = get_register status (false,false,b) in
    11361123      { status with external_ram =
    1137           WordMap.add (mk_word (zero `Eight) addr) v status.external_ram }
     1124          Physical.WordMap.add (mk_word (zero `Eight) addr) v status.external_ram }
    11381125;;
    11391126
    … …  
    17411728        let dptr = mk_word status.dph status.dpl in
    17421729        let cry, addr = half_add dptr big_acc in
    1743         let lookup = WordMap.find addr status.code_memory in
     1730        let lookup = Physical.WordMap.find addr status.code_memory in
    17441731        { status with acc = lookup }
    17451732      | `MOVC (`A, `A_PC) ->
    … …  
    17501737        let status = { status with pc = inc_pc } in
    17511738        let cry,addr = half_add inc_pc big_acc in
    1752         let lookup = WordMap.find addr status.code_memory in
     1739        let lookup = Physical.WordMap.find addr status.code_memory in
    17531740        { status with acc = lookup }
    17541741      (* data transfer *)
    … …  
    18131800          status
    18141801      | `RET ->
    1815         let high_bits = read_at_sp status in
    1816         let new_sp,cy,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) false in
    1817         let status = { status with sp = new_sp } in
    1818         let low_bits = read_at_sp status in
    1819         let new_sp,_,_,_ = subb8_with_c status.sp (vect_of_int 1 `Eight) cy in
    1820         let status = { status with sp = new_sp } in
    1821         { status with pc = mk_word high_bits low_bits }
    1822 (*
    18231802        (* DPM: What happens when we underflow? *)
    18241803        let high_bits = read_at_sp status in
    … …  
    18291808        let status = { status with sp = new_sp } in
    18301809        { status with pc = mk_word high_bits low_bits }
    1831 *)
    18321810      | `RETI ->
    18331811        let high_bits = read_at_sp status in
    … …  
    18461824        let status = { status with sp = new_sp } in
    18471825        let status = write_at_sp status pc_upper_byte in
    1848         let n1, n2 = from_byte pc_upper_byte in
    1849         let (b1,b2,b3,_) = from_word11 a in
    1850         let (p1,p2,p3,p4),(p5,_,_,_) = from_nibble n1, from_nibble n2 in
    1851         let addr = mk_word (mk_byte (mk_nibble p1 p2 p3 p4) (mk_nibble p5 b1 b2 b3)) pc_lower_byte in
     1826        let addr = addr16_of_addr11 status.pc a in
    18521827        { status with pc = addr }
    18531828      | `LCALL (`ADDR16 addr) ->
    … …  
    18611836        { status with pc = addr }
    18621837      | `AJMP (`ADDR11 a) ->
    1863         let pc_upper_byte, pc_lower_byte = from_word status.pc in
    1864         let n1, n2 = from_byte pc_upper_byte in
    1865         let (p1,p2,p3,p4),(p5,_,_,_) = from_nibble n1, from_nibble n2 in
    1866         let (b1,b2,b3,b) = from_word11 a in
    1867         let addr = mk_word (mk_byte (mk_nibble p1 p2 p3 p4) (mk_nibble p5 b1 b2 b3)) b in
    1868         let cry, new_pc = half_add status.pc addr in
    1869         { status with pc = new_pc }
     1838        let addr = addr16_of_addr11 status.pc a in
     1839        { status with pc = addr }
    18701840      | `LJMP (`ADDR16 a) ->
    18711841        { status with pc = a }
    … …  
    19541924;;
    19551925
    1956 let eq_pc pc1 pc2 =
    1957   let to_int = BitVectors.int_of_vect in
    1958   to_int pc1 = to_int pc2
    1959 
    1960 let end_of_program st = match st.exit_pc with
    1961   | None -> false
    1962   | Some exit_pc -> eq_pc st.pc exit_pc
    1963 
    1964 let print_result st =
    1965   Printf.printf "Result : DPL = %d DPH = %d\n%!"
    1966     (BitVectors.int_of_vect st.dpl) (BitVectors.int_of_vect st.dph)
    1967 
    1968 let print_instr instr =
    1969   Printf.printf "%s\n%!" (ASMPrinter.pp_instruction instr)
     1926
     1927let load_program p =
     1928  let st = load p.ASM.code initialize in
     1929  { st with exit_addr = p.ASM.exit_addr ; cost_labels = p.ASM.cost_labels }
    19701930
    19711931let observe_trace trace_ref st =
    1972   let pc = st.pc in
    1973   let (instr, _, _) = fetch st.code_memory pc in
    1974   let ipc = BitVectors.int_of_vect pc in
    1975   (* <DEBUG> *)
    1976   print_result st ;
    1977   Printf.printf "%d: %!" ipc ;
    1978   print_instr instr ;
    1979   (* </DEBUG> *)
    19801932  let cost_label =
    1981     if IntMap.mem ipc st.costs then [IntMap.find ipc st.costs]
     1933    if BitVectors.WordMap.mem st.pc st.cost_labels then
     1934      [BitVectors.WordMap.find st.pc st.cost_labels]
    19821935    else [] in
    19831936  trace_ref := cost_label @ !trace_ref ;
    1984   if end_of_program st then raise Halt else st
    1985 
    1986 let interpret p =
     1937  if st.pc = st.exit_addr (* <=> end of program *) then raise Halt else st
     1938
     1939let result st =
     1940  let i = BitVectors.int_of_vect st.dpl in
     1941  IntValue.Int8.of_int i
     1942
     1943let interpret print_result p =
    19871944  if p.ASM.has_main then
    1988     let (insts, exit_pc, costs) = assembly p in
    1989     let st = load insts (Some exit_pc) costs initialize in
     1945    let st = load_program p in
    19901946    let trace = ref [] in
    19911947    let callback = observe_trace trace in
    19921948    let st = execute callback st in
    1993     (* <DEBUG> *)
    1994     print_result st ;
    1995     (* </DEBUG> *)
    1996     List.rev !trace
    1997   else []
    1998 
    1999 let parse_and_interpret_hex file =
    2000   let intel_hex = IntelHex.intel_hex_of_file file in
    2001   let physical = IntelHex.process_intel_hex intel_hex in
    2002   let st = load_mem physical None IntMap.empty initialize in
    2003   let callback = observe_trace (ref []) in
    2004   ignore (execute callback st)
     1949    let res = result st in
     1950    if print_result then
     1951      Printf.printf "8051: %s\n%!" (IntValue.Int8.to_string res) ;
     1952    (res, List.rev !trace)
     1953  else (IntValue.Int8.zero, [])

  • Deliverables/D2.2/8051/src/ASM/ASMInterpret.mli

    r486 r619  
    33
    44exception CodeTooLarge
    5 
     5 
    66type time = int;;
    77type line = [ `P1 of byte
    … …  
    1818(* In:  reception time, line of input, new continuation,
    1919   Out: transmission time, output line, expected duration until reply,
    20         new continuation.
     20   new continuation.
    2121*)
    2222type continuation =
    2323  [`In of time * line * epsilon * continuation] option *
    24   [`Out of (time -> line -> time * continuation) ];;
    25 
    26 module IntMap: Map.S with type key = int
    27 type costs = CostLabel.t IntMap.t
     24    [`Out of (time -> line -> time * continuation) ];;
    2825
    2926type status =
    30 {
    31   (* Memory *)
    32   code_memory: WordMap.map;        (* can be reduced *)
    33   low_internal_ram: Byte7Map.map;
    34   high_internal_ram: Byte7Map.map;
    35   external_ram: WordMap.map;
     27    {
     28      (* Memory *)
     29      code_memory: WordMap.map;        (* can be reduced *)
     30      low_internal_ram: Byte7Map.map;
     31      high_internal_ram: Byte7Map.map;
     32      external_ram: WordMap.map;
     33     
     34      (* Program counter *)
     35      pc: word;
     36     
     37      (* SFRs *)
     38      sp: byte;
     39      dpl: byte;
     40      dph: byte;
     41      pcon: byte;
     42      tcon: byte;
     43      tmod: byte;
     44      tl0: byte;
     45      tl1: byte;
     46      th0: byte;
     47      th1: byte;
     48      p1: byte;
     49      scon: byte;
     50      sbuf: byte;
     51      ie: byte;
     52      p3: byte;
     53      ip: byte;
     54      psw: byte;
     55      acc: byte;
     56      b: byte;
     57      t2con: byte;   (* 8052 only *)
     58      rcap2l: byte;  (* 8052 only *)
     59      rcap2h: byte;  (* 8052 only *)
     60      tl2: byte;     (* 8052 only *)
     61      th2: byte;     (* 8052 only *)
     62     
     63      (* Latches for the output lines *)
     64      p1_latch: byte;
     65      p3_latch: byte;
     66     
     67      (* Fields for tracking the state of the processor. *)
     68     
     69      (* IO specific *)
     70      previous_p1_val: bool;
     71      previous_p3_val: bool;
     72     
     73      serial_epsilon_out: epsilon option;
     74      serial_epsilon_in: epsilon option;
     75     
     76      io_epsilon: epsilon;
     77     
     78      serial_v_in: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option;
     79      serial_v_out: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option;
     80     
     81      serial_k_out: continuation option;
     82     
     83      io: continuation;
     84      expected_out_time: [ `None | `Now | `At of time ];
     85     
     86      (* Timer and clock specific *)
     87      clock: time;
     88      timer0: word;
     89      timer1: word;
     90      timer2: word;  (* can be missing *)
     91     
     92      esi_running: bool;
     93      t0i_running: bool;
     94      t1i_running: bool;
     95      e0i_running: bool;
     96      e1i_running: bool;
     97      es_running: bool;
    3698
    37   (* Program counter *)
    38   pc: word;
    39 
    40   (* SFRs *)
    41   sp: byte;
    42   dpl: byte;
    43   dph: byte;
    44   pcon: byte;
    45   tcon: byte;
    46   tmod: byte;
    47   tl0: byte;
    48   tl1: byte;
    49   th0: byte;
    50   th1: byte;
    51   p1: byte;
    52   scon: byte;
    53   sbuf: byte;
    54   ie: byte;
    55   p3: byte;
    56   ip: byte;
    57   psw: byte;
    58   acc: byte;
    59   b: byte;
    60   t2con: byte;   (* 8052 only *)
    61   rcap2l: byte;  (* 8052 only *)
    62   rcap2h: byte;  (* 8052 only *)
    63   tl2: byte;     (* 8052 only *)
    64   th2: byte;     (* 8052 only *)
    65 
    66   (* Latches for the output lines *)
    67   p1_latch: byte;
    68   p3_latch: byte;
    69 
    70   (* Fields for tracking the state of the processor. *)
    71  
    72   (* IO specific *)
    73   previous_p1_val: bool;
    74   previous_p3_val: bool;
    75 
    76   serial_epsilon_out: epsilon option;
    77   serial_epsilon_in: epsilon option;
    78 
    79   io_epsilon: epsilon;
    80 
    81   serial_v_in: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option;
    82   serial_v_out: [`Eight of byte | `Nine of (BitVectors.bit * byte) ] option;
    83 
    84   serial_k_out: continuation option;
    85 
    86   io: continuation;
    87   expected_out_time: [ `None | `Now | `At of time ];
    88 
    89   (* Timer and clock specific *)
    90   clock: time;
    91   timer0: word;
    92   timer1: word;
    93   timer2: word;  (* can be missing *)
    94 
    95   esi_running: bool;
    96   t0i_running: bool;
    97   t1i_running: bool;
    98   e0i_running: bool;
    99   e1i_running: bool;
    100   es_running: bool;
    101 
    102   exit_pc: word option;
    103   costs: costs;
    104 }
    105 
     99      exit_addr   : BitVectors.word;
     100      cost_labels : string BitVectors.WordMap.t
     101    }
     102     
    106103val string_of_status: status -> string
    107104
    108 val assembly: ASM.program -> BitVectors.byte list (*ASM.instruction list * symbol_table *) * word (* exit pc *) * string IntMap.t
     105
     106val assembly:
     107  [< ASM.labelled_instruction] ASM.pretty_program -> ASM.program
    109108
    110109(*
    111 val link:
    112  (ASM.instruction list * symbol_table * cost_map) list -> BitVectors.byte list
     110  val link:
     111  (ASM.instruction list * symbol_table * cost_map) list -> BitVectors.byte list
    113112*)
    114 
     113 
    115114val initialize: status
    116 
    117 val load_mem: Physical.WordMap.map -> word option -> costs -> status -> status
    118 val load: BitVectors.byte list -> word option -> costs -> status -> status
    119 
     115 
     116val load_code_memory: BitVectors.byte list -> Physical.WordMap.map
     117val load_mem: Physical.WordMap.map -> status -> status
     118val load: BitVectors.byte list -> status -> status
     119 
    120120exception Halt  (* to be raised to stop execution *)
    121 
     121 
    122122(* the callback function is used to observe the execution
    123123   trace; it can raise Hold to stop execution. Otherwise
    124124   the processor never halts. *)
    125125val execute: (status -> unit) -> status -> status
    126 
     126 
    127127val fetch: Physical.WordMap.map -> word -> ASM.instruction * word * int
    128128
    129 val interpret : ASM.program -> AST.trace
    130 
    131 val parse_and_interpret_hex : string -> unit
     129val load_program : ASM.program -> status
     130val interpret    : bool -> ASM.program -> AST.trace

  • Deliverables/D2.2/8051/src/ASM/ASMPrinter.ml

    r486 r619  
    1 open BitVectors;;
    2 open ASM;;
    31
    4 let pp_arg =
    5  function
    6     `A -> "A"
    7   | `B -> "B"
    8   | `C -> "C"
    9   | `DPTR -> "DPTR"
    10   | `ADDR11 x -> hex_string_of_vect x
    11   | `ADDR16 x -> hex_string_of_vect x
    12   | `DATA x -> "#0" ^ hex_string_of_vect x ^ "h"
    13   | `DATA16 x -> "#0" ^ hex_string_of_vect x ^ "h"
    14   | `BIT x -> "bit " ^ hex_string_of_vect (x: byte)
    15   | `NBIT x -> "nbit " ^ hex_string_of_vect (x: byte)
    16   | `REG (r1, r2, r3) -> "R" ^ string_of_int (int_of_vect (mk_nibble false r1 r2 r3))
    17   | `REL x -> hex_string_of_vect x
    18   | `A_DPTR -> "@DPTR"
    19   | `A_PC -> "@PC"
    20   | `DIRECT x -> "0" ^ (hex_string_of_vect (x: byte)) ^ "h"
    21   | `EXT_INDIRECT x -> "ext_indirect " ^ string_of_bool x
    22   | `EXT_IND_DPTR -> "@DPTR"
    23 (* DPM: weird: this seems to be reversed in mcu8051ide: change made. *)
    24   | `INDIRECT x -> if not x then "@R0" else "@R1"
    25   | `IND_DPTR -> "@DPTR"
    26   | `Label s -> s
    27 ;;
    28 
    29 let pp_jump =
    30  function
    31     `CJNE (`U1 (a1,a2),a3) -> "cjne " ^ pp_arg a1 ^ ", " ^ pp_arg a2 ^ ", " ^ pp_arg a3
    32   | `CJNE (`U2 (a1,a2),a3) -> "cjne " ^ pp_arg a1 ^ ", " ^ pp_arg a2 ^ ", " ^ pp_arg a3
    33   | `DJNZ (a1,a2) -> "djnz " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    34   | `JB (a1,a2) -> "jb " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    35   | `JBC (a1,a2) -> "jbc " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    36   | `JC a1 -> "jc " ^ pp_arg a1
    37   | `JNB (a1,a2) -> "jnb " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    38   | `JNC a1 -> "jnc " ^ pp_arg a1
    39   | `JNZ a1 -> "jnz " ^ pp_arg a1
    40   | `JZ a1 -> "jz  " ^ pp_arg a1
    41 
    42 let pp_instruction =
    43  function
    44     `Label l -> l ^ ":"
    45   | `Cost l -> l ^ ":"
    46   | `Jmp j -> "ljmp " ^ j
    47   | `Call j -> "lcall " ^ j
    48   | `WithLabel i -> pp_jump i
    49   | `Begin_fun -> "\n; Begin function"
    50   | `End_fun -> "; End function\n"
    51   |  (#jump as i) -> pp_jump i
    52   | `Mov (a1,a2) -> "mov " ^ pp_arg a1 ^ ", " ^ a2
    53   | `ACALL a1 -> "acall " ^ pp_arg a1
    54   | `ADD (a1,a2) -> "add " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    55   | `ADDC (a1,a2) -> "addc " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    56   | `AJMP a1 -> "ajmp " ^ pp_arg a1
    57   | `ANL (`U1 (a1,a2)) -> "anl " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    58   | `ANL (`U2 (a1,a2)) -> "anl " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    59   | `ANL (`U3 (a1,a2)) -> "anl " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    60   | `CLR a1 -> "clr " ^ pp_arg a1
    61   | `CPL a1 -> "cpl " ^ pp_arg a1
    62   | `DA a1 -> "da " ^ pp_arg a1
    63   | `DEC a1 -> "dec " ^ pp_arg a1
    64   | `DIV (a1,a2) -> "div AB"
    65   | `INC a1 -> "inc " ^ pp_arg a1
    66   | `JMP a1 -> "jmp " ^ pp_arg a1
    67   | `LCALL a1 -> "lcall " ^ pp_arg a1
    68   | `LJMP a1 -> "ljmp " ^ pp_arg a1
    69   | `MOV (`U1 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    70   | `MOV (`U2 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    71   | `MOV (`U3 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    72   | `MOV (`U4 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    73   | `MOV (`U5 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    74   | `MOV (`U6 (a1,a2)) -> "mov " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    75   | `MOVC (a1,a2) -> "movc " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    76   | `MOVX (`U1 (a1,a2)) -> "movx " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    77   | `MOVX (`U2 (a1,a2)) -> "movx " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    78   | `MUL(a1, a2) -> "mul AB"
    79   | `NOP -> "nop"
    80   | `ORL (`U1(a1,a2)) -> "orl " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    81   | `ORL (`U2(a1,a2)) -> "orl " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    82   | `ORL (`U3(a1,a2)) -> "orl " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    83   | `POP a1 -> "pop " ^ pp_arg a1
    84   | `PUSH a1 -> "push " ^ pp_arg a1
    85   | `RET -> "ret"
    86   | `RETI -> "reti"
    87   | `RL a1 -> "rl " ^ pp_arg a1
    88   | `RLC a1 -> "rlc " ^ pp_arg a1
    89   | `RR a1 -> "rr " ^ pp_arg a1
    90   | `RRC a1 -> "rrc " ^ pp_arg a1
    91   | `SETB a1 -> "setb " ^ pp_arg a1
    92   | `SJMP a1 -> "sjmp " ^ pp_arg a1
    93   | `SUBB (a1,a2) -> "subb " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    94   | `SWAP a1 -> "swap " ^ pp_arg a1
    95   | `XCH (a1,a2) -> "xch " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    96   | `XCHD(a1,a2) -> "xchd " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    97   | `XRL(`U1(a1,a2)) -> "xrl " ^ pp_arg a1 ^ ", " ^ pp_arg a2
    98   | `XRL(`U2(a1,a2)) -> "xrl " ^ pp_arg a1 ^ ", " ^ pp_arg a2
     2(** This module provides a function to print [ASM] programs. *)
    993
    1004let print_program p =
    101   let f s i = Printf.sprintf "%s%s\n" s (pp_instruction i) in
    102   "Org 0\n\n" ^ (List.fold_left f "" p.ASM.code) ^ "\nEND\n"
     5  let code_memory = ASMInterpret.load_code_memory p.ASM.code in
     6  let intel_hex = IntelHex.pack_exported_code_memory 16 65536 code_memory in
     7  IntelHex.string_of_intel_hex_format intel_hex

  • Deliverables/D2.2/8051/src/ASM/ASMPrinter.mli

    r486 r619  
    1 val pp_arg:
    2     [< `A
    3      | `ADDR11 of 'a BitVectors.vect
    4      | `ADDR16 of 'b BitVectors.vect
    5      | `A_DPTR
    6      | `A_PC
    7      | `B
    8      | `BIT of BitVectors.byte
    9      | `C
    10      | `DATA of 'c BitVectors.vect
    11      | `DATA16 of 'd BitVectors.vect
    12      | `DIRECT of BitVectors.byte
    13      | `DPTR
    14      | `EXT_INDIRECT of bool
    15      | `EXT_IND_DPTR
    16      | `INDIRECT of bool
    17      | `IND_DPTR
    18      | `NBIT of BitVectors.byte
    19      | `REG of BitVectors.bit * BitVectors.bit * BitVectors.bit
    20      | `REL of 'e BitVectors.vect ] -> string
    21 val pp_instruction: [< ASM.labelled_instruction] -> string
     1
     2(** This module provides a function to print [ASM] programs. *)
    223
    234val print_program : ASM.program -> string

  • Deliverables/D2.2/8051/src/ASM/BitVectors.ml

    r486 r619  
    155155(* CSC: only works properly with bytes!!! *)
    156156let hex_string_of_vect v = Printf.sprintf "%0 2X" (int_of_vect v);;
     157
     158module WordMap =
     159  Map.Make (struct type t = word let compare = compare end);;

  • Deliverables/D2.2/8051/src/ASM/BitVectors.mli

    r486 r619  
    5454val shift_right : 'a vect -> 'a vect
    5555val shift_left : 'a vect -> 'a vect
     56
     57module WordMap: Map.S with type key = word

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

    r486 r619  
    4444    | Mul -> Val.mul
    4545    | Divu -> Val.divu
    46     | Modu -> Val.modu
     46    | Modu -> Val.modulou
    4747
    4848  let op1 = function
    … …  
    5757      (res2, Val.or_op of1 of2)
    5858    | Sub ->
    59       let (res1, uf1) = Val.sub_and_of v1 v2 in
    60       let (res2, uf2) = Val.sub_and_of res1 carry in
     59      let (res1, uf1) = Val.sub_and_uf v1 v2 in
     60      let (res2, uf2) = Val.sub_and_uf res1 carry in
    6161      (res2, Val.or_op uf1 uf2)
    6262    | And -> (Val.and_op v1 v2, carry)

  • Deliverables/D2.2/8051/src/ASM/IntelHex.ml

    r486 r619  
    33open Util;;
    44open Parser;;
     5open Printf;;
    56
    67exception WrongFormat of string
    … …  
    3233    | '9' -> 9 | 'A' -> 10 | 'B' -> 11
    3334    | 'C' -> 12 | 'D' -> 13 | 'E' -> 14
    34     | 'F' -> 15 | _ -> assert false
     35    | 'F' -> 15 | 'a' -> 10 | 'b' -> 11
     36    | 'c' -> 12 | 'd' -> 13 | 'e' -> 14
     37    | 'f' -> 15 | _ -> assert false
    3538
    3639let intel_hex_entry_type_of_int =
    … …  
    9396    aux (false, (vect_of_int 0 `Eight)) r
    9497
    95 let checksum_valid hex_entry =
     98let calculate_checksum hex_entry =
    9699 let ty = (flip vect_of_int $ `Eight) $ int_of_intel_hex_entry_type hex_entry.record_type in
    97100 let addr1,addr2 = from_word hex_entry.record_addr in
    98101 let _, total = add_bytes (hex_entry.record_length :: addr1 :: addr2 :: ty :: hex_entry.data_field) in
    99102 let _,total = half_add (vect_of_int 1 `Eight) $ complement total in
    100    hex_entry.data_checksum = total
    101 
     103  total
     104
     105let checksum_valid hex_entry =
     106  let total = calculate_checksum hex_entry in
     107    hex_entry.data_checksum = total
    102108
    103109let prs_intel_hex_record =
    … …  
    135141let string_of_intel_hex_entry entry =
    136142  let length_string = hex_string_of_vect entry.record_length in
    137   let addr_string = hex_string_of_vect entry.record_addr in
    138   let checksum_string = hex_string_of_vect entry.data_checksum in
    139   let type_string = Printf.sprintf "%0 2d" (int_of_intel_hex_entry_type entry.record_type) in
     143  let addr_string = Printf.sprintf "%04X" (int_of_vect entry.record_addr) in
     144  let checksum_string = Printf.sprintf "%02X" (int_of_vect entry.data_checksum) in
     145  let type_string = Printf.sprintf "%02d" (int_of_intel_hex_entry_type entry.record_type) in
    140146  let data_string = String.concat "" (List.map hex_string_of_vect entry.data_field) in
    141147    ":" ^ length_string ^ addr_string ^ type_string ^ data_string ^ checksum_string
    … …  
    188194  aux Physical.WordMap.empty
    189195;;
     196
     197(* DPM: this needs some comment:
     198     We aim to extract code memory into segmented lists of bytes, with a maximum
     199     length (chunk_size).  The code memory map has a fixed size (max_addressable)
     200     on the 8051.  Further, the chunks we extract get segmented when we find an
     201     unitialized zone in the code memory.
     202*)
     203let export_code_memory chunk_size max_addressable code_mem =
     204  let rec aux chunk address start_address rbuff lbuff =
     205    if address = max_addressable then
     206      (start_address, List.rev rbuff)::lbuff
     207    else if chunk = 0 then
     208      aux chunk_size address address [] ((start_address, List.rev rbuff)::lbuff)
     209    else
     210      let code = Physical.WordMap.find (vect_of_int address `Sixteen) code_mem in
     211        aux (chunk - 1) (address + 1) start_address (code::rbuff) lbuff
     212  in
     213    List.rev (aux chunk_size 0 0 [] [])
     214;;
     215
     216let clean_exported_code_memory = List.filter (fun x -> snd x <> [])
     217;;
     218
     219let calculate_data_checksum (record_length, record_addr, record_type, data_field) =
     220  let ty = (flip vect_of_int $ `Eight) $ int_of_intel_hex_entry_type record_type in
     221  let addr1,addr2 = from_word record_addr in
     222  let _, total = add_bytes (record_length :: addr1 :: addr2 :: ty :: data_field) in
     223  let _,total = half_add (vect_of_int 0 `Eight) $ complement total in
     224    total
     225;;
     226
     227let process_exported_code_memory =
     228  List.map (fun x ->
     229    let record_length = vect_of_int (List.length (snd x)) `Eight in
     230    let record_addr = vect_of_int (fst x) `Sixteen in
     231    let record_type = Data in
     232    let data_field = snd x in
     233    let temp_record =
     234      { record_length = record_length;
     235        record_addr = record_addr;
     236        record_type = record_type;
     237        data_field = data_field;
     238        data_checksum = zero `Eight
     239      } in
     240    { temp_record with data_checksum = calculate_checksum temp_record })
     241;;
     242
     243let pack_exported_code_memory chunk_size max_addressable code_mem =
     244  let export = export_code_memory chunk_size max_addressable code_mem in
     245  let cleaned = clean_exported_code_memory export in
     246  let processed = process_exported_code_memory cleaned in
     247  let end_buffer =
     248    [{ record_length = zero `Eight;
     249      record_addr = zero `Sixteen;
     250      record_type = End;
     251      data_field = [];
     252      data_checksum = vect_of_int 255 `Eight
     253    }] in
     254    processed @ end_buffer
     255;;
     256
     257let file_of_intel_hex path fmt =
     258  let str_fmt = string_of_intel_hex_format fmt in
     259  let channel = open_out path in
     260    fprintf channel "%s\n" str_fmt;
     261    close_out channel
     262;;

  • Deliverables/D2.2/8051/src/ASM/IntelHex.mli

    r486 r619  
    1111
    1212val intel_hex_of_file: string -> intel_hex_format
     13val file_of_intel_hex: string -> intel_hex_format -> unit
    1314val process_intel_hex: intel_hex_format -> Physical.WordMap.map
     15
     16val pack_exported_code_memory: int -> int -> Physical.WordMap.map -> intel_hex_format
     17val file_of_intel_hex: string -> intel_hex_format -> unit

  • Deliverables/D2.2/8051/src/ASM/Parser.ml

    r486 r619  
    8484       x = '4' || x = '5' || x = '6' || x = '7' ||
    8585       x = '8' || x = '9' || x = 'A' || x = 'B' ||
    86        x = 'C' || x = 'D' || x = 'E' || x = 'F')
     86       x = 'C' || x = 'D' || x = 'E' || x = 'F' ||
     87       x = 'a' || x = 'b' || x = 'c' || x = 'd' ||
     88       x = 'e' || x = 'f')
    8789

  • Deliverables/D2.2/8051/src/ASM/Physical.ml

    r486 r619  
    1010   val find : key -> map -> byte
    1111   val add : key -> byte -> map -> map
     12   val fold : (key -> byte -> 'b -> 'b) -> map -> 'b -> 'b
     13   val equal: (byte -> byte -> bool) -> map -> map -> bool
    1214 end
    1315;;
    … …  
    2123      find k m
    2224    with Not_found -> zero `Eight
     25  let fold = fold
     26  let equal = equal
    2327end;;
    2428
    … …  
    3135      find k m
    3236    with Not_found -> zero `Eight
     37  let fold = fold
     38  let equal = equal
    3339end;;
    3440
    … …  
    97103  | _ -> assert false
    98104;;
     105
     106let addr16_of_addr11 pc a =
     107 let pc_upper, _ = from_word pc in
     108 let n1, n2 = from_byte pc_upper in
     109 let (b1,b2,b3,b) = from_word11 a in
     110 let (p1,p2,p3,p4),(p5,_,_,_) = from_nibble n1, from_nibble n2 in
     111  mk_word (mk_byte (mk_nibble p1 p2 p3 p4) (mk_nibble p5 b1 b2 b3)) b
     112;;

  • Deliverables/D2.2/8051/src/ASM/Physical.mli

    r486 r619  
    1010   val find : key -> map -> byte
    1111   val add : key -> byte -> map -> map
     12   val fold : (key -> byte -> 'b -> 'b) -> map -> 'b -> 'b
     13   val equal: (byte -> byte -> bool) -> map -> map -> bool
    1214 end
    1315;;
    … …  
    2628val dec: byte -> byte (* with roll-over *)
    2729val inc: byte -> byte (* with roll-over *)
     30
     31val addr16_of_addr11: word -> word11 -> word

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

    r486 r619  
    5555      renv   : hdw_reg_env ;
    5656      mem    : memory ;
    57       trace  : AST.trace }
     57      trace  : CostLabel.t list }
    5858
    5959
    … …  
    448448    (Val.to_string st.pc) (current_label lbls_offs st) ;
    449449  Printf.printf "SP: %s\n%!"
    450     (Val.to_string (Val.merge [I8051.RegisterMap.find I8051.sph st.renv ;
    451                                I8051.RegisterMap.find I8051.spl st.renv])) ;
     450    (Val.to_string (Val.merge [get_reg (Hdw I8051.sph) st ;
     451                               get_reg (Hdw I8051.spl) st])) ;
    452452  Printf.printf "ISP: %s%!" (Val.to_string st.isp) ;
    453453  print_lenv st.lenv ;
    … …  
    456456  Printf.printf "\n%!"
    457457
    458 let rec iter_small_step lbls_offs st = match fetch_stmt lbls_offs st with
    459   | ERTL.St_return ret_regs when st.st_frs = [] ->
    460 (*
    461     print_state lbls_offs st ;
    462     let res = fetch_result st.renv ret_regs in
    463     Printf.printf "Return: %s\n%!" (Val.to_string res) ;
    464 *)
    465     List.rev st.trace
    466   | stmt ->
    467 (*
    468     print_state lbls_offs st ;
    469 *)
    470     let st' = interpret_stmt lbls_offs st stmt in
    471     iter_small_step lbls_offs st'
     458let compute_result st ret_regs =
     459  try
     460    let v = get_reg (Psd (MiscPottier.last ret_regs)) st in
     461    if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
     462    else IntValue.Int8.zero
     463  with Not_found -> IntValue.Int8.zero
     464
     465let rec iter_small_step print_result lbls_offs st =
     466  match fetch_stmt lbls_offs st with
     467    | ERTL.St_return ret_regs when st.st_frs = [] ->
     468      let (res, cost_labels) as trace =
     469        (compute_result st ret_regs, List.rev st.trace) in
     470      if print_result then
     471        Printf.printf "ERTL: %s\n%!" (IntValue.Int8.to_string res) ;
     472      trace
     473    | stmt ->
     474    (*
     475      print_state lbls_offs st ;
     476    *)
     477      let st' = interpret_stmt lbls_offs st stmt in
     478      iter_small_step print_result lbls_offs st'
    472479
    473480
    … …  
    530537   - Initialize the carry flag to 0. *)
    531538
    532 let interpret p = match p.ERTL.main with
    533   | None -> []
     539let interpret print_result p = match p.ERTL.main with
     540  | None -> (IntValue.Int8.zero (* TODO *), [])
    534541  | Some main ->
    535542    let lbls_offs = labels_offsets p in
    … …  
    541548    let st = init_main_call lbls_offs st main in
    542549    let st = change_carry st Val.zero in
    543     iter_small_step lbls_offs st
     550    iter_small_step print_result lbls_offs st

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

    r486 r619  
    22(** This module provides an interpreter for the [ERTL] language. *)
    33
    4 val interpret : ERTL.program -> AST.trace
     4val interpret : bool -> ERTL.program -> AST.trace

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

    r486 r619  
    4242      renv   : hdw_reg_env ;
    4343      mem    : memory ;
    44       trace  : AST.trace }
     44      trace  : CostLabel.t list }
    4545
    4646
    … …  
    195195  match Mem.find_fun_def st.mem ptr with
    196196    | LIN.F_int def ->
    197 (*
    198       Printf.printf "Pushing return address in IRAM: %s\n%!"
    199         (Val.to_string (next_pc st).pc) ;
    200 *)
    201197      let st = save_ra st in
    202198      init_fun_call st ptr
    … …  
    205201let interpret_return st =
    206202  let pc = return_pc st in
    207 (*
    208   Printf.printf "Returning to %s\n%!" (Val.to_string pc) ;
    209 *)
    210203  change_pc st pc
    211204
    … …  
    328321  Printf.printf "\n%!"
    329322
    330 let print_result st =
    331   let string_of_reg r = Val.to_string (get_reg r st) in
    332   Printf.printf "DPH: %s - DPL: %s\n%!"
    333     (string_of_reg I8051.dph) (string_of_reg I8051.dpl)
    334 
    335 let rec iter_small_step st =
     323let compute_result st =
     324  let v = get_reg I8051.dpl st in
     325  if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
     326  else IntValue.Int8.zero
     327
     328let rec iter_small_step print_result st =
    336329(*
     330  (* <DEBUG> *)
    337331  print_state st ;
     332  (* </DEBUG> *)
    338333*)
    339334  match fetch_stmt st with
    340335    | LIN.St_return when Val.eq (return_pc st) Val.zero ->
    341 (*
    342       print_state st ;
    343       print_result st ;
    344 *)
    345       List.rev st.trace
     336      let (res, cost_labels) as trace =
     337        (compute_result st, List.rev st.trace) in
     338      if print_result then
     339        Printf.printf "LIN: %s\n%!" (IntValue.Int8.to_string res) ;
     340      trace
    346341    | stmt ->
    347342      let st' = interpret_stmt st stmt in
    348       iter_small_step st'
     343      iter_small_step print_result st'
    349344
    350345
    … …  
    406401   - Initialize the carry flag to 0. *)
    407402
    408 let interpret p = match p.LIN.main with
    409   | None -> []
     403let interpret print_result p = match p.LIN.main with
     404  | None -> (IntValue.Int8.zero, [])
    410405  | Some main ->
    411406    let st = empty_state in
    … …  
    416411    let st = init_main_call st main in
    417412    let st = change_carry st Val.zero in
    418     iter_small_step st
     413    iter_small_step print_result st

  • Deliverables/D2.2/8051/src/LIN/LINInterpret.mli

    r486 r619  
    33    return the trace of cost labels encountered. *)
    44
    5 val interpret: LIN.program -> AST.trace
     5val interpret: bool -> LIN.program -> AST.trace

  • Deliverables/D2.2/8051/src/LIN/LINToASM.ml

    r486 r619  
    129129
    130130
    131 (* Move the first cost label of each function at the beginning of the
    132    function. Indeed, some preamble instructions (such as frame creation) might
    133    get in the way.  *)
    134 
    135 let move_first_cost_label_up_code =
    136   let rec aux preamble = function
    137     | [] -> preamble
    138     | LIN.St_cost lbl :: code -> LIN.St_cost lbl :: preamble @ code
    139     | inst :: code -> aux (preamble @ [inst]) code
    140   in aux []
    141 
    142 let move_first_cost_label_up_funct (id, def) =
    143   let def' = match def with
    144     | LIN.F_int int_def -> LIN.F_int (move_first_cost_label_up_code int_def)
    145     | _ -> def in
    146   (id, def')
    147 
    148 let move_first_cost_label_up p =
    149   { p with LIN.functs = List.map move_first_cost_label_up_funct p.LIN.functs }
    150 
    151 
    152131(* Translating programs.
    153132
    … …  
    165144  let tmp_universe = Label.Gen.new_universe fresh_tmp in
    166145  let glbls_addr = globals_addr p.LIN.vars in
    167   { ASM.preamble = p.LIN.vars ;
    168     ASM.exit_label = exit_label ;
    169     ASM.code =
    170       translate_functs tmp_universe glbls_addr exit_label p.LIN.main
    171         p.LIN.functs ;
    172     ASM.has_main = p.LIN.main <> None }
     146  let p =
     147    { ASM.ppreamble = p.LIN.vars ;
     148      ASM.pexit_label = exit_label ;
     149      ASM.pcode =
     150        translate_functs tmp_universe glbls_addr exit_label p.LIN.main
     151          p.LIN.functs ;
     152      ASM.phas_main = p.LIN.main <> None } in
     153  ASMInterpret.assembly p

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

    r486 r619  
    4545      renv   : hdw_reg_env ;
    4646      mem    : memory ;
    47       trace  : AST.trace }
     47      trace  : CostLabel.t list }
    4848
    4949
    … …  
    371371    (string_of_reg I8051.dph) (string_of_reg I8051.dpl)
    372372
    373 let rec iter_small_step lbls_offs st =
     373let compute_result st =
     374  let v = get_reg I8051.dpl st in
     375  if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
     376  else IntValue.Int8.zero
     377
     378let rec iter_small_step print_result lbls_offs st =
    374379(*
    375380    print_state lbls_offs st ;
    … …  
    377382  match fetch_stmt lbls_offs st with
    378383    | LTL.St_return when Val.eq (return_pc st) Val.zero ->
    379 (*
    380       print_state lbls_offs st ;
    381       print_result st ;
    382 *)
    383       List.rev st.trace
     384      let (res, cost_labels) as trace =
     385        (compute_result st, List.rev st.trace) in
     386      if print_result then
     387        Printf.printf "LTL: %s\n%!" (IntValue.Int8.to_string res) ;
     388      trace
    384389    | stmt ->
    385390      let st' = interpret_stmt lbls_offs st stmt in
    386       iter_small_step lbls_offs st'
     391      iter_small_step print_result lbls_offs st'
    387392
    388393
    … …  
    446451   - Initialize the carry flag to 0. *)
    447452
    448 let interpret p = match p.LTL.main with
    449   | None -> []
     453let interpret print_result p = match p.LTL.main with
     454  | None -> (IntValue.Int8.zero, [])
    450455  | Some main ->
    451456    let lbls_offs = labels_offsets p in
    … …  
    457462    let st = init_main_call lbls_offs st main in
    458463    let st = change_carry st Val.zero in
    459     iter_small_step lbls_offs st
     464    iter_small_step print_result lbls_offs st

  • Deliverables/D2.2/8051/src/LTL/LTLInterpret.mli

    r486 r619  
    33    return the trace of cost labels encountered. *)
    44
    5 val interpret: LTL.program -> AST.trace
     5val interpret: bool -> LTL.program -> AST.trace

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

    r486 r619  
    4141type state =
    4242  | State of stack_frame list * RTL.graph * Label.t * Val.t (* sp *) *
    43              local_env * Val.t (* carry *) * memory * AST.trace
     43             local_env * Val.t (* carry *) * memory * CostLabel.t list
    4444  | CallState of stack_frame list * RTL.function_def *
    45                  Val.t list (* args *) * memory * AST.trace
     45                 Val.t list (* args *) * memory * CostLabel.t list
    4646  | ReturnState of stack_frame list * Val.t list (* return values *) *
    47                    memory * AST.trace
     47                   memory * CostLabel.t list
    4848
    4949
    … …  
    101101    (mem   : memory)
    102102    (stmt  : RTL.statement)
    103     (t     : AST.trace) :
     103    (t     : CostLabel.t list) :
    104104    state = match stmt with
    105105
    … …  
    269269    (args  : Val.t list)
    270270    (mem   : memory)
    271     (t     : AST.trace) :
     271    (t     : CostLabel.t list) :
    272272    state =
    273273  match f_def with
    … …  
    286286    (ret_vals : Val.t list)
    287287    (mem      : memory)
    288     (t        : AST.trace) :
     288    (t        : CostLabel.t list) :
    289289    state =
    290290  let f i lenv r = Register.Map.add r (List.nth ret_vals i) lenv in
    … …  
    311311    (Register.print r) (Val.to_string v))
    312312
    313 let rec iter_small_step st = match small_step st with
     313let compute_result vs =
     314  try
     315    let v = MiscPottier.last vs in
     316    if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
     317    else IntValue.Int8.zero
     318  with Not_found -> IntValue.Int8.zero
     319
     320let rec iter_small_step print_result st = match small_step st with
    314321(*
     322  (* <DEBUG> *)
    315323  | ReturnState ([], vs, mem, t) ->
    316324    Mem.print mem ;
    … …  
    331339    Printf.printf "Carry = %s\n\n%!" (Val.to_string carry) ;
    332340    iter_small_step st'
     341  (* </DEBUG> *)
    333342*)
    334343  | ReturnState ([], vs, mem, t) ->
    335 (*
    336     Printf.printf "Return: %s\n%!" (print_ret_vals vs) ;
    337 *)
    338     List.rev t
    339   | st' -> iter_small_step st'
     344    let (res, cost_labels) as trace = (compute_result vs, List.rev t) in
     345    if print_result then
     346      Printf.printf "RTL: %s\n%!" (IntValue.Int8.to_string res) ;
     347    trace
     348  | st' -> iter_small_step print_result st'
    340349
    341350
    … …  
    357366(* Interpret the program only if it has a main. *)
    358367
    359 let interpret p = match p.RTL.main with
    360   | None -> []
     368let interpret print_result p = match p.RTL.main with
     369  | None -> (IntValue.Int8.zero, [])
    361370  | Some main ->
    362371    let mem = init_mem p in
    363372    let main_def = find_function mem main in
    364373    let st = CallState ([], main_def, [], mem, []) in
    365     iter_small_step st
     374    iter_small_step print_result st

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

    r486 r619  
    33    and return the trace of cost labels encountered. *)
    44
    5 val interpret : RTL.program -> AST.trace
     5val interpret : bool -> RTL.program -> AST.trace

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

    r486 r619  
    171171  | [] -> [fun start_lbl -> adds_graph [ERTL.St_skip start_lbl] start_lbl]
    172172  | [r] ->
    173     [fun start_lbl ->
    174       adds_graph [ERTL.St_set_hdw (I8051.st0, r, start_lbl)] start_lbl]
     173    [fun start_lbl dest_lbl def ->
     174      let (def, r_tmp) = fresh_reg def in
     175      adds_graph [ERTL.St_int (r_tmp, 0, start_lbl) ;
     176                  ERTL.St_set_hdw (I8051.st1, r_tmp, start_lbl) ;
     177                  ERTL.St_set_hdw (I8051.st0, r, start_lbl)]
     178        start_lbl dest_lbl def]
    175179  | r1 :: r2 :: _ ->
    176180    [(fun start_lbl ->
    177       adds_graph [ERTL.St_set_hdw (I8051.st1, r1, start_lbl)] start_lbl) ;
    178      (fun start_lbl ->
    179        adds_graph [ERTL.St_set_hdw (I8051.st0, r2, start_lbl)] start_lbl)]
     181      adds_graph [ERTL.St_set_hdw (I8051.st1, r1, start_lbl) ;
     182                  ERTL.St_set_hdw (I8051.st0, r2, start_lbl)] start_lbl)]
    180183
    181184let add_epilogue ret_regs srah sral sregs def =
    … …  
    267270
    268271(* Fetching the result depends on the type of the function, or say, the number
    269    of registers that are waiting for a value. *)
     272   of registers that are waiting for a value. Temporary non allocatable
     273   registers are used. Indeed, moving directly from DPL to a pseudo-register may
     274   cause a bug: DPL might be used to compute the address of the
     275   pseudo-register. *)
    270276
    271277let fetch_result ret_regs start_lbl = match ret_regs with
    272278  | [] -> adds_graph [ERTL.St_skip start_lbl] start_lbl
    273279  | [r] ->
    274     adds_graph
     280      adds_graph
    275281      [ERTL.St_hdw_to_hdw (I8051.st0, I8051.dpl, start_lbl) ;
    276282       ERTL.St_get_hdw (r, I8051.st0, start_lbl)]
    … …  
    401407
    402408
     409(* Move the first cost label of each function at the beginning of the
     410   function. Indeed, the instructions for calling conventions (stack allocation
     411   for example) are added at the very beginning of the function, thus before the
     412   first cost label. *)
     413
     414let generate stmt def =
     415  let entry = Label.Gen.fresh def.ERTL.f_luniverse in
     416  let def =
     417    { def with ERTL.f_graph = Label.Map.add entry stmt def.ERTL.f_graph } in
     418  { def with ERTL.f_entry = entry }
     419
     420let find_and_remove_first_cost_label def =
     421  let rec aux lbl = match Label.Map.find lbl def.ERTL.f_graph with
     422    | ERTL.St_cost (cost_label, next_lbl) ->
     423      let graph = Label.Map.add lbl (ERTL.St_skip next_lbl) def.ERTL.f_graph in
     424      (cost_label, { def with ERTL.f_graph = graph })
     425    | ERTL.St_skip lbl | ERTL.St_comment (_, lbl) | ERTL.St_get_hdw (_, _, lbl)
     426    | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
     427    | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl)
     428    | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl)
     429    | ERTL.St_move (_, _, lbl) | ERTL.St_opaccs (_, _, _, _, lbl)
     430    | ERTL.St_op1 (_, _, _, lbl) | ERTL.St_op2 (_, _, _, _, lbl)
     431    | ERTL.St_clear_carry lbl | ERTL.St_load (_, _, _, lbl)
     432    | ERTL.St_store (_, _, _, lbl) | ERTL.St_call_id (_, _, lbl)
     433    | ERTL.St_newframe lbl | ERTL.St_delframe lbl | ERTL.St_framesize (_, lbl)
     434      ->
     435      aux lbl
     436    | ERTL.St_condacc _ | ERTL.St_return _ ->
     437      (* Should be impossible: the first cost label is found after some linear
     438         instructions. *)
     439      assert false in
     440  aux def.ERTL.f_entry
     441
     442let move_first_cost_label_up_internal def =
     443  let (cost_label, def) = find_and_remove_first_cost_label def in
     444  generate (ERTL.St_cost (cost_label, def.ERTL.f_entry)) def
     445
     446let move_first_cost_label_up (id, def) =
     447  let def' = match def with
     448    | ERTL.F_int int_fun ->
     449      ERTL.F_int (move_first_cost_label_up_internal int_fun)
     450    | _ -> def in
     451  (id, def')
     452
     453
    403454let translate p =
    404455  (* We simplify tail calls as regular calls for now. *)
    405456  let p = RTLtailcall.simplify p in
     457  (* The tranformation on each RTL function: create an ERTL function and move
     458     its first cost label at the very beginning. *)
     459  let f funct = move_first_cost_label_up (translate_funct funct) in
    406460  { ERTL.vars   = p.RTL.vars ;
    407     ERTL.functs = List.map translate_funct p.RTL.functs ;
     461    ERTL.functs = List.map f p.RTL.functs ;
    408462    ERTL.main   = p.RTL.main }

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

    r486 r619  
    3838type state =
    3939  | State of stack_frame list * RTLabs.graph * Val.t (* stack pointer *) *
    40              Label.t * local_env * memory * AST.trace
     40             Label.t * local_env * memory * CostLabel.t list
    4141  | CallState of stack_frame list * RTLabs.function_def *
    42                  Val.t list (* args *) * memory * AST.trace
     42                 Val.t list (* args *) * memory * CostLabel.t list
    4343  | ReturnState of stack_frame list * Val.t (* return value *) *
    44                    memory * AST.trace
     44                   memory * CostLabel.t list
    4545
    4646
    … …  
    135135  | AST.Op_divu -> Val.divu
    136136  | AST.Op_mod -> Val.modulo
    137   | AST.Op_modu -> Val.modu
     137  | AST.Op_modu -> Val.modulou
    138138  | AST.Op_and -> Val.and_op
    139139  | AST.Op_or -> Val.or_op
    … …  
    192192    (mem  : memory)
    193193    (stmt : RTLabs.statement)
    194     (t    : AST.trace) :
     194    (t    : CostLabel.t list) :
    195195    state = match stmt with
    196196
    … …  
    364364    (args  : Val.t list)
    365365    (mem   : memory)
    366     (t     : AST.trace) :
     366    (t     : CostLabel.t list) :
    367367    state =
    368368  match f_def with
    … …  
    382382    (ret_val : Val.t)
    383383    (mem     : memory)
    384     (t       : AST.trace) :
     384    (t       : CostLabel.t list) :
    385385    state =
    386386  let lenv = adds sf.ret_regs ret_val sf.lenv in
    … …  
    400400
    401401
    402 let rec iter_small_step st = match small_step st with
     402let compute_result v =
     403  if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
     404  else IntValue.Int8.zero
     405
     406let rec iter_small_step print_result st = match small_step st with
    403407(*
     408  (* <DEBUG> *)
    404409  | ReturnState ([], v, mem, t) ->
    405410    Mem.print mem ;
    … …  
    409414  | ReturnState (_, _, mem, _)
    410415  | State (_, _, _, _, _, mem, _) as st' -> Mem.print mem ; iter_small_step st'
     416  (* </DEBUG> *)
    411417*)
    412   | ReturnState ([], v, mem, t) -> List.rev t
    413   | st' -> iter_small_step st'
     418  | ReturnState ([], v, mem, t) ->
     419    let (res, cost_labels) as trace = (compute_result v, List.rev t) in
     420    if print_result then
     421      Printf.printf "RTLabs: %s\n%!" (IntValue.Int8.to_string res) ;
     422    trace
     423  | st' -> iter_small_step print_result st'
    414424
    415425
    … …  
    431441(* Interpret the program only if it has a main. *)
    432442
    433 let interpret p = match p.RTLabs.main with
    434   | None -> []
     443let interpret print_result p = match p.RTLabs.main with
     444  | None -> (IntValue.Int8.zero, [])
    435445  | Some main ->
    436446    let mem = init_mem p in
    437447    let main_def = find_function mem main in
    438448    let st = CallState ([], main_def, [], mem, []) in
    439     iter_small_step st
     449    iter_small_step print_result st

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

    r486 r619  
    33    and return the trace of cost labels encountered. *)
    44
    5 val interpret : RTLabs.program -> AST.trace
     5val interpret : bool -> RTLabs.program -> AST.trace

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

    r486 r619  
    2222*)
    2323let process filename =
    24   let _ = Printf.eprintf "Processing %s :\n" filename in
    25   let src_language = Options.get_source_language () in
    26   let tgt_language = Options.get_target_language () in
    27   let input_ast    = Languages.parse src_language filename in
    28   let input_ast    = Languages.labelize input_ast in
     24  let _ = Printf.eprintf "Processing %s.\n%!" filename in
     25  let src_language    = Options.get_source_language () in
     26  let tgt_language    = Options.get_target_language () in
     27  let input_ast       = Languages.parse src_language filename in
     28  let input_ast       = Languages.labelize input_ast in
     29  let (exact_output, output_filename) = match Options.get_output_files () with
     30    | None -> (false, filename)
     31    | Some filename' -> (true, filename') in
     32  let save = Languages.save exact_output output_filename in
    2933  let target_asts =
    3034    (** If debugging is enabled, the compilation function returns all
    … …  
    3438  in
    3539  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
    36     Languages.save filename final_ast;
     40    save final_ast;
    3741    (if Options.annotation_requested () then
    38        let annotated_input_ast = Languages.annotate input_ast final_ast in
    39        Languages.save filename annotated_input_ast);
     42       let (annotated_input_ast, cost_incr) =
     43         Languages.annotate input_ast final_ast in
     44       save annotated_input_ast;
     45       Languages.save_cost_incr output_filename cost_incr);
    4046    (if Options.is_debug_enabled () then
    41       List.iter (Languages.save filename) intermediate_asts);
     47      List.iter save intermediate_asts);
    4248    if Options.interpretation_requested () || Options.is_debug_enabled () then
    4349      begin
    4450        let asts = input_ast :: target_asts in
    45         let label_traces = List.map Languages.interpret asts in
    46           Printf.eprintf "Checking execution traces...";
    47           Checker.same_traces (List.combine asts label_traces);
    48           Printf.eprintf "OK.\n%!";
     51        let print_result = Options.is_print_result_enabled () in
     52        let label_traces = List.map (Languages.interpret print_result) asts in
     53        Printf.eprintf "Checking execution traces...%!";
     54        Checker.same_traces (List.combine asts label_traces);
     55        Printf.eprintf "OK.\n%!";
    4956      end
    5057
    5158let _ =
    5259  if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files
    53   else List.iter process input_files
     60  else List.iter process input_files 

  • Deliverables/D2.2/8051/src/checker.ml

    r486 r619  
    1 let same_traces (traces : ((Languages.ast * (Label.t list)) list)) =
     1let same_traces (traces : ((Languages.ast * AST.trace) list)) =
    22  let compare_trace trace1 trace2 =
    33    let occs_trace1 = Misc.ListExt.multi_set_of_list trace1
    … …  
    55    Misc.ListExt.assoc_diff occs_trace1 occs_trace2
    66  in
    7   let check_trace (_, trace1) (_, trace2) =
     7  let check_trace (_, (_, trace1)) (_, (_, trace2)) =
    88    compare_trace trace1 trace2 = []
    99  in
    … …  
    2222  match Misc.ListExt.transitive_forall2 check_trace traces with
    2323    | None -> ()
    24     | Some ((ast1, trace1), (ast2, trace2)) ->
     24    | Some ((ast1, (res1, trace1)), (ast2, (res2, trace2))) ->
    2525      let lang1 = Languages.to_string (Languages.language_of_ast ast1)
    2626      and lang2 = Languages.to_string (Languages.language_of_ast ast2) in

  • Deliverables/D2.2/8051/src/checker.mli

    r486 r619  
    33(** [same_traces ts] checks that the collected execution traces are
    44    identical (modulo permutation). *)
    5 val same_traces : (Languages.ast * (Label.t list)) list -> unit
    6 
    7 
    8 
     5val same_traces : (Languages.ast * AST.trace) list -> unit

  • Deliverables/D2.2/8051/src/clight/clightAnnotator.ml

    r486 r619  
    1212
    1313
    14 (* Program var names, cost labels and labels *)
     14(* Program var and fun names, cost labels and labels *)
    1515
    1616let string_set_of_list l =
    … …  
    312312  let res = ClightParser.process tmp_file in
    313313  Misc.SysExt.safe_remove tmp_file ;
    314   res
    315 
    316 
     314  (res, cost_incr)

  • Deliverables/D2.2/8051/src/clight/clightAnnotator.mli

    r486 r619  
    55    global variable --- the so-called cost variable --- is added to the program.
    66    Then, each cost label in the program is replaced by an increment of the cost
    7     variable, following the mapping [cost_map]. *)
     7    variable, following the mapping [cost_map]. The returned string is the name
     8    of the cost increment function. *)
    89
    9 val instrument : Clight.program -> int CostLabel.Map.t -> Clight.program
     10val instrument : Clight.program -> int CostLabel.Map.t ->
     11                 Clight.program * string
    1012
    1113val cost_labels : Clight.program -> CostLabel.Set.t

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

    r486 r619  
    248248  (*Pointer*)
    249249  | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
    250       Value.add v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))
     250      Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
    251251  | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 ->
    252       Value.add v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))
     252      Value.add v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
    253253  (*Error*)
    254254  | _ -> assert false (*Type error*)
    … …  
    271271  (*Pointer*)
    272272  | ((v1,t1) , (v2,t2)) when is_pointer_type t1 && is_int_type t2 ->
    273       Value.sub v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))
    274   | ((v2,t2) , (v1,t1)) when is_pointer_type t1 && is_int_type t2 ->
    275       Value.sub v1 (Value.of_int ((Value.to_int v2)*(sizeof (get_subtype t1))))
     273      Value.sub v1 (Value.mul v2 (Value.of_int (sizeof (get_subtype t1))))
    276274  (*Error*)
    277275  | _ -> assert false (*Type error*)
    … …  
    611609  | State(f,Sswitch(a,sl),k,e,m) ->
    612610      let (n,l) = (match eval_expr globalenv e m a with
    613                      | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll) 
     611                     | ((v,_),ll) when Value.is_int v -> (Value.to_int v,ll)
    614612                     | _ -> assert false (*Wrong switch index*)
    615613      ) in
    … …  
    682680    (m,(g2,f))
    683681
     682let compute_result v =
     683  if Value.is_int v then IntValue.Int8.cast (Value.to_int_repr v)
     684  else IntValue.Int8.zero
     685
    684686let interpret debug prog = match prog.prog_main with
    685   | None -> []
     687  | None -> (IntValue.Int8.zero, [])
    686688  | Some main ->
    687689      let (m,g) = initmem_clight prog in
    … …  
    689691      let rec exec trace = function
    690692        | (Returnstate(v,Kstop,m),l) ->
     693(*
    691694            if debug then (
    692695              print_string ("Result: "^(Value.to_string v));
    … …  
    694697              Mem.print m
    695698            );
    696             l@trace
     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
    697704        | (State(_,Sskip,Kstop,_,m),l) -> (*Implicit return in main*)
     705(*
    698706            if debug then (
    699707              print_string ("Result: (implicit return)");
    … …  
    701709              Mem.print m
    702710            );
    703             l@trace
     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
    704716        | (state,l) ->
     717(*
    705718            if debug then print_string ((string_of_state state)^"\n");
     719*)
    706720            exec (l@trace) (next_step g state)
    707721      in
     722(*
    708723      if debug then print_string "> --- Interpret Clight --- <\n";
    709       exec [] first_state
     724*)
     725      exec [] first_state

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

    r486 r619  
    154154let make_cast e = function
    155155  | (Tint(_,_),Tint(I8,Signed)) when int_size>8     -> Op1 (Op_cast8signed,e)
    156   | (Tint(_,_),Tint(I8,Unsigned)) when int_size>8   -> Op1 (Op_cast8signed,e)
     156  | (Tint(_,_),Tint(I8,Unsigned)) when int_size>8   -> Op1 (Op_cast8unsigned,e)
    157157  | (Tint(_,_),Tint(I16,Signed)) when int_size>16   -> Op1 (Op_cast16signed,e)
    158158  | (Tint(_,_),Tint(I16,Unsigned)) when int_size>16 -> Op1 (Op_cast16unsigned,e)
    … …  
    521521  | (id,External (i,p,r)) -> (id, F_ext (translate_external i p r))
    522522
    523 let translate p =
     523let translate p =
     524  (* TODO: Clight32ToClight8 transformation *)
     525(*
     526  let p = Clight32ToClight8.translate p in
     527*)
     528  (* <DEBUG> *)
     529(*
     530  Printf.printf "%s\n%!" (ClightPrinter.print_program p) ;
     531*)
     532  (* </DEBUG> *)
    524533  let globals = List.map (fun p -> (fst (fst p),snd p) ) p.prog_vars in
    525534  let p =

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

    r486 r619  
    137137    (f_name, instrument_function costs_mapping cost_id f_def) in
    138138  let functs = List.map f p.Cminor.functs in
    139   { Cminor.vars   = vars ;
    140     Cminor.functs = functs ;
    141     Cminor.main   = p.Cminor.main }
     139  ({ Cminor.vars   = vars ;
     140     Cminor.functs = functs ;
     141     Cminor.main   = p.Cminor.main },
     142   "" (* TODO *))
    142143
    143144

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

    r486 r619  
    55    global variable --- the so-called cost variable --- is added to the program.
    66    Then, each cost label in the program is replaced by an increment of the cost
    7     variable, following the mapping [cost_map]. *)
     7    variable, following the mapping [cost_map]. The returned string is the name
     8    of the cost increment function. *)
    89
    9 val instrument : Cminor.program -> int CostLabel.Map.t -> Cminor.program
     10val instrument : Cminor.program -> int CostLabel.Map.t ->
     11                 Cminor.program * string
    1012
    1113val cost_labels : Cminor.program -> CostLabel.Set.t

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

    r486 r619  
    128128  | Op_divu             -> Value.divu arg1 arg2
    129129  | Op_mod              -> Value.modulo arg1 arg2
    130   | Op_modu             -> Value.modu arg1 arg2
     130  | Op_modu             -> Value.modulou arg1 arg2
    131131  | Op_and              -> Value.and_op arg1 arg2
    132132  | Op_or               -> Value.or_op arg1 arg2
    … …  
    405405    (m,(g2,f))
    406406
     407let compute_result v =
     408  if Value.is_int v then IntValue.Int8.cast (Value.to_int_repr v)
     409  else IntValue.Int8.zero
     410
    407411let interpret debug prog = match prog.main with
    408   | None -> []
     412  | None -> (IntValue.Int8.zero, [])
    409413  | Some main ->
    410414      let (m,global_env) = initmem_cminor prog in
    … …  
    413417                           [], Ct_stop,m),[]) in
    414418      let rec exec l = function
    415         | (State_return(v,Ct_stop,m),lbl) ->
     419        | (State_return(v,Ct_stop,m),lbl) ->
     420(*
    416421            if debug then (
    417422              print_string ("Result: "^(Value.to_string v));
    … …  
    419424              Mem.print m
    420425            );
    421             lbl@l
     426*)
     427          let (res, cost_labels) as trace = (compute_result v, lbl@l) in
     428          if debug then
     429            Printf.printf "Cminor: %s\n%!" (IntValue.Int8.to_string res) ;
     430          trace
    422431        | (State_regular(_,St_skip,Ct_stop,_,_,m),lbl) ->
     432(*
    423433            if debug then (
    424434              print_string ("Result: (implicit return)\n");
    … …  
    426436              Mem.print m
    427437            );
    428             lbl@l
     438*)
     439          let (res, cost_labels) as trace = (IntValue.Int8.zero, lbl@l) in
     440          if debug then
     441            Printf.printf "Cminor: %s\n%!" (IntValue.Int8.to_string res) ;
     442          trace
    429443        | (state,lbl) ->
     444(*
    430445            if debug then print_string ((string_of_state state)^"\n");
     446*)
    431447            exec (lbl@l) (state_transition state global_env)
    432448      in
     449(*
    433450      if debug then print_string ">------------------- Interpret Cminor -------------------<\n";
     451*)
    434452      (exec [] first_state)

  • Deliverables/D2.2/8051/src/common/AST.mli

    r486 r619  
    9292
    9393
    94 (* Traces returned by interpreters: only cost labels are observed. *)
     94(* Traces returned by interpreters: result and cost labels are observed. The
     95   result is interpreted as an 8 bits integer for coherence between
     96   languages. *)
    9597
    96 type trace = CostLabel.t list
     98type trace = IntValue.int8 * CostLabel.t list

  • Deliverables/D2.2/8051/src/common/intValue.ml

    r486 r619  
     1
     2(** This module defines functions to manipulate bounded integers. They can be
     3    used to represent sequences of bits. *)
    14
    25open Big_int
    36
    47
     8(* Integers, whatever their size, will be represented using the Big_int
     9   module. This allows immediate conversion, and allows the representation of
     10   any integer (that fits into memory). *)
     11
    512type int_repr = Big_int.big_int
    613
     14(* The parameter module. Bounded integers are characterized by the number of
     15   bits used to represent them. *)
     16   
    717module type INTTYPE =
    818sig
    9   val size      : int (* in bytes *)
    10   val is_signed : bool
     19  val size : int (* in bytes *)
    1120end
     21
     22(* The signature provided to manipulate bounded integers. *)
    1223
    1324module type S = sig
    … …  
    2031  val one       : t
    2132
    22   val succ   : t -> t
    23   val pred   : t -> t
    24   val add    : t -> t -> t
    25   (** [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the
    26       unsigned value of [i2] overflows. *)
    27   val add_of : t -> t -> bool
    28   val sub    : t -> t -> t
    29   (** [sub_of i1 i2] returns true iff substracting the unsigned value of [i1]
    30       and the unsigned value of [i2] underflows. *)
    31   val sub_of : t -> t -> bool
    32   val mul    : t -> t -> t
    33   val div    : t -> t -> t
    34   val modulo : t -> t -> t
    35   val eq     : t -> t -> bool
    36   val neq    : t -> t -> bool
    37   val lt     : t -> t -> bool
    38   val le     : t -> t -> bool
    39   val gt     : t -> t -> bool
    40   val ge     : t -> t -> bool
    41   val neg    : t -> t
    42   val lognot : t -> t
    43   val logand : t -> t -> t
    44   val logor  : t -> t -> t
    45   val logxor : t -> t -> t
    46   val shl    : t -> t -> t
    47   val shr    : t -> t -> t
    48   val shrl   : t -> t -> t
    49   val max    : t -> t -> t
    50   val min    : t -> t -> t
    51   val cast   : int_repr -> t
    52   val of_int : int -> t
    53   val to_int : t -> int
     33  val succ    : t -> t
     34  val pred    : t -> t
     35  val add     : t -> t -> t
     36  (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
     37  val add_of  : t -> t -> bool
     38  val sub     : t -> t -> t
     39  (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2]
     40      underflows. *)
     41  val sub_uf  : t -> t -> bool
     42  val mul     : t -> t -> t
     43  val div     : t -> t -> t
     44  val divu    : t -> t -> t
     45  val modulo  : t -> t -> t
     46  val modulou : t -> t -> t
     47  val eq      : t -> t -> bool
     48  val neq     : t -> t -> bool
     49  val lt      : t -> t -> bool
     50  val ltu     : t -> t -> bool
     51  val le      : t -> t -> bool
     52  val leu     : t -> t -> bool
     53  val gt      : t -> t -> bool
     54  val gtu     : t -> t -> bool
     55  val ge      : t -> t -> bool
     56  val geu     : t -> t -> bool
     57  val neg     : t -> t
     58  val lognot  : t -> t
     59  val logand  : t -> t -> t
     60  val logor   : t -> t -> t
     61  val logxor  : t -> t -> t
     62  val shl     : t -> t -> t
     63  val shr     : t -> t -> t
     64  val shrl    : t -> t -> t
     65  val max     : t -> t -> t
     66  val maxu    : t -> t -> t
     67  val min     : t -> t -> t
     68  val minu    : t -> t -> t
     69  val cast    : int_repr -> t
     70  val of_int  : int -> t
     71  val to_int  : t -> int
     72
     73  (** [zero_ext n a] performs zero extension on [a] where [n] bits are
     74      significant. *)
     75  val zero_ext : int -> t -> t
     76  (** [sign_ext n a] performs sign extension on [a] where [n] bits are
     77      significant. *)
     78  val sign_ext : int -> t -> t
    5479
    5580  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
    5681      element is the high bits, and the last is the low bits. *)
    5782  val break : t -> int -> t list
    58   (** [merge l] creates an the integer where the first element of [l] is its
     83  (** [merge l] creates the integer where the first element of [l] is its
    5984      high bits, etc, and the last element of [l] is its low bits. *)
    6085  val merge : t list -> t
    … …  
    6388
    6489
    65 (* First, we use a parameter module and a functor where integers may be
    66    unbounded. This will allow to create the Integer module (unbounded integers)
    67    as well as bounded integers. *)
    68 
    69 module type INTTYPE_ARB =
    70 sig
    71   val size      : int
    72   val is_signed : bool
    73   val arbitrary : bool
    74 end
    75 
    76 (* The following functor works for unbounded integers as well as for bounded
    77    intergers. *)
    78 
    79 module Make_Arb (IntType: INTTYPE_ARB) : S =
     90module Make (IntType: INTTYPE) : S =
    8091struct
    8192
    … …  
    90101  let two = succ_big_int unit_big_int
    91102
    92   let half_bound = power_int_positive_int 2 (size-1)
    93 
    94   (* The upper bound of signed integers. *)
    95   let shbound = half_bound
    96   (* The lower bound of signed integers. *)
    97   let slbound = minus_big_int half_bound
    98 
    99   (* The upper bound of unsigned integers. *)
    100   let uhbound = mult_int_big_int 2 half_bound
    101   (* The lower bound of unsigned integers. *)
    102   let ulbound = zero
    103 
    104   (* [unsign a] returns the unsigned value of [a]. *)
    105   let unsign a =
    106     if lt_big_int a zero_big_int then add_big_int uhbound a
    107     else a
    108 
    109   (* [is_in_repr a] returns true iff [a] is a value comprised in the interval of
    110      representation. *)
    111   let is_in_repr a =
    112     if IntType.is_signed then (le_big_int slbound a) && (lt_big_int a shbound)
    113     else (le_big_int ulbound a) && (lt_big_int a uhbound)
     103  (* Integers will all be taken modulo the following value. *)
     104  let _mod = power_int_positive_int 2 size
     105
     106  (* The lower bound (inclusive). *)
     107  let lower_bound = zero
     108  (* The upper bound (inclusive). *)
     109  let upper_bound = pred_big_int _mod
    114110
    115111  (* [cast a] returns a modulo of [a] such that the result fits in the interval
    116112     of representation. *)
    117   let cast a =
    118     if IntType.arbitrary then a
    119     else
    120       if is_in_repr a then a
    121       else
    122         if IntType.is_signed then
    123           sub_big_int
    124             (mod_big_int (add_big_int a half_bound) uhbound)
    125             half_bound
    126         else mod_big_int a uhbound
     113  let cast a = mod_big_int a _mod
     114
     115  (* Half bound (exclusive), i.e. upper bound of signed integers. *)
     116  let half_bound = power_int_positive_int 2 (size-1)
     117
     118  (* Signed value of [a]. *)
     119  let signed a = sub_big_int (cast a) half_bound
     120
     121  let signed_op op a b = op (signed a) (signed b)
    127122
    128123  let succ a = cast (succ_big_int a)
    … …  
    130125  let add a b = cast (add_big_int a b)
    131126
    132   (* [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the
    133      unsigned value of [i2] overflows. *)
    134   let add_of a b =
    135     let u1 = unsign a in
    136     let u2 = unsign b in
    137     let i = add_big_int u1 u2 in
    138     ge_big_int i uhbound
     127  (* [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
     128  let add_of a b = gt_big_int (add_big_int a b) upper_bound
    139129
    140130  let sub a b = cast (sub_big_int a b)
    141131
    142   (* [sub_of i1 i2] returns true iff substracting the unsigned value of [i1] and
    143      the unsigned value of [i2] underflows. *)
    144   let sub_of a b =
    145     let u1 = unsign a in
    146     let u2 = unsign b in
    147     let i = sub_big_int u1 u2 in
    148     lt_big_int i zero_big_int
     132  let cast_op op a b = op (cast a) (cast b)
    149133
    150134  let mul a b = cast (mult_big_int a b)
    151   let div a b = cast (div_big_int a b)
    152   let modulo a b = cast (mod_big_int a b)
     135  let div a b = cast (signed_op div_big_int a b)
     136  let divu a b = cast_op div_big_int a b
     137  let modulo a b = cast (signed_op mod_big_int a b)
     138  let modulou a b = cast_op mod_big_int a b
     139
    153140  let eq = eq_big_int
    154141  let neq a b = not (eq a b)
    155   let lt a b = lt_big_int (cast a) (cast b)
    156   let le a b = le_big_int (cast a) (cast b)
    157   let gt a b = gt_big_int (cast a) (cast b)
    158   let ge a b = ge_big_int (cast a) (cast b)
     142  let lt a b = signed_op lt_big_int a b
     143  let le a b = signed_op le_big_int a b
     144  let gt a b = signed_op gt_big_int a b
     145  let ge a b = signed_op ge_big_int a b
     146  let ltu a b = cast_op lt_big_int a b
     147  let leu a b = cast_op le_big_int a b
     148  let gtu a b = cast_op gt_big_int a b
     149  let geu a b = cast_op ge_big_int a b
     150
     151  (* [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2] underflows. *)
     152  let sub_uf a b = lt_big_int (sub_big_int a b) zero
     153
    159154  let of_int i = cast (big_int_of_int i)
    160   let to_int i = int_of_big_int i
     155  let to_int i = int_of_big_int (cast i)
     156
    161157  let neg a = cast (minus_big_int a)
    162158
    163   let lognot a =
    164     let mone = minus_big_int unit_big_int in
    165     if IntType.is_signed then sub mone a
    166     else sub (pred uhbound) a
     159  let lognot = sub upper_bound
    167160
    168161  let shl a b =
    169     let pow = power_int_positive_big_int 2 b in
     162    let pow = power_int_positive_big_int 2 (cast b) in
    170163    cast (mult_big_int a pow)
    171164
    172165  let shr a b =
    173     let pow = power_int_positive_big_int 2 b in
    174     cast (div_big_int a pow)
    175 
    176   let shrl a b =
     166    let a = cast a in
     167    let b = cast b in
    177168    let added =
    178       if IntType.is_signed || (lt_big_int b half_bound) then zero_big_int
     169      if lt_big_int a half_bound then zero
    179170      else half_bound in
    180171    let rec aux acc b =
    181       if eq_big_int b zero_big_int then acc
     172      if eq b zero then acc
    182173      else
    183         let cont_acc = add_big_int added (div_big_int acc two) in
    184         let cont_b = pred_big_int b in
     174        let cont_acc = add added (divu acc two) in
     175        let cont_b = pred b in
    185176        aux cont_acc cont_b
    186177    in
    187178    cast (aux a b)
     179
     180  let shrl a b =
     181    let pow = power_int_positive_big_int 2 (cast b) in
     182    cast (div_big_int (cast a) pow)
    188183
    189184  let max a b = if lt a b then b else a
    190185  let min a b = if gt a b then b else a
    191 
    192   let is_odd a = eq_big_int (mod_big_int a two) unit_big_int
    193   (* [to_bits a] returns the list of bits (0 or 1) that a represents. Signed
    194      integers are represented using the 2-complement representation. *)
     186  let maxu a b = if ltu a b then b else a
     187  let minu a b = if gtu a b then b else a
     188
     189  let is_odd a = eq (modulou a two) one
     190  (* [to_bits a] returns the list of bits (0 or 1) that [a] represents. *)
    195191  let to_bits a =
    196192    let rec aux acc a i =
    197193      if i >= size then acc
    198       else aux ((is_odd a) :: acc) (div_big_int a two) (i+1)
    199     in
    200     aux [] a 0
     194      else aux ((is_odd a) :: acc) (divu a two) (i+1)
     195    in
     196    aux [] (cast a) 0
    201197
    202198  (* [from_bits bits] returns the integer that the list of bits [bits]
    203      represents. Signed integers are represented using the 2-complement
    204      representation. *)
     199     represents. *)
    205200  let from_bits bits =
    206201    let rec aux acc = function
    207202      | [] -> acc
    208203      | b :: bits ->
    209         let next_acc = mult_int_big_int 2 acc in
    210         let next_acc = if b then succ_big_int next_acc else next_acc in
     204        let next_acc = mul acc two in
     205        let next_acc = if b then succ next_acc else next_acc in
    211206        aux next_acc bits
    212207    in
    213     cast (aux zero_big_int bits)
     208    aux zero bits
    214209
    215210  (* [binary_log_op f a b] applies the binary boolean operation [f]
    … …  
    224219  let logxor = binary_log_op xor
    225220
     221
     222  (* [zero_ext n a] performs zero extension on [a] where [n] bits are
     223     significant. *)
     224  let zero_ext n a =
     225    let pow2 = power_int_positive_int 2 n in
     226    cast (mod_big_int a pow2)
     227
     228  (* [sign_ext n a] performs sign extension on [a] where [n] bits are
     229     significant. *)
     230  let sign_ext n a =
     231    let a' = zero_ext n a in
     232    let pow2 = power_int_positive_int 2 (n-1) in
     233    let sign = divu a pow2 in
     234    if is_odd sign then
     235      let added = shr half_bound (of_int (n-1)) in
     236      add a' added
     237    else a'
     238
     239
    226240  (* [break i n] cuts [i] in [n] parts. In the resulting list, the first element
    227241     is the high bits, and the last is the low bits. *)
    228242  let break a n =
    229     let chunk_size = (8 * IntType.size) / n in
     243    let chunk_size = size / n in
    230244    let pow2_chunk_size = power_int_positive_int 2 chunk_size in
    231245    let rec aux acc a i =
    232246      if i = 0 then acc
    233247      else
    234         let (next, chunk) = Big_int.quomod_big_int a pow2_chunk_size in
     248        let (next, chunk) = quomod_big_int a pow2_chunk_size in
    235249        aux ((cast chunk) :: acc) next (i-1)
    236250    in
    237     aux [] a n
     251    aux [] (cast a) n
    238252
    239253  (* [merge l] creates the integer where the first element of [l] is its high
    … …  
    244258      let al = List.rev al in
    245259      let nb_chunks = List.length al in
    246       let chunk_size = (8 * IntType.size) / nb_chunks in
     260      let chunk_size = size / nb_chunks in
    247261      let pow2_chunk_size = power_int_positive_int 2 chunk_size in
    248262      let rec aux pow2 = function
    … …  
    255269
    256270
    257 module Make (IntType : INTTYPE) =
    258   Make_Arb (struct include IntType let arbitrary = false end)
    259 
    260 
    261 module Int8s : S = Make
    262   (struct
    263     let size = 1
    264     let is_signed = true
    265    end)
    266 
    267 module Int8u : S = Make
    268   (struct
    269     let size = 1
    270     let is_signed = false
    271    end)
    272 
    273 module Int16s : S = Make
    274   (struct
    275     let size = 2
    276     let is_signed = true
    277    end)
    278 
    279 module Int16u : S = Make
    280   (struct
    281     let size = 2
    282     let is_signed = false
    283    end)
    284 
    285 module Int32 : S = Make
    286   (struct
    287     let size = 4
    288     let is_signed = true
    289    end)
    290 
    291 module Integer : S = Make_Arb
    292   (struct
    293     let size = 1
    294     let is_signed = true
    295     let arbitrary = true
    296    end)
    297 
    298 
    299 type int8s   = Int8s.t
    300 type int8u   = Int8u.t
    301 type int16s  = Int16s.t
    302 type int16u  = Int16u.t
    303 type int32   = Int32.t
    304 type integer = Integer.t
     271module Int8  : S = Make (struct let size = 1 end)
     272module Int16 : S = Make (struct let size = 2 end)
     273module Int32 : S = Make (struct let size = 4 end)
     274
     275type int8  = Int8.t
     276type int16 = Int16.t
     277type int32 = Int32.t

  • Deliverables/D2.2/8051/src/common/intValue.mli

    r486 r619  
    11
    2 (** This module defines functions to manipulate integers coded on various number
    3     of bits (sized integers). *)
     2(** This module defines functions to manipulate bounded integers. They can be
     3    used to represent sequences of bits. *)
    44
    55(* Integers, whatever their size, will be represented using the Big_int
    … …  
    99type int_repr = Big_int.big_int
    1010
    11 (* The parameter module. Sized integers are characterized by the number of bits
    12    used to represent them, and the fact that they are signed or not. *)
     11(* The parameter module. Bounded integers are characterized by the number of
     12   bits used to represent them. *)
    1313   
    1414module type INTTYPE =
    1515sig
    16   val size      : int (* in bytes *)
    17   val is_signed : bool
     16  val size : int (* in bytes *)
    1817end
    1918
    20 (* The signature provided to manipulate sized integers. *)
     19(* The signature provided to manipulate bounded integers. *)
    2120
    2221module type S = sig
    … …  
    2928  val one       : t
    3029
    31   val succ   : t -> t
    32   val pred   : t -> t
    33   val add    : t -> t -> t
    34   (** [add_of i1 i2] returns true iff adding the unsigned value of [i1] and the
    35       unsigned value of [i2] overflows. *)
    36   val add_of : t -> t -> bool
    37   val sub    : t -> t -> t
    38   (** [sub_of i1 i2] returns true iff substracting the unsigned value of [i1]
    39       and the unsigned value of [i2] overflows. *)
    40   val sub_of : t -> t -> bool
    41   val mul    : t -> t -> t
    42   val div    : t -> t -> t
    43   val modulo : t -> t -> t
    44   val eq     : t -> t -> bool
    45   val neq    : t -> t -> bool
    46   val lt     : t -> t -> bool
    47   val le     : t -> t -> bool
    48   val gt     : t -> t -> bool
    49   val ge     : t -> t -> bool
    50   val neg    : t -> t
    51   val lognot : t -> t
    52   val logand : t -> t -> t
    53   val logor  : t -> t -> t
    54   val logxor : t -> t -> t
    55   val shl    : t -> t -> t
    56   val shr    : t -> t -> t
    57   val shrl   : t -> t -> t
    58   val max    : t -> t -> t
    59   val min    : t -> t -> t
    60   val cast   : int_repr -> t
    61   val of_int : int -> t
    62   val to_int : t -> int
     30  val succ    : t -> t
     31  val pred    : t -> t
     32  val add     : t -> t -> t
     33  (** [add_of i1 i2] returns [true] iff adding [i1] and [i2] overflows. *)
     34  val add_of  : t -> t -> bool
     35  val sub     : t -> t -> t
     36  (** [sub_uf i1 i2] returns [true] iff substracting [i1] and [i2]
     37      underflows. *)
     38  val sub_uf  : t -> t -> bool
     39  val mul     : t -> t -> t
     40  val div     : t -> t -> t
     41  val divu    : t -> t -> t
     42  val modulo  : t -> t -> t
     43  val modulou : t -> t -> t
     44  val eq      : t -> t -> bool
     45  val neq     : t -> t -> bool
     46  val lt      : t -> t -> bool
     47  val ltu     : t -> t -> bool
     48  val le      : t -> t -> bool
     49  val leu     : t -> t -> bool
     50  val gt      : t -> t -> bool
     51  val gtu     : t -> t -> bool
     52  val ge      : t -> t -> bool
     53  val geu     : t -> t -> bool
     54  val neg     : t -> t
     55  val lognot  : t -> t
     56  val logand  : t -> t -> t
     57  val logor   : t -> t -> t
     58  val logxor  : t -> t -> t
     59  val shl     : t -> t -> t
     60  val shr     : t -> t -> t
     61  val shrl    : t -> t -> t
     62  val max     : t -> t -> t
     63  val maxu    : t -> t -> t
     64  val min     : t -> t -> t
     65  val minu    : t -> t -> t
     66  val cast    : int_repr -> t
     67  val of_int  : int -> t
     68  val to_int  : t -> int
     69
     70  (** [zero_ext n a] performs zero extension on [a] where [n] bits are
     71      significant. *)
     72  val zero_ext : int -> t -> t
     73  (** [sign_ext n a] performs sign extension on [a] where [n] bits are
     74      significant. *)
     75  val sign_ext : int -> t -> t
    6376
    6477  (** [break i n] cuts [i] in [n] parts. In the resulting list, the first
    … …  
    7184end
    7285
    73 (** The functor to create bounded integers from a size and a signedness. *)
     86(** The functor to create bounded integers from a size. *)
    7487
    7588module Make: functor (IntType: INTTYPE) -> S
    7689
     90module Int8  : S
     91module Int16 : S
     92module Int32 : S
     93
     94type int8  = Int8.t
     95type int16 = Int16.t
     96type int32 = Int32.t
     97
     98
     99(*
    77100module Int8s   : S
    78101module Int8u   : S
    … …  
    90113type int32   = Int32.t
    91114type integer = Integer.t
     115*)

  • Deliverables/D2.2/8051/src/common/memory.ml

    r486 r619  
    192192    | Some alignment when (size <= alignment) && (is_multiple size alignment) ->
    193193      let size = Offset.of_int size in
    194       let rem = Offset.modulo off size in
     194      let rem = Offset.modulou off size in
    195195      if Offset.eq rem Offset.zero then off
    196196      else Offset.add off (Offset.sub size rem)
    197197    | Some alignment ->
    198198      let size = Offset.of_int alignment in
    199       let rem = Offset.modulo off size in
     199      let rem = Offset.modulou off size in
    200200      if Offset.eq rem Offset.zero then off
    201201      else Offset.add off (Offset.sub size rem)
    … …  
    263263  (* Pretty printing *)
    264264
    265 let print mem =
     265  let print mem =
    266266    let print_cells off = function
    267267      | Datum (size, v) when Value.eq v Value.undef ->
    … …  
    275275      match content with
    276276        | Contents contents ->
    277             Printf.printf "(%s -> %s)%!"
    278               (Offset.to_string contents.low) (Offset.to_string contents.high) ;
    279             OffsetMap.iter print_cells contents.cells
     277          Printf.printf "(%s -> %s)%!"
     278            (Offset.to_string contents.low) (Offset.to_string contents.high) ;
     279          OffsetMap.iter print_cells contents.cells
    280280        | Fun_def _ -> Printf.printf "function definition%!" ;
    281281    in
    282282    BlockMap.iter print_block mem.blocks ;
    283283    Printf.printf "\n%!"
    284 
    285 
    286284
    287285
    … …  
    405403    all_are_in_list msg mem b first_off last_off [Datum (1, Value.undef) ; Cont]
    406404
     405  let string_of_alignment = function
     406    | None -> "none"
     407    | Some alignment -> string_of_int alignment
     408
    407409  (** [write_value msg mem b off size v size'] store the value [v] at the offset
    408410      [off] of the block [b] in the memory [mem]. [size] is the size of the

  • Deliverables/D2.2/8051/src/common/memory.mli

    r486 r619  
    108108              (int list (* resulting offsets *) * int (* full size *))
    109109
    110   val size_of_datas    : AST.data list -> int
     110  val size_of_datas : AST.data list -> int
    111111
    112112  (** [offsets_of_datas datas] returns the aligned offsets for the datas
    … …  
    114114  val offsets_of_datas : AST.data list -> (AST.data * int (* offset *)) list
    115115
    116   val alloc_datas      : 'fun_def memory -> AST.data list ->
    117                          ('fun_def memory * Value.t)
     116  val alloc_datas : 'fun_def memory -> AST.data list ->
     117                    ('fun_def memory * Value.t)
    118118
    119119  val print : 'fun_def memory -> unit

  • Deliverables/D2.2/8051/src/common/value.ml

    r486 r619  
    103103  val add_and_of : t -> t -> (t * t)
    104104  val add        : t -> t -> t
    105   (** [add_of v1 v2] returns the 1 value if the sum of [v1] and [v2]
    106       overflows, and 0 otherwise. *)
     105  (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2]
     106      overflows, and [0] otherwise. *)
    107107  val add_of     : t -> t -> t
    108108  (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
    109       this substraction overflows. *)
    110   val sub_and_of : t -> t -> (t * t)
     109      this substraction underflows. *)
     110  val sub_and_uf : t -> t -> (t * t)
    111111  val sub        : t -> t -> t
    112   (** [sub_of v1 v2] returns the 1 value if the substraction of [v1] and [v2]
    113       overflows, and 0 otherwise. *)
    114   val sub_of     : t -> t -> t
     112  (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2]
     113      underflows, and [0] otherwise. *)
     114  val sub_uf     : t -> t -> t
    115115  val mul        : t -> t -> t
    116116  val div        : t -> t -> t
    117117  val divu       : t -> t -> t
    118118  val modulo     : t -> t -> t
    119   val modu       : t -> t -> t
     119  val modulou    : t -> t -> t
    120120  val and_op     : t -> t -> t
    121121  val or_op      : t -> t -> t
    … …  
    166166  (* This module will be used to represent integer values. *)
    167167  module Int =
    168     IntValue.Make (struct let size = D.int_size let is_signed = true end)
    169 
    170   (* This module will be used to define unsigned operations on integer
    171      values. *)
    172   module Intu =
    173     IntValue.Make (struct let size = D.int_size let is_signed = false end)
     168    IntValue.Make (struct let size = D.int_size end)
    174169
    175170  (* Addresses are represented by a block, i.e. a base address, and an offset
    … …  
    183178
    184179  module Block =
    185     IntValue.Make (struct let size = D.ptr_size let is_signed = true end)
     180    IntValue.Make (struct let size = D.ptr_size end)
    186181  module Offset = (* Block *)
    187     IntValue.Make (struct let size = D.ptr_size let is_signed = true end)
     182    IntValue.Make (struct let size = D.ptr_size end)
    188183
    189184  (* We want to be able to put an address into registers, and we want to be able
    … …  
    226221    | _, Val_ptrl _ -> -1
    227222
     223(*
    228224  let hash = function
    229225    | Val_int i -> Int.to_int i
    … …  
    232228    | Val_ptr (b,o)
    233229    | Val_ptrh (b,o)
    234     | Val_ptrl (b,o) -> Integer.to_int (Integer.add b o)
     230    | Val_ptrl (b,o) -> Int.to_int (Int.add b o)
     231*)
     232
     233  let hash = Hashtbl.hash
    235234
    236235  let equal a b = compare a b = 0
    … …  
    315314    | _ -> Val_undef
    316315
    317   (** [cast8unsigned v] returns undefined for non-integer values. For integer
    318       values, it supposes that the value is a 8 bit unsigned integer. It will
    319       return the integer value that represents the same quantity, but using
    320       every bits (2-completement representation). The other cast operations
    321       behave the same way. *)
    322 
    323   let cast8unsigned = cast Int8u.cast
    324   let cast8signed = cast Int8s.cast
    325   let cast16unsigned = cast Int16u.cast
    326   let cast16signed = cast Int16s.cast
    327   let cast32 = cast Int32.cast
     316  (** Sign or 0 extensions from various bounded integers. *)
     317  let cast8unsigned = cast (Int.zero_ext 8)
     318  let cast8signed = cast (Int.sign_ext 8)
     319  let cast16unsigned = cast (Int.zero_ext 16)
     320  let cast16signed = cast (Int.sign_ext 16)
     321  let cast32 = cast (Int.zero_ext 32)
    328322
    329323
    … …  
    335329    | Val_int i1, Val_int i2 -> Val_int (f i1 i2)
    336330    | _ -> Val_undef
    337 
    338   let binary_intu_op f v1 v2 = match v1, v2 with
    339     | Val_int i1, Val_int i2 ->
    340       Val_int (Int.cast (f (Intu.cast i1) (Intu.cast i2)))
    341     | _, _ -> Val_undef
    342 
    343   let binary_int_cmp f v1 v2 = match v1, v2 with
    344     | Val_int i1, Val_int i2 -> of_bool (f i1 i2)
    345     | _, _ -> Val_undef
    346 
    347   let binary_intu_cmp f v1 v2 = match v1, v2 with
    348     | Val_int i1, Val_int i2 ->
    349       of_bool (f (Intu.cast i1) (Intu.cast i2))
    350     | _, _ -> Val_undef
    351331
    352332  let unary_float_op f = function
    … …  
    431411  let succ v = add v (Val_int Int.one)
    432412
    433   (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
    434       this substraction overflows. *)
    435   let sub_and_of v1 v2 = match v1, v2 with
     413  (** [sub_and_uf v1 v2] returns the substraction of [v1] and [v2], and whether
     414      this substraction underflows. *)
     415  let sub_and_uf v1 v2 = match v1, v2 with
    436416    | Val_int i1, Val_int i2 ->
    437       (Val_int (Int.sub i1 i2), of_bool (Int.sub_of i1 i2))
     417      (Val_int (Int.sub i1 i2), of_bool (Int.sub_uf i1 i2))
    438418    | Val_ptr (b, off), Val_int i ->
    439419      (Val_ptr (b, Offset.sub off i),
    440        of_bool (Offset.sub_of off (Offset.cast i)))
     420       of_bool (Offset.sub_uf off (Offset.cast i)))
    441421    | Val_ptrh (b, off), Val_int i ->
    442422      (Val_ptrh (b, Offset.sub off i),
    443        of_bool (Offset.sub_of off (Offset.cast i)))
     423       of_bool (Offset.sub_uf off (Offset.cast i)))
    444424    | Val_ptrl (b, off), Val_int i ->
    445425      (Val_ptrl (b, Offset.sub off i),
    446        of_bool (Offset.sub_of off (Offset.cast i)))
     426       of_bool (Offset.sub_uf off (Offset.cast i)))
    447427    | Val_ptr (b1, off1), Val_ptr (b2, off2)
    448428    | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
    449429    | Val_ptrl (b1, off1), Val_ptrl (b2, off2) when Block.eq b1 b2 ->
    450430      (Val_int (Int.cast (Offset.sub off1 off2)),
    451        of_bool (Offset.sub_of off1 off2))
     431       of_bool (Offset.sub_uf off1 off2))
    452432    | _, _ -> (Val_undef, Val_undef)
    453433
    454   let sub v1 v2 = fst (sub_and_of v1 v2)
    455   let sub_of v1 v2 = snd (sub_and_of v1 v2)
     434  let sub v1 v2 = fst (sub_and_uf v1 v2)
     435  let sub_uf v1 v2 = snd (sub_and_uf v1 v2)
    456436
    457437  let pred v = sub v (Val_int Int.one)
    … …  
    471451  let divu v1 v2 =
    472452    if is_zero v2 then Val_undef
    473     else binary_intu_op Intu.div v1 v2
     453    else binary_int_op Int.divu v1 v2
    474454
    475455  let modulo v1 v2 =
    … …  
    477457    else binary_int_op Int.modulo v1 v2
    478458
    479   let modu v1 v2 =
     459  let modulou v1 v2 =
    480460    if is_zero v2 then Val_undef
    481     else binary_intu_op Intu.modulo v1 v2
     461    else binary_int_op Int.modulou v1 v2
    482462
    483463  let and_op = binary_int_op Int.logand
    … …  
    503483    | _ -> Val_undef
    504484
    505   let cmpp_eq f_int v1 v2 = match v1, v2 with
     485  let cmp f_int f_ptr v1 v2 = match v1, v2 with
    506486    | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
    507487    | Val_ptr (b1, off1), Val_ptr (b2, off2)
    508488    | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
    509     | Val_ptrl (b1, off1), Val_ptrl (b2, off2) ->
    510       of_bool ((Block.eq b1 b2) && (Offset.eq off1 off2))
    511     | _ -> Val_undef
    512 
    513   let cmpp_ne cmp_eq v1 v2 = notbool (cmp_eq v1 v2)
    514 
    515   let cmpp_lt f_int v1 v2 = match v1, v2 with
    516     | Val_int i1, Val_int i2 -> of_bool (f_int i1 i2)
    517     | Val_ptr (b1, off1), Val_ptr (b2, off2)
    518     | Val_ptrh (b1, off1), Val_ptrh (b2, off2)
    519     | Val_ptrl (b1, off1), Val_ptrl (b2, off2) ->
    520       of_bool ((Block.lt b1 b2) ||
    521                ((Block.eq b1 b2) && (Offset.lt off1 off2)))
    522     | _ -> Val_undef
    523 
    524   let cmpp_ge cmp_lt v1 v2 = notbool (cmp_lt v1 v2)
    525   let cmpp_le cmp_lt cmp_eq v1 v2 = orbool (cmp_lt v1 v2) (cmp_eq v1 v2)
    526   let cmpp_gt cmp_le v1 v2 = notbool (cmp_le v1 v2)
    527 
    528   let cmp_eq = cmpp_eq Int.eq
    529   let cmp_ne = cmpp_ne cmp_eq
    530   let cmp_lt = cmpp_lt Int.lt
    531   let cmp_ge = cmpp_ge cmp_lt
    532   let cmp_le = cmpp_le cmp_lt cmp_eq
    533   let cmp_gt = cmpp_gt cmp_le
    534 
    535   let cmp_eq_u = cmpp_eq Intu.eq
    536   let cmp_ne_u = cmpp_ne cmp_eq_u
    537   let cmp_lt_u = cmpp_lt Intu.lt
    538   let cmp_ge_u = cmpp_ge cmp_lt_u
    539   let cmp_le_u = cmpp_le cmp_lt_u cmp_eq_u
    540   let cmp_gt_u = cmpp_gt cmp_le_u
     489    | Val_ptrl (b1, off1), Val_ptrl (b2, off2) when Block.eq b1 b2 ->
     490      of_bool (f_ptr off1 off2)
     491    | _ -> Val_undef
     492
     493  let cmp_eq = cmp Int.eq Offset.eq
     494  let cmp_ne = cmp Int.neq Offset.neq
     495  let cmp_lt = cmp Int.lt Offset.lt
     496  let cmp_ge = cmp Int.ge Offset.ge
     497  let cmp_le = cmp Int.le Offset.le
     498  let cmp_gt = cmp Int.gt Offset.gt
     499
     500  let cmp_eq_u = cmp Int.eq Offset.eq
     501  let cmp_ne_u = cmp Int.neq Offset.neq
     502  let cmp_lt_u = cmp Int.ltu Offset.ltu
     503  let cmp_ge_u = cmp Int.geu Offset.geu
     504  let cmp_le_u = cmp Int.leu Offset.leu
     505  let cmp_gt_u = cmp Int.gtu Offset.gtu
    541506
    542507  let cmp_eq_f = binary_float_cmp (=)

  • Deliverables/D2.2/8051/src/common/value.mli

    r486 r619  
    6464  val undef     : t
    6565
    66   (** [cast8unsigned v] returns undefined for non-integer values. For integer
    67       values, it supposes that the value is a 8 bit unsigned integer. It will
    68       return the integer value that represents the same quantity, but using
    69       every bits. The other cast operations behave the same way. *)
     66
     67  (** Sign or 0 extensions from various bounded integers. *)
    7068  val cast8unsigned  : t -> t
    7169  val cast8signed    : t -> t   
    … …  
    9694  val add_and_of : t -> t -> (t * t)
    9795  val add        : t -> t -> t
    98   (** [add_of v1 v2] returns the 1 value if the sum of [v1] and [v2]
    99       overflows, and 0 otherwise. *)
     96  (** [add_of v1 v2] returns the [1] value if the sum of [v1] and [v2]
     97      overflows, and [0] otherwise. *)
    10098  val add_of     : t -> t -> t
    10199  (** [sub_and_of v1 v2] returns the substraction of [v1] and [v2], and whether
    102       this substraction overflows. *)
    103   val sub_and_of : t -> t -> (t * t)
     100      this substraction underflows. *)
     101  val sub_and_uf : t -> t -> (t * t)
    104102  val sub        : t -> t -> t
    105   (** [sub_of v1 v2] returns the 1 value if the substraction of [v1] and [v2]
    106       overflows, and 0 otherwise. *)
    107   val sub_of     : t -> t -> t
     103  (** [sub_of v1 v2] returns the [1] value if the substraction of [v1] and [v2]
     104      underflows, and [0] otherwise. *)
     105  val sub_uf     : t -> t -> t
    108106  val mul        : t -> t -> t
    109107  val div        : t -> t -> t
    110108  val divu       : t -> t -> t
    111109  val modulo     : t -> t -> t
    112   val modu       : t -> t -> t
     110  val modulou    : t -> t -> t
    113111  val and_op     : t -> t -> t
    114112  val or_op      : t -> t -> t

  • Deliverables/D2.2/8051/src/dev_test.ml

    r486 r619  
    99
    1010  let f filename =
    11 
    12     ASMInterpret.parse_and_interpret_hex filename
    13 
    14 (*
     11    let target = Languages.Clight in
    1512    let print = false in
    16     let interpret = false in
    17     let labelize = false in
    18     let target = Languages.ASM in
     13    let interpret = true in
    1914    let p = Languages.parse Languages.Clight filename in
    20     let p = if labelize then Languages.labelize p else p in
     15    let p = Languages.labelize p in
    2116    let ps = Languages.compile false Languages.Clight target p in
    2217    let f f' p = match Languages.language_of_ast p with
    … …  
    2419      | _ -> ()
    2520    in
    26     if print then List.iter (f (Languages.save filename)) ps ;
    27     if interpret then List.iter (f (fun p -> ignore (Languages.interpret p))) ps
    28 *)
     21    if print then List.iter (f (Languages.save false filename)) ps ;
     22    if interpret then
     23      List.iter (f (fun p -> ignore (Languages.interpret true p))) ps
    2924  in
    3025

  • Deliverables/D2.2/8051/src/languages.ml

    r486 r619  
    199199(* FIXME *)
    200200let instrument costs_mapping = function
    201   | AstClight p ->
    202     AstClight (ClightAnnotator.instrument p costs_mapping)
     201  | AstClight p ->
     202    let (p', cost_incr) = ClightAnnotator.instrument p costs_mapping in
     203    (AstClight p', cost_incr)
    203204  | AstCminor p ->
    204     AstCminor (CminorAnnotator.instrument p costs_mapping)
     205    let (p', cost_incr) = CminorAnnotator.instrument p costs_mapping in
     206    (AstCminor p', cost_incr)
    205207  | p ->
    206208    Error.warning "during instrumentation"
    … …  
    208210         "Instrumentation is not implemented for source language `%s'."
    209211         (to_string (language_of_ast p)));
    210     p
     212    (p, "")
    211213
    212214let annotate input_ast final =
    … …  
    232234    ASMPrinter.print_program p
    233235
    234 let save filename ast =
    235   let output_filename =
    236     Misc.SysExt.alternative
    237       (Filename.chop_extension filename
    238        ^ "." ^ extension (language_of_ast ast))
    239   in
     236let save exact_output filename ast =
     237  let ext_chopped_filename =
     238    if exact_output then filename
     239    else
     240      try Filename.chop_extension filename
     241      with Invalid_argument ("Filename.chop_extension") -> filename in
     242  let ext_filename =
     243    ext_chopped_filename ^ "." ^ extension (language_of_ast ast) in
     244  let output_filename =
     245    if exact_output then ext_filename
     246    else Misc.SysExt.alternative ext_filename in
    240247  let cout = open_out output_filename in
    241248  output_string cout (string_output ast);
    … …  
    243250  close_out cout
    244251
    245 let interpret = function
     252let save_cost_incr filename cost_incr =
     253  let cout = open_out (filename ^ ".cerco") in
     254  output_string cout cost_incr;
     255  flush cout;
     256  close_out cout
     257
     258let interpret print_result = function
    246259  | AstClight p ->
    247     ClightInterpret.interpret false p
     260    ClightInterpret.interpret print_result p
    248261  | AstCminor p ->
    249     CminorInterpret.interpret false p 
     262    CminorInterpret.interpret print_result p 
    250263  | AstRTLabs p ->
    251     RTLabsInterpret.interpret p
     264    RTLabsInterpret.interpret print_result p
    252265  | AstRTL p ->
    253     RTLInterpret.interpret p
     266    RTLInterpret.interpret print_result p
    254267  | AstERTL p ->
    255     ERTLInterpret.interpret p
     268    ERTLInterpret.interpret print_result p
    256269  | AstLTL p ->
    257     LTLInterpret.interpret p
     270    LTLInterpret.interpret print_result p
    258271  | AstLIN p ->
    259     LINInterpret.interpret p
     272    LINInterpret.interpret print_result p
    260273  | AstASM p ->
    261     ASMInterpret.interpret p
     274    ASMInterpret.interpret print_result p

  • Deliverables/D2.2/8051/src/languages.mli

    r486 r619  
    6161val labelize : ast -> ast
    6262
    63 (** [annotate input_ast target_ast] inserts cost annotations into the
    64     input AST from the (final) target AST. *)
    65 val annotate : ast -> ast -> ast
     63(** [annotate input_ast target_ast] inserts cost annotations into the input AST
     64    from the (final) target AST. It also returns the name of the cost increment
     65    function *)
     66val annotate : ast -> ast -> (ast * string)
    6667
    67 (** [interpret ast] runs the program [ast] from the default initial
    68     configuration. This interpretation may emit some cost labels. *)
    69 val interpret : ast -> CostLabel.t list
     68(** [interpret print_result ast] runs the program [ast] from the default initial
     69    configuration. This interpretation may emit some cost labels. If
     70    [print_result] is [true], then the result of the interpretations is
     71    output. *)
     72val interpret : bool -> ast -> AST.trace
    7073
    7174(** {2 Serialization} *)
    7275
    73 (** [save filename input_ast] pretty prints [input_ast] in a fresh
    74     file whose name is prefixed by [filename] and whose extension
    75     is deduced from the language of the AST. *)
    76 val save : string -> ast -> unit
     76(** [save exact_output filename input_ast] pretty prints [input_ast] in a file
     77    whose name is prefixed by [filename] and whose extension is deduced from the
     78    language of the AST. If [exact_output] is false then the written file will
     79    be fresh. *)
     80val save : bool -> string -> ast -> unit
     81
     82(** [save_cost_incr filename cost_incr] prints the name of the cost increment
     83    function [cost_incr] in the file prefixed by [filename] and extended with
     84    ".cost". If the file already exists, it is overwritten. *)
     85val save_cost_incr : string -> string -> unit
    7786
    7887(** [from_string s] parses [s] as an intermediate language name. *)

  • Deliverables/D2.2/8051/src/options.ml

    r486 r619  
    2828let input_files ()              = !input_files
    2929
     30let output_files                = ref None
     31let set_output_files s          = output_files := Some s
     32let get_output_files ()         = !output_files
     33
    3034let annotation_flag             = ref false
    3135let request_annotation          = (:=) annotation_flag
    … …  
    3943let set_debug                   = (:=) debug_flag
    4044let is_debug_enabled ()         = !debug_flag
     45
     46let print_result_flag           = ref false
     47let set_print_result            = (:=) print_result_flag
     48let is_print_result_enabled ()  = !print_result_flag
    4149
    4250let dev_test                    = ref false
    … …  
    6472  " Debugging mode.";
    6573
     74  "-o", Arg.String set_output_files,
     75  " Prefix of the output files.";
     76
     77  "-res", Arg.Set print_result_flag,
     78  " Print the result of interpretations.";
     79
    6680  "-dev", Arg.Set dev_test,
    6781  " Playground for developers.";

  • Deliverables/D2.2/8051/src/options.mli

    r486 r619  
    2121val input_files    : unit -> string list
    2222
     23(** {2 Output files} *)
     24val set_output_files : string -> unit
     25val get_output_files : unit -> string option
     26
    2327(** {2 Verbose mode} *)
    2428val is_debug_enabled : unit -> bool
    2529
     30(** {2 Print results requests} *)
     31val is_print_result_enabled : unit -> bool
     32
    2633(** {2 Developers' playground} *)
    2734val is_dev_test_enabled : unit -> bool

  • Deliverables/D2.2/8051/src/utilities/miscPottier.ml

    r486 r619  
    3232  aux 0 l
    3333
     34let rec last = function
     35  | [] -> raise Not_found
     36  | [a] -> a
     37  | _ :: l -> last l
     38
    3439(* [split a i] splits the list a in two lists: one with the elements
    3540   up until the [i]th (exclusive) and one with the rest. *)
    … …  
    4045    let (l1, l2) = split (List.tl l) (i-1) in
    4146    ((List.hd l) :: l1, l2)
     47
     48(* [split_last l] returns the list [l] without its last element and its last
     49   element. Raises Invalid_argument "MiscPottier.split_last" if the list is
     50   empty. *)
     51
     52let split_last l = match split l ((List.length l) - 1) with
     53  | l', last :: _ -> (l', last)
     54  | _ -> raise (Invalid_argument "MiscPottier.split_last")
    4255
    4356let rec update_list_assoc a b = function

  • Deliverables/D2.2/8051/src/utilities/miscPottier.mli

    r486 r619  
    66val index_of : 'a -> 'a list -> int
    77
    8 val foldi: (int -> 'a -> 'b -> 'a) -> 'a -> 'b list -> 'a
     8val foldi : (int -> 'a -> 'b -> 'a) -> 'a -> 'b list -> 'a
    99
    10 val iteri: (int -> 'a -> unit) -> 'a list -> unit
     10val iteri : (int -> 'a -> unit) -> 'a list -> unit
    1111
    12 val mapi: (int -> 'a -> 'b) -> 'a list -> 'b list
     12val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
    1313
    14 (* [split a i] splits the list a in two lists: one with the elements
     14(* Raises Not_found if the list is empty. *)
     15val last : 'a list -> 'a
     16
     17(* [split l i] splits the list [l] in two lists: one with the elements
    1518   up until the [i]th (exclusive) and one with the rest. *)
    1619
    1720val split: 'a list -> int -> ('a list * 'a list)
     21
     22(* [split_last l] returns the list [l] without its last element and its last
     23   element. Raises Invalid_argument "MiscPottier.split_last" if the list is
     24   empty. *)
     25
     26val split_last : 'a list -> ('a list * 'a)
    1827
    1928val update_list_assoc: 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list

  • Deliverables/D2.2/8051/tests/clight/array.c

    r486 r619  
    3939}
    4040
    41 main(){
     41int main(){
    4242        int t[10] = {1,2,3,4,5,6,7,8,9,0};
    4343        int a = array_local();
    … …  
    4545        int c = array_param(t,2,3);
    4646        return a+b+c; //19
    47         //return b;
     47        // return b;
    4848}
Note: See TracChangeset for help on using the changeset viewer.