From f2a5f50aa3a2d034b949d52236e95dade470c9a5 Mon Sep 17 00:00:00 2001 From: Nikos Date: Fri, 29 Nov 2013 19:07:19 +0000 Subject: [PATCH] Fixed a bug with constants in guards. --- src/jimplefront/jstar.ml | 3 ++- src/topl/toplPreprocessor.ml | 13 ++++++++++++- src/topl/toplPreprocessor.mli | 5 +++-- src/topl/toplSpecs.ml | 20 ++++++++++++++------ 4 files changed, 31 insertions(+), 10 deletions(-) diff --git a/src/jimplefront/jstar.ml b/src/jimplefront/jstar.ml index 44dbec1..500511a 100644 --- a/src/jimplefront/jstar.ml +++ b/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 diff --git a/src/topl/toplPreprocessor.ml b/src/topl/toplPreprocessor.ml index 187e891..d0ad21e 100644 --- a/src/topl/toplPreprocessor.ml +++ b/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 *) (* {{{ *) diff --git a/src/topl/toplPreprocessor.mli b/src/topl/toplPreprocessor.mli index 1bd1bd6..4054c7a 100644 --- a/src/topl/toplPreprocessor.mli +++ b/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 diff --git a/src/topl/toplSpecs.ml b/src/topl/toplSpecs.ml index 927d4b0..797066b 100644 --- a/src/topl/toplSpecs.ml +++ b/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; *)