Conversation
…IFIER_nondet_bool
| | `Add -> | ||
| mk_or srk [mk_and srk (left.guard::(!left_eq)); | ||
| mk_and srk (right.guard::(!right_eq))] | ||
| | `And -> |
There was a problem hiding this comment.
Skolem constants must be renamed for And (e.g., "K.assume(sk1 = 0) and K.assume(sk1 = 1)" should the same as "K.assume(sk1 = 0 /\ sk2 = 1)", rather than false).
And also doesn't require introducing phi variables -- we can simply equate the right-hand sides of the transform (e.g., [x -> 0] /\ [x -> y] --> [x -> 0 when y = 0]).
| trs | ||
| guards | ||
| ([post], post) | ||
| ([ |
There was a problem hiding this comment.
Maybe cleaner to require post to be a state formula that is free of Skolem constants? Then rather using the guard of the path-to-error summary in GPS as the post-condition, we place the path-to-error as the last transition in trs and the post-condition is false. (Maybe there's some performance overhead with this encoding?)
There was a problem hiding this comment.
Whatever overhead there is might be worth it, because interpolate_or_get_model doesn't generate indicator variables for the post-condition, just the transitions. So the post-condition is always the guard of the path-to-error summary, I think. We generally want to allow it to be stronger.
| | None -> Interpretation.value model s))*) (*(Interpretation.empty srk)*) symbols in | ||
| logf "hashtable length: %d\n" (Hashtbl.length ss_inv); | ||
| logf "%a" Interpretation.pp m; | ||
| Format.print_flush (); |
| let assume_positive = K.assume gasexpr in | ||
| let decr_by_one = Syntax.mk_sub srk gas_var_term (mk_int 1) |> K.assign (VVal gas_var) in | ||
| K.mul assume_positive decr_by_one in | ||
| let initial_gas = K.havoc [ VVal gas_var ] in |
There was a problem hiding this comment.
Do we need the havoc? Should have the same effect if we leave it uninitialized.
| let new_vtx () = (Def.mk (Assume Bexpr.ktrue)).did | ||
|
|
||
| let instrument_with_gas (ts: TSG.t) gasexpr : TSG.t = | ||
| let modify_pre ts u = |
There was a problem hiding this comment.
There's a convenient function in WeightedGraph that helps with this kind of instrumentation---split_vertex wg u weight v takes all of the outgoing edges of u and makes them outgoing edges of v, and adds an edge from u to v with the given weight.
| let log_model prefix model = | ||
| logf "[model] %s: %a\n" prefix Interpretation.pp model | ||
|
|
||
| (* |
| in | ||
| (ts, err_loc) | ||
|
|
||
| module Summarizer = |
There was a problem hiding this comment.
I think we can omit all of the interprocedural logic until we have a better idea of what it's going to look like in the end.
|
|
||
| type equery = OverApprox | UnderApprox | ||
|
|
||
| module ART |
|
Oops --- sorry Zak, I should have opened a PR from this branch: https://github.com/ruijiefang/duet/tree/gps-improvements, or at least merge changes there into the |
|
Let us continue the discussion at #72 |
2 participants
No description provided.