Skip to content

Commit

Permalink
fixes trivial assertions (#1108)
Browse files Browse the repository at this point in the history
If an assertion doesn't contain a symbolic value then we were having
an empty set of constraints, which trivially were true. In other
words, `assert true` doesn't hold.

This PR fixes this by treating non-symbolic values as symbolic
constants.
  • Loading branch information
ivg authored May 29, 2020
1 parent 5a98402 commit fbaf190
Showing 1 changed file with 9 additions and 8 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -940,6 +940,12 @@ module SymbolicPrimitives(Machine : Primus.Machine.S) = struct
>>= fun () ->
Val.b1

let assertion_of_value x =
Executor.value x >>| (function
| None -> SMT.word (Primus.Value.to_word x)
| Some x -> x) >>|
SMT.formula ~refute:true

(* we can later add operators that manipulate the scopes
in which the assertion is checked *)
let assert_ name assertions =
Expand All @@ -948,17 +954,12 @@ module SymbolicPrimitives(Machine : Primus.Machine.S) = struct
Constraints.get Context.Scope.path >>= fun path ->
let constraints = Set.to_list @@ Set.union user path in
Machine.List.fold assertions ~init:constraints
~f:(fun constraints assertion ->
Executor.value assertion >>| function
| None -> constraints
| Some expr ->

SMT.formula ~refute:true expr :: constraints) >>|
SMT.check >>= function
~f:(fun constraints x ->
assertion_of_value x >>| fun assertion ->
assertion :: constraints) >>| SMT.check >>= function
| None -> Machine.return ()
| Some model ->
Val.Symbol.of_value name >>= fun name ->
Debug.msg "%s doesn't hold!" name >>= fun () ->
Executor.inputs >>| Seq.to_list >>= fun inputs ->
report (name,model,inputs)) >>= fun () ->
Val.b1
Expand Down

0 comments on commit fbaf190

Please sign in to comment.