Skip to content

Commit

Permalink
[textual][refactor] make internal transformations more visible
Browse files Browse the repository at this point in the history
Summary:
the round of transformations we perform before generating SIL is made more visible.
It will be useful for a next diff.

Reviewed By: ngorogiannis

Differential Revision:
D66537540

Privacy Context Container: L1208441

fbshipit-source-id: 5b912f6472e88a5130a31dad4b59537f2c3052bc
  • Loading branch information
davidpichardie authored and facebook-github-bot committed Dec 3, 2024
1 parent de74457 commit d790d86
Show file tree
Hide file tree
Showing 8 changed files with 100 additions and 90 deletions.
7 changes: 4 additions & 3 deletions infer/src/integration/Python.ml
Original file line number Diff line number Diff line change
Expand Up @@ -96,11 +96,12 @@ let process_file ~is_binary file =
TextualVerification.verify textual |> Result.map_error ~f
in
if Config.debug_mode then dump_textual_file ~version:1 file verified_textual ;
let* cfg, tenv, transformed_textual =
let transformed_textual, decls = TextualTransform.run Python verified_textual in
if Config.debug_mode then dump_textual_file ~version:2 file transformed_textual ;
let* cfg, tenv =
let f = Error.textual_transformation sourcefile in
TextualSil.module_to_sil verified_textual |> Result.map_error ~f
TextualSil.module_to_sil Python transformed_textual decls |> Result.map_error ~f
in
if Config.debug_mode then dump_textual_file ~version:2 file transformed_textual ;
let sil = {TextualParser.TextualFile.sourcefile; cfg; tenv} in
if Config.python_skip_db then Ok None
else (
Expand Down
7 changes: 2 additions & 5 deletions infer/src/python/unit/PyIR2TextualTest.ml
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,12 @@ let run module_ =
let textual = PyIR2Textual.mk_module module_ in
F.printf "TRANSFORMATION PyIR -> Textual@\n" ;
F.printf "%a" Textual.Module.pp textual ;
let* verified_textual =
let+ verified_textual =
TextualVerification.verify textual |> Result.map_error ~f:(fun err -> `VerificationError err)
in
F.printf "TYPE INFERENCE@\n" ;
F.printf "%a" Textual.Module.pp verified_textual ;
let+ _, _, transformed_textual =
TextualSil.module_to_sil verified_textual
|> Result.map_error ~f:(fun err -> `TransformationError err)
in
let transformed_textual, _ = TextualTransform.run Python verified_textual in
F.printf "FINAL TRANSFORMATIONS@\n" ;
F.printf "%a" Textual.Module.pp transformed_textual
in
Expand Down
18 changes: 16 additions & 2 deletions infer/src/textual/TextualParser.ml
Original file line number Diff line number Diff line change
Expand Up @@ -100,10 +100,24 @@ module TextualFile = struct
|> Result.map_error ~f:(fun err -> (sourcefile, [VerificationError err]))


let lang sourcefile module_ =
match Textual.Module.lang module_ with
| None ->
Error
( sourcefile
, [ TransformError
[ { loc= Textual.Location.Unknown
; msg= lazy "Missing or unsupported source_language attribute" } ] ] )
| Some lang ->
Ok lang


let textual_to_sil sourcefile module_ =
let open IResult.Let_syntax in
let* cfg, tenv, _ =
TextualSil.module_to_sil module_
let* lang = lang sourcefile module_ in
let module_, decls_env = TextualTransform.run lang module_ in
let* cfg, tenv =
TextualSil.module_to_sil lang module_ decls_env
|> Result.map_error ~f:(fun errors -> (sourcefile, [TransformError errors]))
in
Ok {sourcefile; cfg; tenv}
Expand Down
107 changes: 42 additions & 65 deletions infer/src/textual/TextualSil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1214,69 +1214,45 @@ end
module ModuleBridge = struct
open Module

let to_sil module_ =
match lang module_ with
| None ->
raise
(TextualTransformError
[{loc= Location.Unknown; msg= lazy "Missing or unsupported source_language attribute"}]
)
| Some lang ->
let errors, decls_env = TextualDecls.make_decls module_ in
if not (List.is_empty errors) then
L.die InternalError
"to_sil conversion should not be performed if TextualDecls verification has raised any \
errors before." ;
let module_, new_decls_were_added =
let open TextualTransform in
(* note: because && and || operators are lazy we must remove them before moving calls *)
module_ |> remove_if_terminator |> remove_effects_in_subexprs lang decls_env
in
let module_ =
let open TextualTransform in
module_ |> let_propagation |> out_of_ssa
in
let decls_env =
if new_decls_were_added then TextualDecls.make_decls module_ |> snd else decls_env
in
let all_proc_entries, types_used_as_enclosing_but_not_defined =
TextualDecls.get_proc_entries_by_enclosing_class decls_env
in
let cfgs = Cfg.create () in
let tenv = Tenv.create () in
TypeName.Set.iter
(fun name -> TypeNameBridge.to_sil lang name |> Tenv.mk_struct ~dummy:true tenv |> ignore)
types_used_as_enclosing_but_not_defined ;
List.iter module_.decls ~f:(fun decl ->
match decl with
| Global _ ->
()
| Struct strct ->
let proc_entries =
TypeName.Map.find_opt strct.name all_proc_entries |> Option.value ~default:[]
in
let source_file = Some (TextualDecls.source_file decls_env |> SourceFile.file) in
StructBridge.to_sil lang decls_env tenv proc_entries source_file strct
| Procdecl _ ->
()
| Proc pdesc ->
if not (ProcDesc.is_ready_for_to_sil_conversion pdesc) then
(* we only run SSA verification if the to_sil conversion needs
extra transformation, because some .sil files that are generated by
Java examples are not in SSA *)
SsaVerification.run pdesc ;
ProcDescBridge.to_sil lang decls_env cfgs pdesc ) ;
(* Register undefined types in tenv *)
let is_undefined_type tname =
(not (TypeName.Set.mem tname types_used_as_enclosing_but_not_defined))
&& TextualDecls.get_struct decls_env tname |> Option.is_none
in
TextualDecls.get_undefined_types decls_env
|> Seq.iter (fun tname ->
if is_undefined_type tname then
let sil_tname = TypeNameBridge.to_sil lang tname in
Tenv.mk_struct ~dummy:true tenv sil_tname |> ignore ) ;
(cfgs, tenv, module_)
let to_sil lang module_ decls_env =
let all_proc_entries, types_used_as_enclosing_but_not_defined =
TextualDecls.get_proc_entries_by_enclosing_class decls_env
in
let cfgs = Cfg.create () in
let tenv = Tenv.create () in
TypeName.Set.iter
(fun name -> TypeNameBridge.to_sil lang name |> Tenv.mk_struct ~dummy:true tenv |> ignore)
types_used_as_enclosing_but_not_defined ;
List.iter module_.decls ~f:(fun decl ->
match decl with
| Global _ ->
()
| Struct strct ->
let proc_entries =
TypeName.Map.find_opt strct.name all_proc_entries |> Option.value ~default:[]
in
let source_file = Some (TextualDecls.source_file decls_env |> SourceFile.file) in
StructBridge.to_sil lang decls_env tenv proc_entries source_file strct
| Procdecl _ ->
()
| Proc pdesc ->
if not (ProcDesc.is_ready_for_to_sil_conversion pdesc) then
(* we only run SSA verification if the to_sil conversion needs
extra transformation, because some .sil files that are generated by
Java examples are not in SSA *)
SsaVerification.run pdesc ;
ProcDescBridge.to_sil lang decls_env cfgs pdesc ) ;
(* Register undefined types in tenv *)
let is_undefined_type tname =
(not (TypeName.Set.mem tname types_used_as_enclosing_but_not_defined))
&& TextualDecls.get_struct decls_env tname |> Option.is_none
in
TextualDecls.get_undefined_types decls_env
|> Seq.iter (fun tname ->
if is_undefined_type tname then
let sil_tname = TypeNameBridge.to_sil lang tname in
Tenv.mk_struct ~dummy:true tenv sil_tname |> ignore ) ;
(cfgs, tenv)


let of_sil ~sourcefile ~lang tenv cfg =
Expand All @@ -1302,8 +1278,9 @@ end

let proc_decl_to_sil lang procdecl = ProcDeclBridge.to_sil lang procdecl

let module_to_sil module_ =
try Ok (ModuleBridge.to_sil module_) with Textual.TextualTransformError errors -> Error errors
let module_to_sil lang module_ decls_env =
try Ok (ModuleBridge.to_sil lang module_ decls_env)
with Textual.TextualTransformError errors -> Error errors


let pp_copyright fmt =
Expand Down
5 changes: 4 additions & 1 deletion infer/src/textual/TextualSil.mli
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,10 @@ val proc_decl_to_sil : Textual.Lang.t -> Textual.ProcDecl.t -> Procname.t
[@@warning "-unused-value-declaration"]

val module_to_sil :
Textual.Module.t -> (Cfg.t * Tenv.t * Textual.Module.t, Textual.transform_error list) result
Textual.Lang.t
-> Textual.Module.t
-> TextualDecls.t
-> (Cfg.t * Tenv.t, Textual.transform_error list) result
(** convert a Textual unit into Infer internal representation (cfg + tenv). During the process the
textual representation undergoes several transformations. The result is passed as the third
element of the returned tuple *)
Expand Down
17 changes: 17 additions & 0 deletions infer/src/textual/TextualTransform.ml
Original file line number Diff line number Diff line change
Expand Up @@ -883,3 +883,20 @@ let out_of_ssa module_ =
{pdesc with nodes}
in
module_map_procs ~f:transform module_


let run lang module_ =
let errors, decls_env = TextualDecls.make_decls module_ in
if not (List.is_empty errors) then
L.die InternalError
"to_sil conversion should not be performed if TextualDecls verification has raised any \
errors before." ;
let module_, new_decls_were_added =
(* note: because && and || operators are lazy we must remove them before moving calls *)
module_ |> remove_if_terminator |> remove_effects_in_subexprs lang decls_env
in
let decls_env =
if new_decls_were_added then TextualDecls.make_decls module_ |> snd else decls_env
in
let module_ = module_ |> let_propagation |> out_of_ssa in
(module_, decls_env)
14 changes: 12 additions & 2 deletions infer/src/textual/TextualTransform.mli
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ val fix_closure_app : Textual.Module.t -> Textual.Module.t

val remove_effects_in_subexprs :
Textual.Lang.t -> TextualDecls.t -> Textual.Module.t -> Textual.Module.t * bool
[@@warning "-unused-value-declaration"]
(* generates enough intermediate Let and Load instructions to make the procdesc free
of side-effect sub-expressions.
Example:
Expand All @@ -27,7 +28,16 @@ val remove_effects_in_subexprs :
*)

val remove_if_terminator : Textual.Module.t -> Textual.Module.t
[@@warning "-unused-value-declaration"]

val let_propagation : Textual.Module.t -> Textual.Module.t
val let_propagation : Textual.Module.t -> Textual.Module.t [@@warning "-unused-value-declaration"]

val out_of_ssa : Textual.Module.t -> Textual.Module.t
val out_of_ssa : Textual.Module.t -> Textual.Module.t [@@warning "-unused-value-declaration"]

val run : Textual.Lang.t -> Textual.Module.t -> Textual.Module.t * TextualDecls.t
(* run the following transformations in the given order:
1) remove_if_terminator
2) remove_effects_in_subexprs (also removes closures expressions)
3) let_propagation
4) out_of_ssa in
*)
15 changes: 3 additions & 12 deletions infer/src/textual/unit/TextualSilTest.ml
Original file line number Diff line number Diff line change
Expand Up @@ -11,23 +11,14 @@ module T = Textual
open TextualTestHelpers

let module_to_sil_exn module_ =
match TextualSil.module_to_sil module_ with
| Ok (cfg, tenv, _) ->
let module_, decls = TextualTransform.run Hack module_ in
match TextualSil.module_to_sil Hack module_ decls with
| Ok (cfg, tenv) ->
(cfg, tenv)
| Error err ->
raise (Textual.TextualTransformError err)


let%expect_test _ =
let no_lang = {|define nothing() : void { #node: ret null }|} in
let m = parse_module no_lang in
try module_to_sil_exn m |> ignore
with T.TextualTransformError errs ->
List.iter errs ~f:(Textual.pp_transform_error sourcefile F.std_formatter) ;
[%expect
{| dummy.sil, <unknown location>: transformation error: Missing or unsupported source_language attribute |}]


let%expect_test "undefined types are included in tenv" =
let source =
{|
Expand Down

0 comments on commit d790d86

Please sign in to comment.