Fixed a bug with constants in guards.

src/jimplefront/jstar.ml

@@ -180,7 +180,8 @@ let main () =
     prof_phase "topl preprocessing";
     let cores = ToplPreprocessor.instrument_procedures cores in
     let topls = ToplPreprocessor.read_properties !topl_files in
-    let topls = List.map ToplPreprocessor.parse_values topls in
+    (*  Remove this as it messes up true/false
+        let topls = List.map ToplPreprocessor.parse_values topls in *)
     let topl_monitor = ToplPreprocessor.compile programs topls in
     let question =
       { Core.q_procs = topl_monitor @ cores

src/topl/toplPreprocessor.ml

@@ -49,12 +49,21 @@ let get_vertices p =
   let f acc t = t.A.source :: t.A.target :: acc in
   "start" :: "error" :: List.fold_left f [] p.A.transitions
 
+let int_match x = Str.string_match (Str.regexp "[0-9]+$") x 0
+let str_match x = Str.string_match (Str.regexp "\".*\"$") x 0
+
 (* }}} *)
 (* conversion to ToplMonitor representation *) (* {{{ *)
 let convert_guard guard =
   let convert = function
     | A.Variable (vr, i) -> TM.EqReg (i, vr)
-    | A.Constant (vl, i) -> TM.EqCt (i, vl) in
+    | A.Constant (vl, i) -> match vl with
+        | "true" -> TM.Not (TM.EqCt (i, E.mk_int_const "0"))
+        | "false" -> TM.EqCt (i, E.mk_int_const "0")
+        | x -> if int_match x then TM.EqCt (i, E.mk_int_const x) 
+          else if str_match x then TM.EqCt (i, E.mk_string_const x) 
+          else failwith ("Asked to convert an invalid constant ("^x^")")
+  in
   TM.And (List.map convert guard.A.value_guards)
 
 let convert_action = List.fold_left (fun m (k, v) -> TM.VMap.add k v m) TM.VMap.empty
@@ -131,6 +140,7 @@ let construct_monitor ts =
 
 (* }}} *)
 (* parse values *) (* {{{ *)
+(* Remover this as it messes up true/false 
 let parse_values topl =
   let pv_v v = Jparser.jargument Jlexer.token & Lexing.from_string v in
   let pv_vg = function
@@ -141,6 +151,7 @@ let parse_values topl =
   let pv_label l = { l with A.guard = pv_guard l.A.guard } in
   let pv_transition t = { t with A.labels = List.map pv_label t.A.labels } in
   { topl with A.transitions = List.map pv_transition topl.A.transitions }
+*)
 
 (* }}} *)
 (* specialize monitor *) (* {{{ *)

src/topl/toplPreprocessor.mli

@@ -1,8 +1,9 @@
 val read_properties : string list -> (string, string) Topl.PropAst.t list
-val parse_values
+(* val parse_values
   : ('a, string) Topl.PropAst.t -> ('a, ToplMonitor.value) Topl.PropAst.t
+*)
 val compile
   : Jimple_global_types.jimple_file list
-    -> (ToplMonitor.register, ToplMonitor.value) Topl.PropAst.t list
+    -> (ToplMonitor.register, string) Topl.PropAst.t list
     -> Core.ast_procedure list
 val instrument_procedures : Core.ast_procedure list -> Core.ast_procedure list

src/topl/toplSpecs.ml

@@ -19,6 +19,13 @@ let mk_pvar x = Expr.mk_var x
 let mk_evar x = Expr.mk_var ("_"^x)
 let mk_true = Expr.mk_big_star []
 
+(* This function correctly encodes conditions x = true/false. 
+   Ideally, in the future it should also handle integers. *)
+let mk_eq_to x = function
+(*| "true" -> Expr.mk_neq x (Expr.mk_int_const "0")
+  | "false" -> Expr.mk_eq x (Expr.mk_int_const "0") *)
+  | y -> Expr.mk_eq x y
+
 let wrap_call_arg a = mk_pvar (CoreOps.parameter a)
 
 let get_specs_for_enqueue pv =
@@ -27,10 +34,10 @@ let get_specs_for_enqueue pv =
   let specs = Core.TripleSet.create 0 in
   for i = 0 to q_sz - 1 do begin
     let e = pv.queue.(i) in
-    let pre = Expr.mk_eq pv.size (Expr.mk_string_const (string_of_int i)) in
+    let pre = Expr.mk_eq pv.size (Expr.mk_int_const (string_of_int i)) in
     let post = Expr.mk_big_star
       (let cp i = Expr.mk_eq e.(i) (wrap_call_arg i) in
-      Expr.mk_eq pv.size (Expr.mk_string_const (string_of_int (i+1)))
+      Expr.mk_eq pv.size (Expr.mk_int_const (string_of_int (i+1)))
       :: List.map cp (range 0 e_sz)) in
     let modifies = pv.size :: List.map (fun i -> e.(i)) (range 0 e_sz) in
     let modifies = List.map Expr.bk_var modifies in
@@ -209,15 +216,16 @@ let rec remove_thors f =
 
 (* Returns a formula given guard gd, assuming that value i of each event is stored in
    e.(i+1) in event queue *)
+(* NT: The EqCt case has been slightly hacked to address equality with booleans *)
 let rec guard_conditions gd e st =
   match gd with
      | TM.True -> mk_true
-     | TM.EqCt (i,v) -> Expr.mk_eq e.(i+1) v
+     | TM.EqCt (i,v) -> mk_eq_to e.(i+1) v
      | TM.EqReg (i,r) -> Expr.mk_eq e.(i+1) (TM.RMap.find r st)
      | TM.Not g -> negate_formula (guard_conditions g e st)
      | TM.And gs -> Expr.mk_big_star (List.map (fun g -> guard_conditions g e st) gs)
 
-let obs_conditions e { TM.event_time; pattern } = (* failwith "TODO aksdanksd" *)
+let obs_conditions e { TM.event_time; pattern } =
 (* (* debug *) Format.printf "\nNow, the pattern has length: %d\n" (List.length pattern); *)
 (* (* debug *) List.iter (fun s -> Format.printf "- here is a pattern elt: %s\n" s) pattern;*)
    let ev_name = match event_time with
@@ -261,7 +269,7 @@ let step_conditions e st st' s =
 
 let pDeQu n pv el =
    let m = Array.length pv.queue in
-   (Expr.mk_eq pv.size (Expr.mk_string_const (string_of_int (m-n))))
+   (Expr.mk_eq pv.size (Expr.mk_int_const (string_of_int (m-n))))
    :: (logical_dequeue pv.queue el n)
 
 let pDeQu_modifies n pv el =
@@ -305,7 +313,7 @@ let get_specs_for_vertex t pv v s =
   let (el,ef) = make_logical_copy_of_queue pv.queue in
   let mM = Array.length pv.queue in
 (* (* debug *) Format.printf "Here is M: %d\n" mM; *)
-  let pQud = (Expr.mk_eq pv.size (Expr.mk_string_const (string_of_int mM))) :: ef in
+  let pQud = (Expr.mk_eq pv.size (Expr.mk_int_const (string_of_int mM))) :: ef in
   let l_sr0 = make_logical_copy_of_store pv.store 0 (-1) in
   let pInit = store_eq pv.store l_sr0 in
 (* (* debug *) Format.printf "Now, here is the pInit for %s: %a\n" v Psyntax.string_form pInit; *)