Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix incremental invariant parser for server mode #1017

Merged
merged 3 commits into from
Mar 22, 2023
Merged

Fix incremental invariant parser for server mode #1017

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6186df1
Fix incremental invariant parser for server mode
sim642 Mar 22, 2023
9edf77f
Re-enable server mode eval expression checking
sim642 Mar 22, 2023
4dfe744
Add declarations to invariant parser CIL checking
sim642 Mar 22, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 2 additions & 4 deletions src/util/server.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -691,8 +691,7 @@ let () =
let fundec = Node.find_fundec cfg_node in
let loc = UpdateCil.getLoc cfg_node in

(* Disable CIL check because incremental reparsing causes physically non-equal varinfos in this exp. *)
begin match InvariantParser.parse_cil ~check:false (ResettableLazy.force serv.invariant_parser) ~fundec ~loc exp_cabs with
begin match InvariantParser.parse_cil (ResettableLazy.force serv.invariant_parser) ~fundec ~loc exp_cabs with
| Ok exp -> exp
| Error e ->
Response.Error.(raise (make ~code:RequestFailed ~message:"CIL couldn't parse expression (undefined variables or side effects)" ()))
Expand Down Expand Up @@ -732,8 +731,7 @@ let () =
let fundec = Node.find_fundec cfg_node in
let loc = UpdateCil.getLoc cfg_node in

(* Disable CIL check because incremental reparsing causes physically non-equal varinfos in this exp. *)
begin match InvariantParser.parse_cil ~check:false (ResettableLazy.force serv.invariant_parser) ~fundec ~loc exp_cabs with
begin match InvariantParser.parse_cil (ResettableLazy.force serv.invariant_parser) ~fundec ~loc exp_cabs with
| Ok exp ->
let x = Arg.query n (EvalInt exp) in
{
Expand Down
43 changes: 34 additions & 9 deletions src/witness/witnessUtil.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,17 +114,43 @@ end
module InvariantParser =
struct
type t = {
genv: (string, Cabs2cil.envdata * Cil.location) Hashtbl.t;
global_vars: Cil.varinfo list;
}

module VarinfoH = Cilfacade.VarinfoH

let create (file: Cil.file): t =
let global_vars = List.filter_map (function
| Cil.GVar (v, _, _)
| Cil.GFun ({svar=v; _}, _) -> Some v
| _ -> None
) file.globals
in
{global_vars}
(* Reconstruct genv from CIL file instead of using genvironment,
because genvironment contains data from all versions of the file
and incremental update doesn't remove the excess. *)
let genv = Hashtbl.create (Hashtbl.length Cabs2cil.genvironment) in
let global_vars = VarinfoH.create 113 in (* Deduplicates varinfos from declarations and definitions. *)
Cil.iterGlobals file (function
| Cil.GType ({tname; _} as t, loc) ->
let name = "type " ^ tname in
Hashtbl.replace genv name (Cabs2cil.EnvTyp (TNamed (t, [])), loc)
| Cil.GCompTag ({cstruct; cname; _} as c, loc)
| Cil.GCompTagDecl ({cstruct; cname; _} as c, loc) ->
let name = (if cstruct then "struct" else "union") ^ " " ^ cname in
Hashtbl.replace genv name (Cabs2cil.EnvTyp (TComp (c, [])), loc)
| Cil.GEnumTag ({ename; eitems; _} as e, loc)
| Cil.GEnumTagDecl ({ename; eitems; _} as e, loc) ->
let typ = TEnum (e, []) in
let name = "enum " ^ ename in
Hashtbl.replace genv name (Cabs2cil.EnvTyp typ, loc);
List.iter (fun (name, exp, loc) ->
Hashtbl.replace genv name (Cabs2cil.EnvEnum (exp, typ), loc)
) eitems
| Cil.GVar (v, _, loc)
| Cil.GVarDecl (v, loc)
| Cil.GFun ({svar=v; _}, loc) ->
Hashtbl.replace genv v.vname (Cabs2cil.EnvVar v, loc);
VarinfoH.replace global_vars v ()
| _ -> ()
);
let global_vars = List.of_seq (VarinfoH.to_seq_keys global_vars) in
{genv; global_vars}

let parse_cabs (inv: string): (Cabs.expression, string) result =
match Timing.wrap "FrontC" Frontc.parse_standalone_exp inv with
Expand All @@ -133,8 +159,7 @@ struct
Errormsg.log "\n"; (* CIL prints garbage without \n before *)
Error e

let parse_cil {global_vars} ?(check=true) ~(fundec: Cil.fundec) ~loc (inv_cabs: Cabs.expression): (Cil.exp, string) result =
let genv = Cabs2cil.genvironment in
let parse_cil {genv; global_vars} ?(check=true) ~(fundec: Cil.fundec) ~loc (inv_cabs: Cabs.expression): (Cil.exp, string) result =
let env = Hashtbl.copy genv in
List.iter (fun (v: Cil.varinfo) ->
Hashtbl.replace env v.vname (Cabs2cil.EnvVar v, v.vdecl)
Expand Down