From 6186df15007964eb4f7f9b4feb01f9bad2e38afb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Mar 2023 12:31:02 +0200 Subject: [PATCH 1/3] Fix incremental invariant parser for server mode --- src/witness/witnessUtil.ml | 33 ++++++++++++++++++++++++++++++--- 1 file changed, 30 insertions(+), 3 deletions(-) diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index 7521ce7a73..2f5ecbdcb2 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -114,17 +114,45 @@ end module InvariantParser = struct type t = { + genv: (string, Cabs2cil.envdata * Cil.location) Hashtbl.t; global_vars: Cil.varinfo list; } let create (file: Cil.file): t = + (* 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 + 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) + | _ -> () + ); let global_vars = List.filter_map (function | Cil.GVar (v, _, _) + (* | Cil.GVarDecl (v, _) *) (* TODO: add declarations, but only when no definition present to avoid CIL check errors *) | Cil.GFun ({svar=v; _}, _) -> Some v | _ -> None ) file.globals in - {global_vars} + {genv; global_vars} let parse_cabs (inv: string): (Cabs.expression, string) result = match Timing.wrap "FrontC" Frontc.parse_standalone_exp inv with @@ -133,8 +161,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) From 9edf77f90ed2e12e4faba94f119a76b4094565c9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Mar 2023 12:31:55 +0200 Subject: [PATCH 2/3] Re-enable server mode eval expression checking --- src/util/server.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/util/server.ml b/src/util/server.ml index cb810b93a2..2f4e74d12c 100644 --- a/src/util/server.ml +++ b/src/util/server.ml @@ -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)" ())) @@ -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 { From 4dfe744528784c069986b676d22cde6a7340ea6e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Mar 2023 12:38:13 +0200 Subject: [PATCH 3/3] Add declarations to invariant parser CIL checking --- src/witness/witnessUtil.ml | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index 2f5ecbdcb2..54a574d60c 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -118,11 +118,14 @@ struct global_vars: Cil.varinfo list; } + module VarinfoH = Cilfacade.VarinfoH + let create (file: Cil.file): t = (* 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 @@ -142,16 +145,11 @@ struct | Cil.GVar (v, _, loc) | Cil.GVarDecl (v, loc) | Cil.GFun ({svar=v; _}, loc) -> - Hashtbl.replace genv v.vname (Cabs2cil.EnvVar v, loc) + Hashtbl.replace genv v.vname (Cabs2cil.EnvVar v, loc); + VarinfoH.replace global_vars v () | _ -> () ); - let global_vars = List.filter_map (function - | Cil.GVar (v, _, _) - (* | Cil.GVarDecl (v, _) *) (* TODO: add declarations, but only when no definition present to avoid CIL check errors *) - | Cil.GFun ({svar=v; _}, _) -> Some v - | _ -> None - ) file.globals - in + 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 =