CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

The backend name should be verifisc, since specifisc will be the name of the high-level language

Browse Source
This commit is contained in:
Denis Merigoux 2019-08-14 18:50:41 -07:00
commit 82dcdbcfbc
13 changed files with 1117 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

107
ast/ast.ml Normal file
View File

@ -0,0 +1,107 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
(**
This module describes the core backend language for describing tax specifications : Verifisc.
Programs in Verifisc only deal with boolean logic and integer arithmetic modulo 2^64. The
language is imperative, each function consisting of variable definitions and constraints that
should hold during the program execution.
This language is meant for formal analysis of the tax specification.
*)
module Variable (_ : sig end) = struct
type t = {
name: string Pos.marked;
id: int;
descr: string Pos.marked;
}
let counter : int ref = ref 0
let fresh_id () : int=
let v = !counter in
counter := !counter + 1;
v
let new_var
(name: string Pos.marked)
(descr: string Pos.marked)
: t =
{
name; id = fresh_id (); descr;
}
let compare (var1 :t) (var2 : t) =
compare var1.id var2.id
end
module BoolVariable = Variable ()
module BoolVariableMap = Map.Make(BoolVariable)
module IntVariable = Variable ()
module IntVariableMap = Map.Make(IntVariable)
module FunctionVariable = Variable ()
module FunctionVariableMap = Map.Make(FunctionVariable)
type typ =
| Int
| Bool
type comparison_op = Lt | Lte | Gt | Gte | Neq | Eq
type logical_binop = And | Or
type arithmetic_binop = Add | Sub | Mul | Div
type logical_expression =
| Comparison of comparison_op Pos.marked * arithmetic_expression Pos.marked * arithmetic_expression Pos.marked
| LogicalBinop of logical_binop Pos.marked * logical_expression Pos.marked * logical_expression Pos.marked
| LogicalNot of logical_expression Pos.marked
| BoolLiteral of bool
| BoolVar of BoolVariable.t
and arithmetic_expression =
| ArithmeticBinop of arithmetic_binop Pos.marked * arithmetic_expression Pos.marked * arithmetic_expression Pos.marked
| ArithmeticMinus of arithmetic_expression Pos.marked
| Conditional of logical_expression Pos.marked * arithmetic_expression Pos.marked * arithmetic_expression Pos.marked
| IntLiteral of Int64.t
| IntVar of IntVariable.t
type command =
| BoolDef of BoolVariable.t * logical_expression Pos.marked
| IntDef of IntVariable.t * arithmetic_expression Pos.marked
| Constraint of logical_expression Pos.marked
type variables = IntVariable.t list * BoolVariable.t list
type func = {
body: command list;
inputs: variables;
outputs: variables;
}
type idmap_var =
| IDBoolVar of BoolVariable.t
| IDIntVar of IntVariable.t
type idmap = idmap_var list Pos.VarNameToID.t
type program = {
program_functions: func FunctionVariableMap.t;
program_mult_factor: int;
program_idmap: idmap
}

117
ast/format_ast.ml Normal file
View File

@ -0,0 +1,117 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
open Ast
let format_typ (t: typ) : string = match t with
| Int -> "integer"
| Bool -> "boolean"
let format_comparison_op (op : comparison_op) : string = match op with
| Lt -> "<"
| Lte -> "<="
| Gt -> ">"
| Gte -> ">="
| Neq -> "!="
| Eq -> "=="
let format_logical_binop (op: logical_binop) : string = match op with
| And -> "&&"
| Or -> "||"
let format_arithmetic_binop (op: arithmetic_binop) : string = match op with
| Add -> "+"
| Sub -> "-"
| Mul -> "*"
| Div -> "/"
let format_bool_var (b: BoolVariable.t) : string =
Printf.sprintf "%s_%d"
(Pos.unmark b.BoolVariable.name)
b.BoolVariable.id
let format_int_var (b: IntVariable.t) : string =
Printf.sprintf "%s_%d"
(Pos.unmark b.IntVariable.name)
b.IntVariable.id
let format_function_var (b: FunctionVariable.t) : string =
Printf.sprintf "%s_%d"
(Pos.unmark b.FunctionVariable.name)
b.FunctionVariable.id
let rec format_logical_expression (e: logical_expression) : string = match e with
| Comparison (op, e1, e2) ->
Printf.sprintf "(%s %s %s)"
(format_arithmetic_expression (Pos.unmark e1))
(format_comparison_op (Pos.unmark op))
(format_arithmetic_expression (Pos.unmark e2))
| LogicalBinop (op, e1, e2) ->
Printf.sprintf "(%s %s %s)"
(format_logical_expression (Pos.unmark e1))
(format_logical_binop (Pos.unmark op))
(format_logical_expression (Pos.unmark e2))
| LogicalNot e1 ->
Printf.sprintf "!%s" (format_logical_expression (Pos.unmark e1))
| BoolLiteral b -> string_of_bool b
| BoolVar v -> format_bool_var v
and format_arithmetic_expression (e: arithmetic_expression) : string = match e with
| ArithmeticBinop (op, e1, e2) ->
Printf.sprintf "(%s %s %s)"
(format_arithmetic_expression (Pos.unmark e1))
(format_arithmetic_binop (Pos.unmark op))
(format_arithmetic_expression (Pos.unmark e2))
| Conditional (e1, e2, e3) ->
Printf.sprintf "(if %s then %s else %s)"
(format_logical_expression (Pos.unmark e1))
(format_arithmetic_expression (Pos.unmark e2))
(format_arithmetic_expression (Pos.unmark e3))
| ArithmeticMinus e1 ->
Printf.sprintf "- %s" (format_arithmetic_expression (Pos.unmark e1))
| IntLiteral i -> Int64.to_string i
| IntVar v -> format_int_var v
let format_command (c: command) : string = match c with
| BoolDef (bv, e) ->
Printf.sprintf "%s : bool := %s"
(format_bool_var bv)
(format_logical_expression (Pos.unmark e))
| IntDef (iv, e) ->
Printf.sprintf "%s : int := %s"
(format_int_var iv)
(format_arithmetic_expression (Pos.unmark e))
| Constraint e ->
Printf.sprintf "assert(%s)"
(format_logical_expression (Pos.unmark e))
let format_func (f: func) : string =
Printf.sprintf "function(%s, %s) -> %s, %s\n%s"
(String.concat "," (List.map (fun v -> format_int_var v) (fst f.inputs)))
(String.concat "," (List.map (fun v -> format_bool_var v) (snd f.inputs)))
(String.concat "," (List.map (fun v -> format_int_var v) (fst f.outputs)))
(String.concat "," (List.map (fun v -> format_bool_var v) (snd f.outputs)))
(String.concat "\n" (List.map (fun c -> format_command c) f.body))
let format_program (p: program) : string =
FunctionVariableMap.fold (fun fvar f acc ->
acc ^ begin
Printf.sprintf "%s ::= %s\n\n"
(format_function_var fvar)
(format_func f)
end
) p.program_functions ""

110
ast/typechecker.ml Normal file
View File

@ -0,0 +1,110 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
open Ast
type ctx = {
ctx_defined_variables : variables;
}
let rec typecheck_logical_expression
(e: logical_expression Pos.marked)
(ctx: ctx)
: unit = match Pos.unmark e with
| Comparison (_, e1, e2) ->
typecheck_arithmetic_expression e1 ctx;
typecheck_arithmetic_expression e2 ctx
| LogicalBinop (_, e1, e2) ->
typecheck_logical_expression e1 ctx;
typecheck_logical_expression e2 ctx
| LogicalNot e1 ->
typecheck_logical_expression e1 ctx;
| BoolLiteral _ -> ()
| BoolVar var ->
if not (List.mem var (snd ctx.ctx_defined_variables)) then
raise
(Errors.VerifiscTypeError
(Printf.sprintf "boolean variable %s used %s is undefined"
(Pos.unmark var.BoolVariable.name)
(Pos.format_position (Pos.get_position e))
))
and typecheck_arithmetic_expression
(e: arithmetic_expression Pos.marked)
(ctx: ctx)
: unit = match Pos.unmark e with
| ArithmeticBinop (_, e1, e2) ->
typecheck_arithmetic_expression e1 ctx;
typecheck_arithmetic_expression e2 ctx
| ArithmeticMinus e1 ->
typecheck_arithmetic_expression e1 ctx
| Conditional (e1, e2, e3) ->
typecheck_logical_expression e1 ctx;
typecheck_arithmetic_expression e2 ctx;
typecheck_arithmetic_expression e3 ctx
| IntLiteral _ -> ()
| IntVar var ->
if not (List.mem var (fst ctx.ctx_defined_variables)) then
raise
(Errors.VerifiscTypeError
(Printf.sprintf "integer variable %s used %s is undefined"
(Pos.unmark var.IntVariable.name)
(Pos.format_position (Pos.get_position e))
))
let typecheck (program : program) : unit =
FunctionVariableMap.iter (fun _ func ->
let ctx = {
ctx_defined_variables = func.inputs;
} in
let ctx = List.fold_left (fun ctx cmd ->
match cmd with
| BoolDef (var, e) ->
typecheck_logical_expression e ctx;
{
ctx_defined_variables =
(fst ctx.ctx_defined_variables,
var::(snd ctx.ctx_defined_variables)
)}
| IntDef (var, e) ->
typecheck_arithmetic_expression e ctx;
{
ctx_defined_variables =
(var::(fst ctx.ctx_defined_variables),
snd ctx.ctx_defined_variables)
}
| Constraint e ->
typecheck_logical_expression e ctx;
ctx
) ctx func.body in
List.iter (fun output_var ->
if not (List.mem output_var (fst ctx.ctx_defined_variables)) then
raise
(Errors.VerifiscTypeError
(Printf.sprintf "integer output variable %s is undefined"
(Pos.unmark output_var.IntVariable.name)
))
) (fst func.outputs);
List.iter (fun output_var ->
if not (List.mem output_var (snd ctx.ctx_defined_variables)) then
raise
(Errors.VerifiscTypeError
(Printf.sprintf "boolean output variable %s is undefined"
(Pos.unmark output_var.BoolVariable.name)
))
) (snd func.outputs)
) program.program_functions

5
dune Normal file
View File

@ -0,0 +1,5 @@
(include_subdirs unqualified)
(library
(public_name verifisc)
)

20
errors.ml Normal file
View File

@ -0,0 +1,20 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
exception UnsupportedByVerifisc of string
exception VerifiscTypeError of string

107
ir/ast_to_ir.ml Normal file
View File

@ -0,0 +1,107 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
let rec translate_arithmetic_expression
(e: Ast.arithmetic_expression Pos.marked)
: Ir.arithmetic_expression Pos.marked * Ir.command list =
match Pos.unmark e with
| Ast.ArithmeticBinop (op, e1, e2) ->
let new_e1, cmds1 = wrap_int_expr e1 in
let new_e2, cmds2 = wrap_int_expr e2 in
Pos.same_pos_as (Ir.ArithmeticBinop (op, new_e1, new_e2)) e, cmds2@cmds1
| Ast.ArithmeticMinus e1 ->
let new_e1, cmds1 = wrap_int_expr e1 in
Pos.same_pos_as (Ir.ArithmeticMinus new_e1) e, cmds1
| Ast.Conditional (e1, e2, e3) ->
let new_e1, cmds1 = wrap_bool_expr e1 in
let new_e2, cmds2 = wrap_int_expr e2 in
let new_e3, cmds3 = wrap_int_expr e3 in
Pos.same_pos_as (Ir.Conditional (new_e1, new_e2, new_e3)) e, cmds3@cmds2@cmds1
| _ ->
let new_e, cmds = wrap_int_expr e in
Pos.same_pos_as (Ir.IntLiteral new_e) e, cmds
and wrap_int_expr (e: Ast.arithmetic_expression Pos.marked) :
Ir.int_literal Pos.marked * Ir.command list =
match Pos.unmark e with
| Ast.IntLiteral i -> Pos.same_pos_as (Ir.Int i) e, []
| Ast.IntVar v -> Pos.same_pos_as (Ir.IntVar v) e, []
| _ ->
let new_e, cmds = translate_arithmetic_expression e in
let int_var = Ast.IntVariable.new_var (Pos.same_pos_as "vi" e) (Pos.same_pos_as "" e) in
(Pos.same_pos_as (Ir.IntVar int_var) e, (Ir.IntDef (int_var, new_e))::cmds)
and translate_logical_expression
(e: Ast.logical_expression Pos.marked)
: Ir.logical_expression Pos.marked * Ir.command list =
match Pos.unmark e with
| Ast.LogicalBinop (op, e1, e2) ->
let new_e1, cmds1 = wrap_bool_expr e1 in
let new_e2, cmds2 = wrap_bool_expr e2 in
Pos.same_pos_as (Ir.LogicalBinop (op, new_e1, new_e2)) e, cmds2@cmds1
| Ast.LogicalNot e1 ->
let new_e1, cmds1 = wrap_bool_expr e1 in
Pos.same_pos_as (Ir.LogicalNot new_e1) e, cmds1
| Ast.Comparison (op, e1, e2) ->
let new_e1, cmds1 = wrap_int_expr e1 in
let new_e2, cmds2 = wrap_int_expr e2 in
Pos.same_pos_as (Ir.Comparison (op, new_e1, new_e2)) e, cmds2@cmds1
| _ ->
let new_e, cmds = wrap_bool_expr e in
Pos.same_pos_as (Ir.BoolLiteral new_e) e, cmds
and wrap_bool_expr (e: Ast.logical_expression Pos.marked) :
Ir.bool_literal Pos.marked * Ir.command list =
match Pos.unmark e with
| Ast.BoolLiteral i -> Pos.same_pos_as (Ir.Bool i) e, []
| Ast.BoolVar v -> Pos.same_pos_as (Ir.BoolVar v) e, []
| _ ->
let new_e, cmds = translate_logical_expression e in
let bool_var = Ast.BoolVariable.new_var (Pos.same_pos_as "vb" e) (Pos.same_pos_as "" e) in
(Pos.same_pos_as (Ir.BoolVar bool_var) e, (Ir.BoolDef (bool_var, new_e))::cmds)
let translate_body (body: Ast.command list) : Ir.command list =
let new_body = List.fold_left (fun new_body cmd ->
match cmd with
| Ast.BoolDef (bool_var, e) ->
let new_e, new_cmds = translate_logical_expression e in
(Ir.BoolDef (bool_var, new_e))::new_cmds@new_body
| Ast.IntDef (int_var, e) ->
let new_e, new_cmds = translate_arithmetic_expression e in
(Ir.IntDef (int_var, new_e))::new_cmds@new_body
| Ast.Constraint e ->
let new_e, new_cmds = translate_logical_expression e in
(Ir.Constraint new_e)::new_cmds@new_body
) [] body
in
List.rev new_body
let translate_program (p: Ast.program) : Ir.program =
{
Ir.program_idmap = p.Ast.program_idmap;
Ir.program_mult_factor = p.Ast.program_mult_factor;
Ir.program_functions = Ast.FunctionVariableMap.map (fun func ->
{
Ir.inputs = func.Ast.inputs;
Ir.outputs = func.Ast.outputs;
Ir.body = translate_body func.Ast.body
}
) p.Ast.program_functions
}

88
ir/format_ir.ml Normal file
View File

@ -0,0 +1,88 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
open Ir
let format_int_literal (v: int_literal) : string =
match v with
| Int i -> Int64.to_string i
| IntVar var -> Format_ast.format_int_var var
let format_bool_literal (v: bool_literal) : string =
match v with
| Bool b -> string_of_bool b
| BoolVar var -> Format_ast.format_bool_var var
let format_logical_expression (e: logical_expression) : string = match e with
| Comparison (op, v1, v2) ->
Printf.sprintf "%s %s %s"
(format_int_literal (Pos.unmark v1))
(Format_ast.format_comparison_op (Pos.unmark op))
(format_int_literal (Pos.unmark v2))
| LogicalBinop (op, v1, v2) ->
Printf.sprintf "%s %s %s"
(format_bool_literal (Pos.unmark v1))
(Format_ast.format_logical_binop (Pos.unmark op))
(format_bool_literal (Pos.unmark v2))
| LogicalNot v1 ->
Printf.sprintf "!%s" (format_bool_literal (Pos.unmark v1))
| BoolLiteral b -> format_bool_literal (Pos.unmark b)
let format_arithmetic_expression (e: arithmetic_expression) : string = match e with
| ArithmeticBinop (op, v1, v2) ->
Printf.sprintf "%s %s %s"
(format_int_literal (Pos.unmark v1))
(Format_ast.format_arithmetic_binop (Pos.unmark op))
(format_int_literal (Pos.unmark v2))
| Conditional (v1, v2, v3) ->
Printf.sprintf "if %s then %s else %s"
(format_bool_literal (Pos.unmark v1))
(format_int_literal (Pos.unmark v2))
(format_int_literal (Pos.unmark v3))
| ArithmeticMinus v1 ->
Printf.sprintf "- %s" (format_int_literal (Pos.unmark v1))
| IntLiteral v -> format_int_literal (Pos.unmark v)
let format_command (c: command) : string = match c with
| BoolDef (bv, e) ->
Printf.sprintf "%s : bool := %s"
(Format_ast.format_bool_var bv)
(format_logical_expression (Pos.unmark e))
| IntDef (iv, e) ->
Printf.sprintf "%s : int := %s"
(Format_ast.format_int_var iv)
(format_arithmetic_expression (Pos.unmark e))
| Constraint e ->
Printf.sprintf "assert(%s)"
(format_logical_expression (Pos.unmark e))
let format_func (f: func) : string =
Printf.sprintf "function(%s, %s) -> %s, %s\n%s"
(String.concat "," (List.map (fun v -> Format_ast.format_bool_var v) (snd f.inputs)))
(String.concat "," (List.map (fun v -> Format_ast.format_int_var v) (fst f.inputs)))
(String.concat "," (List.map (fun v -> Format_ast.format_int_var v) (fst f.outputs)))
(String.concat "," (List.map (fun v -> Format_ast.format_bool_var v) (snd f.outputs)))
(String.concat "\n" (List.map (fun c -> format_command c) f.body))
let format_program (p: program) : string =
Ast.FunctionVariableMap.fold (fun fvar f acc ->
acc ^ begin
Printf.sprintf "%s ::= %s\n\n"
(Format_ast.format_function_var fvar)
(format_func f)
end
) p.program_functions ""

62
ir/ir.ml Normal file
View File

@ -0,0 +1,62 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
type bool_literal =
| Bool of bool
| BoolVar of Ast.BoolVariable.t
type int_literal =
| Int of Int64.t
| IntVar of Ast.IntVariable.t
type logical_expression =
| Comparison of Ast.comparison_op Pos.marked * int_literal Pos.marked * int_literal Pos.marked
| LogicalBinop of Ast.logical_binop Pos.marked * bool_literal Pos.marked * bool_literal Pos.marked
| LogicalNot of bool_literal Pos.marked
| BoolLiteral of bool_literal Pos.marked
type arithmetic_expression =
| ArithmeticBinop of Ast.arithmetic_binop Pos.marked * int_literal Pos.marked * int_literal Pos.marked
| ArithmeticMinus of int_literal Pos.marked
| Conditional of bool_literal Pos.marked * int_literal Pos.marked * int_literal Pos.marked
| IntLiteral of int_literal Pos.marked
type command =
| BoolDef of Ast.BoolVariable.t * logical_expression Pos.marked
| IntDef of Ast.IntVariable.t * arithmetic_expression Pos.marked
| Constraint of logical_expression Pos.marked
type func = {
body: command list;
inputs: Ast.variables;
outputs: Ast.variables;
}
type program = {
program_functions: func Ast.FunctionVariableMap.t;
program_mult_factor: int;
program_idmap: Ast.idmap
}
let nb_commands (p: program) : int =
Ast.FunctionVariableMap.fold
(fun _ func acc ->
acc + List.length func.body
) p.program_functions 0

122
optimization/dead_code_elimination.ml Normal file
View File

@ -0,0 +1,122 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
open Ir
type data = {
used_bool_vars : unit Ast.BoolVariableMap.t;
used_int_vars: unit Ast.IntVariableMap.t;
}
let empty_data (func: func) = {
used_bool_vars = List.fold_left (fun acc var ->
Ast.BoolVariableMap.add var () acc
) Ast.BoolVariableMap.empty (snd func.outputs);
used_int_vars = List.fold_left (fun acc var ->
Ast.IntVariableMap.add var () acc
) Ast.IntVariableMap.empty (fst func.outputs);
}
let add_bool_use (var: Ast.BoolVariable.t) (data: data) : data =
{ data with
used_bool_vars = Ast.BoolVariableMap.add var () data.used_bool_vars
}
let process_bool_value (v : bool_literal Pos.marked) (data: data) : data =
match Pos.unmark v with
| Bool _ -> data
| BoolVar v -> add_bool_use v data
let add_int_use (var: Ast.IntVariable.t) (data: data) : data =
{ data with
used_int_vars = Ast.IntVariableMap.add var () data.used_int_vars
}
let process_int_value (v : int_literal Pos.marked) (data: data) : data =
match Pos.unmark v with
| Int _ -> data
| IntVar v -> add_int_use v data
let process_bool_expr (e: logical_expression Pos.marked) (data: data) : data =
match Pos.unmark e with
| Comparison (_, v1, v2) ->
let data = process_int_value v1 data in
let data = process_int_value v2 data in
data
| LogicalBinop (_, v1, v2) ->
let data = process_bool_value v1 data in
let data = process_bool_value v2 data in
data
| LogicalNot v1 ->
let data = process_bool_value v1 data in
data
| BoolLiteral v -> process_bool_value v data
let process_int_expr (e: arithmetic_expression Pos.marked) (data: data) : data =
match Pos.unmark e with
| ArithmeticBinop (_, v1, v2) ->
let data = process_int_value v1 data in
let data = process_int_value v2 data in
data
| ArithmeticMinus v1 ->
let data = process_int_value v1 data in
data
| Conditional (v1, v2, v3) ->
let data = process_bool_value v1 data in
let data = process_int_value v2 data in
let data = process_int_value v3 data in
data
| IntLiteral v -> process_int_value v data
let process_command (c: command) (data: data)
: bool * data = match c with
| BoolDef (var, e) ->
let is_necessary = Ast.BoolVariableMap.mem var data.used_bool_vars in
let data =
if is_necessary then
process_bool_expr e data
else data
in
(is_necessary, data)
| IntDef (var, e) ->
let is_necessary = Ast.IntVariableMap.mem var data.used_int_vars in
let data =
if is_necessary then
process_int_expr e data
else data
in
(is_necessary, data)
| Constraint e ->
(true, process_bool_expr e data)
let optimize (p: program) : program =
{ p with
program_functions = Ast.FunctionVariableMap.map (fun func ->
{ func with
body =
let data = empty_data func in
let new_body, _ = List.fold_right (fun cmd (new_body, data) ->
let is_necessary, data = process_command cmd data in
(if is_necessary then cmd::new_body else new_body), data
) func.body ([], data)
in
new_body
}
) p.program_functions
}

203
optimization/global_value_numbering.ml Normal file
View File

@ -0,0 +1,203 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
open Ir
module ValueNumber = struct
type t = int
let counter = ref 0
let fresh () =
let out = !counter in
counter := out + 1;
out
let compare = compare
end
module ValueNumberMap = Map.Make(ValueNumber)
module BooleanNumberExp = struct
type t =
| Comparison of Ast.comparison_op * ValueNumber.t * ValueNumber.t
| LogicalBinop of Ast.logical_binop * ValueNumber.t * ValueNumber.t
| LogicalNot of ValueNumber.t
| BoolLiteral of bool_literal
let compare = compare
end
module BooleanNumberExpMap = Map.Make(BooleanNumberExp)
module ArithmeticNumberExp = struct
type t =
| ArithmeticBinop of Ast.arithmetic_binop * ValueNumber.t * ValueNumber.t
| ArithmeticMinus of ValueNumber.t
| Conditional of ValueNumber.t * ValueNumber.t * ValueNumber.t
| IntLiteral of int_literal
let compare = compare
end
module ArithmeticNumberExpMap = Map.Make(ArithmeticNumberExp)
type data = {
int_numbering : ValueNumber.t ArithmeticNumberExpMap.t;
int_definitions : int_literal Pos.marked ValueNumberMap.t;
bool_numbering : ValueNumber.t BooleanNumberExpMap.t;
bool_definitions : bool_literal Pos.marked ValueNumberMap.t;
}
let empty_data = {
int_numbering = ArithmeticNumberExpMap.empty;
int_definitions = ValueNumberMap.empty;
bool_numbering = BooleanNumberExpMap.empty;
bool_definitions = ValueNumberMap.empty;
}
let update_data_bool (expn : BooleanNumberExp.t) (data : data) : ValueNumber.t * data =
begin match BooleanNumberExpMap.find_opt expn data.bool_numbering with
| Some vn -> vn, data
| None ->
let vn = ValueNumber.fresh () in
(vn, {data with bool_numbering = BooleanNumberExpMap.add expn vn data.bool_numbering})
end
let get_bool_literal (v: bool_literal Pos.marked) (data: data) : ValueNumber.t * data =
update_data_bool (BoolLiteral (Pos.unmark v)) data
let update_data_int (expn : ArithmeticNumberExp.t) (data : data) : ValueNumber.t * data =
begin match ArithmeticNumberExpMap.find_opt expn data.int_numbering with
| Some vn -> vn, data
| None ->
let vn = ValueNumber.fresh () in
(vn, {data with int_numbering = ArithmeticNumberExpMap.add expn vn data.int_numbering})
end
let get_int_literal (v: int_literal Pos.marked) (data: data) : ValueNumber.t * data =
update_data_int (IntLiteral (Pos.unmark v)) data
let logical_expr_to_value_number
(e: logical_expression Pos.marked)
(data : data)
: ValueNumber.t * data =
match Pos.unmark e with
| Comparison (op, v1, v2) ->
let nv1, data = get_int_literal v1 data in
let nv2, data = get_int_literal v2 data in
let expn = BooleanNumberExp.Comparison (Pos.unmark op, nv1, nv2) in
update_data_bool expn data
| LogicalBinop (op, v1, v2) ->
let nv1, data = get_bool_literal v1 data in
let nv2, data = get_bool_literal v2 data in
let expn = BooleanNumberExp.LogicalBinop (Pos.unmark op, nv1, nv2) in
update_data_bool expn data
| LogicalNot v1 ->
let nv1, data = get_bool_literal v1 data in
let expn = BooleanNumberExp.LogicalNot nv1 in
update_data_bool expn data
| BoolLiteral v -> get_bool_literal v data
let arithmetic_expr_to_value_number
(e: arithmetic_expression Pos.marked)
(data : data)
: ValueNumber.t * data = match Pos.unmark e with
| ArithmeticBinop (op, v1, v2) ->
let nv1, data = get_int_literal v1 data in
let nv2, data = get_int_literal v2 data in
let expn = ArithmeticNumberExp.ArithmeticBinop (Pos.unmark op, nv1, nv2) in
update_data_int expn data
| ArithmeticMinus v1 ->
let nv1, data = get_int_literal v1 data in
let expn = ArithmeticNumberExp.ArithmeticMinus nv1 in
update_data_int expn data
| Conditional (v1, v2, v3) ->
let nv1, data = get_bool_literal v1 data in
let nv2, data = get_int_literal v2 data in
let nv3, data = get_int_literal v3 data in
let expn = ArithmeticNumberExp.Conditional (nv1, nv2, nv3) in
update_data_int expn data
| IntLiteral v -> get_int_literal v data
let bool_definition_to_expression (def: bool_literal Pos.marked) : logical_expression Pos.marked =
Pos.same_pos_as (BoolLiteral def) def
let int_definition_to_expression (def: int_literal Pos.marked) : arithmetic_expression Pos.marked =
Pos.same_pos_as (IntLiteral def) def
let gvn_bool_exp (e: logical_expression Pos.marked) (data: data)
: logical_expression Pos.marked * data * ValueNumber.t =
let expn, data = logical_expr_to_value_number e data in
match Pos.unmark e with
| BoolLiteral _ -> (e, data, expn)
| _ -> begin match ValueNumberMap.find_opt expn data.bool_definitions with
| Some def -> (bool_definition_to_expression def, data, expn)
| None -> e, data, expn
end
let gvn_int_exp (e: arithmetic_expression Pos.marked) (data: data)
: arithmetic_expression Pos.marked * data * ValueNumber.t =
let expn, data = arithmetic_expr_to_value_number e data in
match Pos.unmark e with
| IntLiteral _ -> (e, data, expn)
| _ -> begin match ValueNumberMap.find_opt expn data.int_definitions with
| Some def -> (int_definition_to_expression def, data, expn)
| None -> e, data, expn
end
let gvn_command
(c: command)
(data: data)
: (command * data) = match c with
| BoolDef (var, e) ->
let new_e,data, expn = gvn_bool_exp e data in
let data =
{ data with
bool_definitions = ValueNumberMap.update expn (fun def -> match def with
| None -> Some (BoolVar var, Pos.get_position e)
| Some _ -> def (* we always keep the old definition ! *)
) data.bool_definitions
} in
BoolDef (var, new_e), data
| IntDef (var, e) ->
let new_e, data, expn = gvn_int_exp e data in
let data =
{ data with
int_definitions = ValueNumberMap.update expn (fun def -> match def with
| None -> Some (IntVar var, Pos.get_position e)
| Some _ -> def (* we always keep the old definition ! *)
) data.int_definitions
} in
IntDef (var, new_e), data
| Constraint e ->
let new_e,data, _ = gvn_bool_exp e data in
Constraint new_e, data
let optimize (p: program) : program =
{ p with
program_functions = Ast.FunctionVariableMap.map (fun func ->
{ func with
body =
let data = empty_data in
let new_body, _ = List.fold_left (fun (new_body, data) cmd ->
let new_cmd, data = gvn_command cmd data in
new_cmd::new_body, data
) ([], data) func.body
in
List.rev new_body
}
) p.program_functions
}

38
optimization/optimization.ml Normal file
View File

@ -0,0 +1,38 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
open Ir
let optimize
(program: program)
: program =
let program = ref program in
let nb_removed = ref max_int in
while !nb_removed > 0 do
let new_program = Global_value_numbering.optimize !program in
let new_program = Partial_evaluation.optimize new_program in
let new_program = Dead_code_elimination.optimize new_program in
let new_nb_removed =
nb_commands !program -
nb_commands new_program
in
program := new_program;
nb_removed := new_nb_removed;
done;
!program

76
optimization/partial_evaluation.ml Normal file
View File

@ -0,0 +1,76 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
open Ir
type data = {
known_bool_vars : bool_literal Ast.BoolVariableMap.t;
known_int_vars : int_literal Ast.IntVariableMap.t;
}
let empty_data = {
known_bool_vars = Ast.BoolVariableMap.empty;
known_int_vars = Ast.IntVariableMap.empty;
}
let partially_evaluate_logical_expr (e: logical_expression Pos.marked) (_ : data)
: logical_expression Pos.marked = e
let partially_evaluate_arithmetic_expr (e: arithmetic_expression Pos.marked) (_ : data)
: arithmetic_expression Pos.marked = e
let partially_evaluate_command
(c: command)
(data: data)
: (command * data) = match c with
| BoolDef (var, e) ->
let new_e = partially_evaluate_logical_expr e data in
let data =
{ data with
known_bool_vars = match Pos.unmark new_e with
| BoolLiteral b -> Ast.BoolVariableMap.add var (Pos.unmark b) data.known_bool_vars
| _ -> data.known_bool_vars
} in
BoolDef (var, new_e), data
| IntDef (var, e) ->
let new_e = partially_evaluate_arithmetic_expr e data in
let data =
{ data with
known_int_vars = match Pos.unmark new_e with
| IntLiteral i -> Ast.IntVariableMap.add var (Pos.unmark i) data.known_int_vars
| _ -> data.known_int_vars
} in
IntDef (var, new_e), data
| Constraint e ->
let new_e = partially_evaluate_logical_expr e data in
Constraint new_e, data
let optimize (p: program) : program =
{ p with
program_functions = Ast.FunctionVariableMap.map (fun func ->
{ func with
body =
let data = empty_data in
let new_body, _ = List.fold_left (fun (new_body, data) cmd ->
let new_cmd, data = partially_evaluate_command cmd data in
new_cmd::new_body, data
) ([], data) func.body
in
List.rev new_body
}
) p.program_functions
}

62
pos.ml Normal file
View File

@ -0,0 +1,62 @@
(*
Copyright (C) 2019 Inria, contributor: Denis Merigoux <denis.merigoux@inria.fr>
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
(** {1 Source code position} *)
(** A position in the source code is a file, as well as begin and end location of the form col:line *)
type position = {
pos_filename: string;
pos_loc: (Lexing.position * Lexing.position)
}
let format_position (pos: position) : string =
let (s, e) = pos.pos_loc in
Printf.sprintf "in file %s, from %d:%d to %d:%d"
pos.pos_filename
s.Lexing.pos_lnum (s.Lexing.pos_cnum - s.Lexing.pos_bol + 1)
e.Lexing.pos_lnum (e.Lexing.pos_cnum - e.Lexing.pos_bol + 1)
(** Everything related to the source code should keep its position stored, to improve error messages *)
type 'a marked = ('a * position)
(** Placeholder position *)
let no_pos : position =
let zero_pos =
{ Lexing.pos_fname = ""; Lexing.pos_lnum = 0; Lexing.pos_cnum = 0; Lexing.pos_bol = 0 }
in
{
pos_filename = "unknown position";
pos_loc = (zero_pos, zero_pos)
}
let unmark ((x, _) : 'a marked) : 'a = x
let get_position ((_,x) : 'a marked) : position = x
let map_under_mark (f: 'a -> 'b) ((x, y) :'a marked) : 'b marked =
(f x, y)
let same_pos_as (x: 'a) ((_, y) : 'b marked) : 'a marked =
(x,y)
let unmark_option (x: 'a marked option) : 'a option = match x with
| Some x -> Some (unmark x)
| None -> None
module VarNameToID = Map.Make(String)