Changeset 619 for Deliverables/D2.2/8051/src/LTL

Timestamp:

Mar 2, 2011, 3:27:41 PM (9 years ago)

Author:

ayache

Message:

Update of D2.2 from Paris.

Location:

Deliverables/D2.2/8051/src/LTL

Files:

• LTLInterpret.ml (modified) (5 diffs)
• LTLInterpret.mli (modified) (1 diff)

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

@@ -45 +45 @@
       renv   : hdw_reg_env ;
       mem    : memory ;
-      trace  : AST.trace }
+      trace  : CostLabel.t list }
 
 
@@ -371 +371 @@
     (string_of_reg I8051.dph) (string_of_reg I8051.dpl)
 
-let rec iter_small_step lbls_offs st =
+let compute_result st =
+  let v = get_reg I8051.dpl st in
+  if Val.is_int v then IntValue.Int8.cast (Val.to_int_repr v)
+  else IntValue.Int8.zero
+
+let rec iter_small_step print_result lbls_offs st =
 (*
     print_state lbls_offs st ;
@@ -377 +382 @@
   match fetch_stmt lbls_offs st with
     | LTL.St_return when Val.eq (return_pc st) Val.zero ->
-(*
-      print_state lbls_offs st ;
-      print_result st ;
-*)
-      List.rev st.trace
+      let (res, cost_labels) as trace =
+        (compute_result st, List.rev st.trace) in
+      if print_result then
+        Printf.printf "LTL: %s\n%!" (IntValue.Int8.to_string res) ;
+      trace
     | stmt ->
       let st' = interpret_stmt lbls_offs st stmt in
-      iter_small_step lbls_offs st'
+      iter_small_step print_result lbls_offs st'
 
 
@@ -446 +451 @@
    - Initialize the carry flag to 0. *)
 
-let interpret p = match p.LTL.main with
-  | None -> []
+let interpret print_result p = match p.LTL.main with
+  | None -> (IntValue.Int8.zero, [])
   | Some main ->
     let lbls_offs = labels_offsets p in
@@ -457 +462 @@
     let st = init_main_call lbls_offs st main in
     let st = change_carry st Val.zero in
-    iter_small_step lbls_offs st
+    iter_small_step print_result lbls_offs st

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

@@ -3 +3 @@
     return the trace of cost labels encountered. *)
 
-val interpret: LTL.program -> AST.trace
+val interpret: bool -> LTL.program -> AST.trace