Skip to content

Commit

Permalink
Fix missing unrolled iterations in YAML witness invariants
Browse files Browse the repository at this point in the history 
Unrolled loop heads are different nodes, which aren't actually loop heads.
For sound invariants, they must also be included if at a location if at least one is.
  • Loading branch information
@sim642
sim642 committed Nov 17, 2023
1 parent 952b90d commit 4ae3556
Showing 1 changed file with 76 additions and 76 deletions.
152 changes: 76 additions & 76 deletions src/witness/yamlWitness.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -245,29 +245,29 @@ struct
let entries =
if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then (
LH.fold (fun loc ns acc ->
let fundec = ref None in
let inv = List.fold_left (fun acc n ->
if is_invariant_node n then (
if List.exists is_invariant_node ns then (
let fundec = ref None in
let inv = List.fold_left (fun acc n ->
fundec := Some (Node.find_fundec n); (* TODO: fix location hack *)
let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
let lvals = local_lvals n local in
Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
)
else
acc
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let invs = WitnessUtil.InvariantExp.process_exp inv in
List.fold_left (fun acc inv ->
let location_function = (Option.get !fundec).svar.vname in
let location = Entry.location ~location:loc ~location_function in
let invariant = Entry.invariant (CilType.Exp.show inv) in
let entry = Entry.location_invariant ~task ~location ~invariant in
entry :: acc
) acc invs
| `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let invs = WitnessUtil.InvariantExp.process_exp inv in
List.fold_left (fun acc inv ->
let location_function = (Option.get !fundec).svar.vname in
let location = Entry.location ~location:loc ~location_function in
let invariant = Entry.invariant (CilType.Exp.show inv) in
let entry = Entry.location_invariant ~task ~location ~invariant in
entry :: acc
) acc invs
| `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
acc
)
else
acc
) (Lazy.force location2nodes) entries
)
Expand All @@ -279,28 +279,28 @@ struct
let entries =
if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then (
LH.fold (fun loc ns acc ->
let fundec = ref None in
let inv = List.fold_left (fun acc n ->
if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then (
if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then (
let fundec = ref None in
let inv = List.fold_left (fun acc n ->
fundec := Some (Node.find_fundec n); (* TODO: fix location hack *)
let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
)
else
acc
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let invs = WitnessUtil.InvariantExp.process_exp inv in
List.fold_left (fun acc inv ->
let location_function = (Option.get !fundec).svar.vname in
let location = Entry.location ~location:loc ~location_function in
let invariant = Entry.invariant (CilType.Exp.show inv) in
let entry = Entry.loop_invariant ~task ~location ~invariant in
entry :: acc
) acc invs
| `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let invs = WitnessUtil.InvariantExp.process_exp inv in
List.fold_left (fun acc inv ->
let location_function = (Option.get !fundec).svar.vname in
let location = Entry.location ~location:loc ~location_function in
let invariant = Entry.invariant (CilType.Exp.show inv) in
let entry = Entry.loop_invariant ~task ~location ~invariant in
entry :: acc
) acc invs
| `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
acc
)
else
acc
) (Lazy.force location2nodes) entries
)
Expand Down Expand Up @@ -442,29 +442,29 @@ struct
let invariants =
if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then (
LH.fold (fun loc ns acc ->
let fundec = ref None in
let inv = List.fold_left (fun acc n ->
if is_invariant_node n then (
if List.exists is_invariant_node ns then (
let fundec = ref None in
let inv = List.fold_left (fun acc n ->
fundec := Some (Node.find_fundec n); (* TODO: fix location hack *)
let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
let lvals = local_lvals n local in
Invariant.(acc || R.ask_local_node n ~local (Invariant {Invariant.default_context with lvals})) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
)
else
acc
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let invs = WitnessUtil.InvariantExp.process_exp inv in
List.fold_left (fun acc inv ->
let location_function = (Option.get !fundec).svar.vname in
let location = Entry.location ~location:loc ~location_function in
let invariant = CilType.Exp.show inv in
let invariant = Entry.location_invariant' ~location ~invariant in
invariant :: acc
) acc invs
| `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let invs = WitnessUtil.InvariantExp.process_exp inv in
List.fold_left (fun acc inv ->
let location_function = (Option.get !fundec).svar.vname in
let location = Entry.location ~location:loc ~location_function in
let invariant = CilType.Exp.show inv in
let invariant = Entry.location_invariant' ~location ~invariant in
invariant :: acc
) acc invs
| `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
acc
)
else
acc
) (Lazy.force location2nodes) invariants
)
Expand All @@ -476,28 +476,28 @@ struct
let invariants =
if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then (
LH.fold (fun loc ns acc ->
let fundec = ref None in
let inv = List.fold_left (fun acc n ->
if WitnessInvariant.emit_loop_head && WitnessUtil.NH.mem WitnessInvariant.loop_heads n then (
if WitnessInvariant.emit_loop_head && List.exists (WitnessUtil.NH.mem WitnessInvariant.loop_heads) ns then (
let fundec = ref None in
let inv = List.fold_left (fun acc n ->
fundec := Some (Node.find_fundec n); (* TODO: fix location hack *)
let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in
Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
)
else
acc
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let invs = WitnessUtil.InvariantExp.process_exp inv in
List.fold_left (fun acc inv ->
let location_function = (Option.get !fundec).svar.vname in
let location = Entry.location ~location:loc ~location_function in
let invariant = CilType.Exp.show inv in
let invariant = Entry.loop_invariant' ~location ~invariant in
invariant :: acc
) acc invs
| `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let invs = WitnessUtil.InvariantExp.process_exp inv in
List.fold_left (fun acc inv ->
let location_function = (Option.get !fundec).svar.vname in
let location = Entry.location ~location:loc ~location_function in
let invariant = CilType.Exp.show inv in
let invariant = Entry.loop_invariant' ~location ~invariant in
invariant :: acc
) acc invs
| `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
acc
)
else
acc
) (Lazy.force location2nodes) invariants
)
Expand Down

0 comments on commit 4ae3556

Please sign in to comment.