Smt backend - #223
Conversation
|
Oops, should have predicted that failure 💀 |
b68a478 to
c9be566
Compare
0f02bdc to
903c258
Compare
ncough
left a comment
ncough
left a comment
There was a problem hiding this comment.
I'm not quite done reading through yet, but in the interest of not holding anything up, here are some things I have found. I think most are me just not knowing bincaml :)
| | `INTADD -> atom "+" | ||
| | `INTMUL -> atom "*" | ||
| | `INTSUB -> atom "-" | ||
| | `INTDIV -> atom "/" |
There was a problem hiding this comment.
Probably should be div, / is for reals.
| They should be order invariant thanks to SSA, | ||
| however the added dependence on the termination | ||
| condition requires them after it's declared. *) | ||
| CCVector.append_list final_edge assert_stmts; |
There was a problem hiding this comment.
I am just glancing through, so maybe completely wrong. Is it safe here to reorder asserts and assumes? Or are assumes fixed to entry?
| type_err "non-equal ite branches : %s %s" (Types.to_string arg1) | ||
| (Types.to_string arg2); | ||
| ] | ||
| | [ Types.Boolean; arg1 ] -> [] |
There was a problem hiding this comment.
I'm probably missing something, but this case doesn't make a lot of sense to me. What does the single argument case return if the condition is false?
|
|
||
| type intrin = [ `Cases (** choose first argument that is defined *) ] | ||
| type intrin = | ||
| [ `Cases | `IfThenElse (** choose first argument that is defined *) ] |
There was a problem hiding this comment.
Is the comment on the wrong variant?
| let invariants = | ||
| Block.fold_forwards ~phi:const | ||
| ~f:(fun acc stmt -> | ||
| match stmt with Stmt.Instr_Assert { body } -> body :: acc | _ -> acc) |
There was a problem hiding this comment.
Will this include asserts after a statement? Not sure that's right.
|
|
||
| (* Add havoc statements. *) | ||
| let havocs = | ||
| Block.free_vars header_block |
There was a problem hiding this comment.
Is this the variables mentioned in the block, or the live variables across it? Should be the latter. I guess SSA should guarantee these are the same, but does this pass assume SSA?
| in | ||
|
|
||
| (* Update header with new statements. *) | ||
| let header_block = Block.append_stmts header_block (havocs @ assumes) in |
There was a problem hiding this comment.
This places havoc and assume after loop header statements? I'd assume they go just after the asserts.
agle
left a comment
agle
left a comment
There was a problem hiding this comment.
Nick's already looked at the loop stuff so I'll just comment on this part
| function calls which are sensitive to context in program. *) | ||
| let rvar_map (program : Program.t) = | ||
| ambiguities program | ||
| (* Map all ambiguous variables to as expressions. *) |
There was a problem hiding this comment.
I may be misunderstanding but is this to deal with locals that share names with different types in different procedures? If so could you explain briefly in a comment please.
Is it dealing with local variables across different procedures? IMO it would be safer to always mangle local variables with the procedure name, coincident names that are not defined locally in different procedures would constitute an malformed program (I believe there is a check for this but I may be wrong). Sharing definitions of local variables with the same name across different procedures seems to risk funny semantics- creating invalid constraints between locals of different procedures.
For verifying a single procedure at a time, I think you could define locals after the (push) and they will be discarded after the (pop); but without mangling this could still restrict how easy it is to share subgoals between different procedure checks (it requires you pop before analysing another procedure).
Kait suggested it might be to do with inlining definitinos of types where variables are only annotated with their name; in that case it doesn't seem safe to include all local variables in the one map; they might just have different types in different procedrues?
| let proc = Procedure.set_entry_block proc id in | ||
| Procedure.PG.map_graph | ||
| (fun g -> | ||
| Procedure.G.add_edge g (Procedure.Vert.End id) Procedure.Vert.Return) |
There was a problem hiding this comment.
I think an intermediate type would be simpler, rather than proc with flattened graph e.g. {reduced_proc: Stmt.t list, reach_end_pred: Expr.t list;}), the caller can combine with the procedure id or copy of the procedure if needed.
| in | ||
| `Left (Stmt.Instr_Assert { body; attrib }) | ||
| | other -> `Right other) | ||
| in |
| (* Produce a list of builders for a procedure, with context. | ||
| Builder for local declarations + one for each statement. | ||
| Assertions produce a second builder for verification. *) | ||
| let build_procedure ~rvars (program : Program.t) (procedure : Program.proc) : |
There was a problem hiding this comment.
This could maybe be more efficient by passing a iter callback function ((builder * ctx) -> unit) which you call instead of CCVector.push. This means you could construct an Iter.t from this function to pass each intermediate check to the solver.
|
|
||
| (* Add invariants to a backedge, subbing phi node vars. *) | ||
| let add_invariants = | ||
| let phis = |
There was a problem hiding this comment.
Again, probably confused, but I would have thought you'd want to substitute phis based on what this edge is going to do. Here it seems to be substituting for header self loops?
| in | ||
| List.fold_left (transform_loop prog) proc loops | ||
|
|
||
| let transform (prog : Program.t) = |
There was a problem hiding this comment.
Just wanted to comment that I find this implementation quite clean and elegant. Doing something rather intricate in ~100 lines.
| match loop with | ||
| | { block; loop = PrimaryHeader { primary_header; headers; nodes } } -> | ||
| let entries = ProcIntra.compute_entries proc loop in | ||
| let backedges = ProcIntra.compute_backedges proc loop in |
There was a problem hiding this comment.
Is there any issue with calling these after altering proc? Maybe given a nested loop or something?
| in | ||
|
|
||
| (* Add ensures to return block. *) | ||
| match List.head_opt return_id with |
There was a problem hiding this comment.
Is there an invariant ensuring at most one of these?
| Stmt.Instr_Assume | ||
| { | ||
| attrib = StringMap.empty; | ||
| body = subst_var lhs @@ subst_expr args e; |
There was a problem hiding this comment.
A staged subst like this has caught me before. Can you have something like: callee(x): y ensures y = x + 1, invoked as z := callee(y)? Ends up with assume (z = z + 1).
4 participants
Part 1 of the smt backend, yay!
Adds a summary inlining transform which replaces all procedure summaries with asserts/assumes.
Uses this in the dump-smt command, which outputs an smt file that can currently verify basic IL programs (pure and only using primitive types). Support for fancy things like datatypes/matching are not done yet. Should be structured to check that all assertions/ensures are satisfied.
Also makes some changes to the existing smt infrastructure. Fixes some bugs with incorrect symbols for bitvector operations, and makes a mess getting ITEs working (there has to be a better way??).