Changeset 2967

Timestamp:

Mar 26, 2013, 6:54:12 PM (4 years ago)

Author:

sacerdot

Message:

Semantics changed so that a terminating joint program that returns an undefined
value is recognized as a terminating program that returns a dummy integer
(the maximum allowed one). This because the front-end type for termination is
int option and it does not discriminate between "non final" and "final with
no value". How is that possible in the front-end?

Files:

• extracted/traces.ml (modified) (13 diffs)
• src/joint/Traces.ma (modified) (1 diff)

extracted/traces.ml

@@ -157 +157 @@
     Joint_semantics.sem_params -> (AST.ident List.list ->
     Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
-let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_55 =
-  let { globals = globals0; ev_genv = ev_genv0 } = x_55 in
+let rec evaluation_params_rect_Type4 p h_mk_evaluation_params x_3 =
+  let { globals = globals0; ev_genv = ev_genv0 } = x_3 in
   h_mk_evaluation_params globals0 ev_genv0
 
@@ -164 +164 @@
     Joint_semantics.sem_params -> (AST.ident List.list ->
     Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
-let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_57 =
-  let { globals = globals0; ev_genv = ev_genv0 } = x_57 in
+let rec evaluation_params_rect_Type5 p h_mk_evaluation_params x_5 =
+  let { globals = globals0; ev_genv = ev_genv0 } = x_5 in
   h_mk_evaluation_params globals0 ev_genv0
 
@@ -171 +171 @@
     Joint_semantics.sem_params -> (AST.ident List.list ->
     Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
-let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_59 =
-  let { globals = globals0; ev_genv = ev_genv0 } = x_59 in
+let rec evaluation_params_rect_Type3 p h_mk_evaluation_params x_7 =
+  let { globals = globals0; ev_genv = ev_genv0 } = x_7 in
   h_mk_evaluation_params globals0 ev_genv0
 
@@ -178 +178 @@
     Joint_semantics.sem_params -> (AST.ident List.list ->
     Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
-let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_61 =
-  let { globals = globals0; ev_genv = ev_genv0 } = x_61 in
+let rec evaluation_params_rect_Type2 p h_mk_evaluation_params x_9 =
+  let { globals = globals0; ev_genv = ev_genv0 } = x_9 in
   h_mk_evaluation_params globals0 ev_genv0
 
@@ -185 +185 @@
     Joint_semantics.sem_params -> (AST.ident List.list ->
     Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
-let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_63 =
-  let { globals = globals0; ev_genv = ev_genv0 } = x_63 in
+let rec evaluation_params_rect_Type1 p h_mk_evaluation_params x_11 =
+  let { globals = globals0; ev_genv = ev_genv0 } = x_11 in
   h_mk_evaluation_params globals0 ev_genv0
 
@@ -192 +192 @@
     Joint_semantics.sem_params -> (AST.ident List.list ->
     Joint_semantics.genv -> 'a1) -> evaluation_params -> 'a1 **)
-let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_65 =
-  let { globals = globals0; ev_genv = ev_genv0 } = x_65 in
+let rec evaluation_params_rect_Type0 p h_mk_evaluation_params x_13 =
+  let { globals = globals0; ev_genv = ev_genv0 } = x_13 in
   h_mk_evaluation_params globals0 ev_genv0
 
@@ -336 +336 @@
     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
-let rec prog_params_rect_Type4 h_mk_prog_params x_81 =
+let rec prog_params_rect_Type4 h_mk_prog_params x_29 =
   let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
-    stack_sizes0 } = x_81
+    stack_sizes0 } = x_29
   in
   h_mk_prog_params prog_spars0 prog0 stack_sizes0
@@ -345 +345 @@
     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
-let rec prog_params_rect_Type5 h_mk_prog_params x_83 =
+let rec prog_params_rect_Type5 h_mk_prog_params x_31 =
   let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
-    stack_sizes0 } = x_83
+    stack_sizes0 } = x_31
   in
   h_mk_prog_params prog_spars0 prog0 stack_sizes0
@@ -354 +354 @@
     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
-let rec prog_params_rect_Type3 h_mk_prog_params x_85 =
+let rec prog_params_rect_Type3 h_mk_prog_params x_33 =
   let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
-    stack_sizes0 } = x_85
+    stack_sizes0 } = x_33
   in
   h_mk_prog_params prog_spars0 prog0 stack_sizes0
@@ -363 +363 @@
     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
-let rec prog_params_rect_Type2 h_mk_prog_params x_87 =
+let rec prog_params_rect_Type2 h_mk_prog_params x_35 =
   let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
-    stack_sizes0 } = x_87
+    stack_sizes0 } = x_35
   in
   h_mk_prog_params prog_spars0 prog0 stack_sizes0
@@ -372 +372 @@
     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
-let rec prog_params_rect_Type1 h_mk_prog_params x_89 =
+let rec prog_params_rect_Type1 h_mk_prog_params x_37 =
   let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
-    stack_sizes0 } = x_89
+    stack_sizes0 } = x_37
   in
   h_mk_prog_params prog_spars0 prog0 stack_sizes0
@@ -381 +381 @@
     (Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
     Nat.nat Types.option) -> 'a1) -> prog_params -> 'a1 **)
-let rec prog_params_rect_Type0 h_mk_prog_params x_91 =
+let rec prog_params_rect_Type0 h_mk_prog_params x_39 =
   let { prog_spars = prog_spars0; prog = prog0; stack_sizes =
-    stack_sizes0 } = x_91
+    stack_sizes0 } = x_39
   in
   h_mk_prog_params prog_spars0 prog0 stack_sizes0
@@ -674 +674 @@
        (Joint_semantics.spp'__o__msu_pars p).Joint_semantics.call_dest_for_main
      in
-     Errors.res_to_opt
-       (Obj.magic
-         (Monad.m_bind0 (Monad.max_def Errors.res0)
-           (Obj.magic
-             (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
-               pars.globals
-               (let p0 = Joint_semantics.spp'__o__spp p in
-               let globals0 = pars.globals in
-               let g = ge in g.Joint_semantics.ge) ret
-               st.Joint_semantics.st_no_pc)) (fun vals ->
-           Obj.magic (ByteValues.word_of_list_beval vals))))
+     (match Obj.magic
+              (Monad.m_bind0 (Monad.max_def Errors.res0)
+                (Obj.magic
+                  (p.Joint_semantics.spp'.Joint_semantics.msu_pars.Joint_semantics.read_result
+                    pars.globals
+                    (let p0 = Joint_semantics.spp'__o__spp p in
+                    let globals0 = pars.globals in
+                    let g = ge in g.Joint_semantics.ge) ret
+                    st.Joint_semantics.st_no_pc)) (fun vals ->
+                Obj.magic (ByteValues.word_of_list_beval vals))) with
+      | Errors.OK v -> Types.Some v
+      | Errors.Error x -> Types.Some (BitVector.maximum Integers.wordsize))
    | Bool.False -> Types.None)
 

src/joint/Traces.ma

@@ -235 +235 @@
  if eq_program_counter (pc … st) exit_pc' then
    let ret ≝ call_dest_for_main ?? p in
-   res_to_opt … (! vals ← read_result … ge ret st ;
+   match (! vals ← read_result … ge ret st ;
                Word_of_list_beval vals)
+   with
+   [ OK v ⇒ Some ? v
+   | Error _ ⇒ Some … (maximum ?) ]
  else None ?.