Skip to content

Commit

Permalink
Z3: Change accidentally changed things back to ctx
Browse files Browse the repository at this point in the history
  • Loading branch information
@michael-schwarz
michael-schwarz committed Dec 19, 2024
1 parent 196bf69 commit 7211045
Showing 1 changed file with 28 additions and 28 deletions.
56 changes: 28 additions & 28 deletions src/witness/z3/violationZ3.z3.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ struct
(* ("smt.core.minimize", "true"); *)
(* ("sat.core.minimize", "true"); *)
]
let man = mk_context cfg
let ctx = mk_context cfg

type var = varinfo

Expand All @@ -40,43 +40,43 @@ struct
let get_const m x =
match VarMap.find_opt x m with
| Some x -> x
| None -> Arithmetic.Integer.mk_const_s man (get_name x)
let sort = Arithmetic.Integer.mk_sort man
| None -> Arithmetic.Integer.mk_const_s ctx (get_name x)
let sort = Arithmetic.Integer.mk_sort ctx
let freshen env x =
VarMap.add x (Expr.mk_fresh_const man (get_name x) sort) env
VarMap.add x (Expr.mk_fresh_const ctx (get_name x) sort) env
end

let bool_to_int expr =
Boolean.mk_ite man expr (Arithmetic.Integer.mk_numeral_i man 1) (Arithmetic.Integer.mk_numeral_i man 0)
Boolean.mk_ite ctx expr (Arithmetic.Integer.mk_numeral_i ctx 1) (Arithmetic.Integer.mk_numeral_i ctx 0)

let int_to_bool expr =
Boolean.mk_distinct man [expr; Arithmetic.Integer.mk_numeral_i man 0]
Boolean.mk_distinct ctx [expr; Arithmetic.Integer.mk_numeral_i ctx 0]

let rec exp_to_expr env = function
| Const (CInt (i, _, _)) ->
Arithmetic.Integer.mk_numeral_s man (Z.to_string i)
Arithmetic.Integer.mk_numeral_s ctx (Z.to_string i)
| Lval (Var v, NoOffset) ->
Env.get_const env v
| BinOp (PlusA, e1, e2, TInt _) ->
Arithmetic.mk_add man [exp_to_expr env e1; exp_to_expr env e2]
Arithmetic.mk_add ctx [exp_to_expr env e1; exp_to_expr env e2]
| BinOp (MinusA, e1, e2, TInt _) ->
Arithmetic.mk_sub man [exp_to_expr env e1; exp_to_expr env e2]
Arithmetic.mk_sub ctx [exp_to_expr env e1; exp_to_expr env e2]
| BinOp (Mult, e1, e2, TInt _) ->
Arithmetic.mk_mul man [exp_to_expr env e1; exp_to_expr env e2]
Arithmetic.mk_mul ctx [exp_to_expr env e1; exp_to_expr env e2]
| BinOp (Eq, e1, e2, TInt _) ->
bool_to_int (Boolean.mk_eq man (exp_to_expr env e1) (exp_to_expr env e2))
bool_to_int (Boolean.mk_eq ctx (exp_to_expr env e1) (exp_to_expr env e2))
| BinOp (Ne, e1, e2, TInt _) ->
bool_to_int (Boolean.mk_distinct man [exp_to_expr env e1; exp_to_expr env e2])
bool_to_int (Boolean.mk_distinct ctx [exp_to_expr env e1; exp_to_expr env e2])
| BinOp (Gt, e1, e2, TInt _) ->
bool_to_int (Arithmetic.mk_gt man (exp_to_expr env e1) (exp_to_expr env e2))
bool_to_int (Arithmetic.mk_gt ctx (exp_to_expr env e1) (exp_to_expr env e2))
| BinOp (Lt, e1, e2, TInt _) ->
bool_to_int (Arithmetic.mk_lt man (exp_to_expr env e1) (exp_to_expr env e2))
bool_to_int (Arithmetic.mk_lt ctx (exp_to_expr env e1) (exp_to_expr env e2))
| BinOp (Ge, e1, e2, TInt _) ->
bool_to_int (Arithmetic.mk_ge man (exp_to_expr env e1) (exp_to_expr env e2))
bool_to_int (Arithmetic.mk_ge ctx (exp_to_expr env e1) (exp_to_expr env e2))
| BinOp (Le, e1, e2, TInt _) ->
bool_to_int (Arithmetic.mk_le man (exp_to_expr env e1) (exp_to_expr env e2))
bool_to_int (Arithmetic.mk_le ctx (exp_to_expr env e1) (exp_to_expr env e2))
| UnOp (LNot, e, TInt _) ->
bool_to_int (Boolean.mk_not man (int_to_bool (exp_to_expr env e)))
bool_to_int (Boolean.mk_not ctx (int_to_bool (exp_to_expr env e)))
| e ->
failwith @@ GobPretty.sprintf "exp_to_expr: %a" Cil.d_exp e

Expand All @@ -86,19 +86,19 @@ struct
let wp_assert env (from_node, (edge: MyARG.inline_edge), _) = match edge with
| MyARG.CFGEdge (MyCFG.Assign ((Var v, NoOffset), e)) ->
let env' = Env.freshen env v in
(env', [Boolean.mk_eq man (Env.get_const env v) (exp_to_expr env' e)])
(env', [Boolean.mk_eq ctx (Env.get_const env v) (exp_to_expr env' e)])
| MyARG.CFGEdge (MyCFG.Test (e, true)) ->
(env, [Boolean.mk_distinct man [exp_to_expr env e; Arithmetic.Integer.mk_numeral_i man 0]])
(env, [Boolean.mk_distinct ctx [exp_to_expr env e; Arithmetic.Integer.mk_numeral_i ctx 0]])
| MyARG.CFGEdge (MyCFG.Test (e, false)) ->
(env, [Boolean.mk_eq man (exp_to_expr env e) (Arithmetic.Integer.mk_numeral_i man 0)])
(env, [Boolean.mk_eq ctx (exp_to_expr env e) (Arithmetic.Integer.mk_numeral_i ctx 0)])
| MyARG.CFGEdge (MyCFG.Entry fd) ->
let env' = List.fold_left (fun acc formal ->
Env.freshen acc formal
) env fd.sformals
in
let eqs = List.mapi (fun i formal ->
let arg_vname = get_arg_vname i in
Boolean.mk_eq man (Env.get_const env formal) (Env.get_const env' arg_vname)
Boolean.mk_eq ctx (Env.get_const env formal) (Env.get_const env' arg_vname)
) fd.sformals
in
(env', eqs)
Expand All @@ -110,22 +110,22 @@ struct
in
let eqs = List.mapi (fun i arg ->
let arg_vname = get_arg_vname i in
Boolean.mk_eq man (Env.get_const env arg_vname) (exp_to_expr env' arg)
Boolean.mk_eq ctx (Env.get_const env arg_vname) (exp_to_expr env' arg)
) args
in
(env', eqs)
| MyARG.CFGEdge (MyCFG.Ret (None, fd)) ->
(env, [])
| MyARG.CFGEdge (MyCFG.Ret (Some e, fd)) ->
let env' = Env.freshen env return_vname in
(env', [Boolean.mk_eq man (Env.get_const env return_vname) (exp_to_expr env' e)])
(env', [Boolean.mk_eq ctx (Env.get_const env return_vname) (exp_to_expr env' e)])
| MyARG.InlineReturn (None, _, _) ->
(env, [])
| MyARG.InlineReturn (Some (Var v, NoOffset), _, _) ->
let env' = Env.freshen env v in
(env', [Boolean.mk_eq man (Env.get_const env v) (Env.get_const env' return_vname)])
(env', [Boolean.mk_eq ctx (Env.get_const env v) (Env.get_const env' return_vname)])
| _ ->
(* (env, Boolean.mk_true man) *)
(* (env, Boolean.mk_true ctx) *)
failwith @@ GobPretty.sprintf "wp_assert: %a" MyARG.pretty_inline_edge edge

let const_get_symbol (expr: Expr.expr): Symbol.symbol =
Expand All @@ -140,7 +140,7 @@ struct
| Unknown

let wp_path path =
let solver = Solver.mk_simple_solver man in
let solver = Solver.mk_simple_solver ctx in
let rec iter_wp revpath i env = match revpath with
| [] -> Feasible
| step :: revpath' ->
Expand All @@ -149,14 +149,14 @@ struct
| [] -> iter_wp revpath' (i - 1) env'
| [expr] -> do_assert revpath' i env' expr
| exprs ->
let expr = Boolean.mk_and man exprs in
let expr = Boolean.mk_and ctx exprs in
do_assert revpath' i env' expr
end

and do_assert revpath' i env' expr =
Logs.debug "%d: %s" i (Expr.to_string expr);

let track_const = Boolean.mk_const man (Symbol.mk_int man i) in
let track_const = Boolean.mk_const ctx (Symbol.mk_int ctx i) in
Solver.assert_and_track solver expr track_const;

let status = Solver.check solver [] in
Expand Down

0 comments on commit 7211045

Please sign in to comment.