Skip to content

Commit

Permalink
Refactor YAML witness fundec lookup
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Nov 17, 2023
1 parent 4ae3556 commit 0fb479f
Showing 1 changed file with 12 additions and 16 deletions.
28 changes: 12 additions & 16 deletions src/witness/yamlWitness.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -246,20 +246,19 @@ struct
if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then (
LH.fold (fun loc ns acc ->
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 (||) *)
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
let location_function = fundec.svar.vname in
let location = Entry.location ~location:loc ~location_function in
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
Expand All @@ -280,19 +279,18 @@ struct
if entry_type_enabled YamlWitnessType.LoopInvariant.entry_type then (
LH.fold (fun loc ns acc ->
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 (||) *)
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
let location_function = fundec.svar.vname in
let location = Entry.location ~location:loc ~location_function in
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
Expand Down Expand Up @@ -443,20 +441,19 @@ struct
if invariant_type_enabled YamlWitnessType.InvariantSet.LocationInvariant.invariant_type then (
LH.fold (fun loc ns acc ->
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 (||) *)
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
let location_function = fundec.svar.vname in
let location = Entry.location ~location:loc ~location_function in
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
Expand All @@ -477,19 +474,18 @@ struct
if invariant_type_enabled YamlWitnessType.InvariantSet.LoopInvariant.invariant_type then (
LH.fold (fun loc ns acc ->
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 (||) *)
) (Invariant.bot ()) ns
in
match inv with
| `Lifted inv ->
let fundec = Node.find_fundec (List.hd ns) in (* TODO: fix location hack *)
let location_function = fundec.svar.vname in
let location = Entry.location ~location:loc ~location_function in
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
Expand Down

0 comments on commit 0fb479f

Please sign in to comment.