elvis/lci
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Merge with cfg

Browse Source
This commit is contained in:
elvis
2025-01-27 16:32:22 +01:00
parent ad0320875c 2fbbf4e4d1
commit 61ea821d47
63 changed files with 5823 additions and 777 deletions
Download Patch File Download Diff File Expand all files Collapse all files

209
lib/analysis/Cfg.ml Normal file
View File

@ -0,0 +1,209 @@
module type PrintableType = sig
type t
val pp : out_channel -> t -> unit
val pp_list : out_channel -> t list -> unit
end
let globalIdNode = ref 0;
module Node = struct
type t = {
id: int;
}
let compare a b = compare a.id b.id
let create () =
globalIdNode := !globalIdNode + 1;
{id = !globalIdNode;}
end
module NodeMap = struct
include Map.Make(Node)
(* adds the input to the tail of the list for the associated node *)
let add_to_list_last x data m =
let add = function None -> Some [data]
| Some l -> Some (l @ [data]) in
update x add m
end
module NodeSet = Set.Make(Node)
type 'a cfginternal = {
empty: bool;
nodes: NodeSet.t;
edges: (Node.t * (Node.t option)) NodeMap.t;
reverse_edges: (Node.t list) NodeMap.t;
input_val: int option;
input_output_var: (string * string) option;
initial: Node.t option;
terminal: Node.t option;
content: 'a list NodeMap.t;
}
module type C = sig
type elt
type t = elt cfginternal
val empty : t
val merge : t -> t -> Node.t -> Node.t -> t
val concat : t -> t -> t
val add_to_last_node : elt -> t -> t
val pp : out_channel -> t -> unit
end
module Make (M: PrintableType) = struct
type elt = M.t
type t = elt cfginternal
let empty : t =
{ empty = true;
nodes = NodeSet.empty;
edges = NodeMap.empty;
reverse_edges = NodeMap.empty;
input_val = None;
input_output_var = None;
initial = None;
terminal = None;
content = NodeMap.empty }
let merge (cfg1: t) (cfg2: t) (entry_node: Node.t) (exit_node: Node.t) : t =
match (cfg1.empty, cfg2.empty) with
true, _ -> cfg2
| _, true -> cfg1
| false, false ->
let cfg1_initial = Option.get cfg1.initial in
let cfg2_initial = Option.get cfg2.initial in
let cfg1_terminal = Option.get cfg1.terminal in
let cfg2_terminal = Option.get cfg2.terminal in
{ empty = false;
nodes = NodeSet.union cfg1.nodes cfg2.nodes |>
NodeSet.add entry_node |>
NodeSet.add exit_node;
edges = NodeMap.union
(fun _ -> failwith "Failed merging edges of cfg.")
cfg1.edges cfg2.edges |>
NodeMap.add entry_node (cfg1_initial, Some cfg2_initial) |>
NodeMap.add cfg1_terminal (exit_node, None) |>
NodeMap.add cfg2_terminal (exit_node, None);
reverse_edges = NodeMap.union
(fun _ -> failwith "Failed merging edges of cfg.")
cfg1.reverse_edges cfg2.reverse_edges |>
NodeMap.add_to_list cfg1_initial entry_node |>
NodeMap.add_to_list cfg2_initial entry_node |>
NodeMap.add_to_list exit_node cfg1_terminal |>
NodeMap.add_to_list exit_node cfg2_terminal;
input_val = cfg1.input_val;
input_output_var = cfg1.input_output_var;
initial = Some entry_node;
terminal = Some exit_node;
content = NodeMap.union
(fun _ -> failwith "Failed merging code of cfg.")
cfg1.content cfg2.content
}
let concat (cfg1: t) (cfg2: t) : t =
match (cfg1.empty, cfg2.empty) with
true, _ -> cfg2
| _, true -> cfg1
| false, false ->
let cfg1_initial = Option.get cfg1.initial in
let cfg2_initial = Option.get cfg2.initial in
let cfg1_terminal = Option.get cfg1.terminal in
let cfg2_terminal = Option.get cfg2.terminal in
{ empty = false;
nodes = NodeSet.union cfg1.nodes cfg2.nodes;
edges = NodeMap.union
(fun _ -> failwith "Failed merging edges of cfg.")
cfg1.edges cfg2.edges |>
NodeMap.add cfg1_terminal (cfg2_initial, None);
reverse_edges = NodeMap.union
(fun _ -> failwith "Failed merging edges of cfg.")
cfg1.reverse_edges cfg2.reverse_edges |>
NodeMap.add_to_list cfg2_initial cfg1_terminal;
input_val = cfg1.input_val;
input_output_var = cfg1.input_output_var;
initial = Some cfg1_initial;
terminal = Some cfg2_terminal;
content = NodeMap.union
(fun _ -> failwith "Failed merging code of cfg.")
cfg1.content cfg2.content
}
let add_to_last_node (new_content: elt) (cfg: t) : t =
if cfg.empty then
let new_node = Node.create () in
{ empty = false;
nodes = NodeSet.singleton new_node;
edges = NodeMap.empty;
reverse_edges = NodeMap.empty;
input_val = None;
input_output_var = None;
initial = Some new_node;
terminal = Some new_node;
content = NodeMap.singleton new_node [new_content]
}
else
let prevcfg_terminal = Option.get cfg.terminal in
{ cfg with
content = (NodeMap.add_to_list_last
prevcfg_terminal
new_content
cfg.content) }
let pp (ppf) (c: t) : unit =
Printf.fprintf ppf "Nodes' ids: ";
List.iter
(fun (x : Node.t) -> Printf.fprintf ppf "%d " x.id)
(NodeSet.to_list c.nodes);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Nodes' edges:\n";
List.iter
(fun ((n, (a, b)) : (Node.t * (Node.t * Node.t option))) : unit ->
match b with
None -> Printf.fprintf ppf "\t%d -> %d\n" n.id a.id
| Some b -> Printf.fprintf ppf "\t%d -> %d, %d\n" n.id a.id b.id )
(NodeMap.to_list c.edges);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Nodes' back edges:\n";
List.iter (fun ((n, xs) : (Node.t * (Node.t list))) : unit ->
Printf.fprintf ppf "\t%d -> " n.id;
List.iter (fun (x: Node.t) -> Printf.fprintf ppf "%d, " x.id) xs;
Printf.fprintf ppf "\n"
) (NodeMap.to_list c.reverse_edges);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Input Value: ";
(match c.input_val with
Some i -> Printf.fprintf ppf "%d" i;
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Input and Output Vars: ";
(match c.input_output_var with
Some (i, o) -> Printf.fprintf ppf "(in: %s, out: %s)" i o;
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Initial node's id: ";
(match c.initial with
Some i -> Printf.fprintf ppf "%d" (i.id);
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Terminal node's id: ";
(match c.terminal with
Some i -> Printf.fprintf ppf "%d" (i.id);
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Code:\n";
List.iter (fun ((n, stms) : Node.t * elt list) : unit ->
Printf.fprintf ppf "\tid %d --> %a\n%!" n.id M.pp_list stms
) (NodeMap.to_list c.content);
Printf.fprintf ppf "\n";
end
;;

48
lib/analysis/Cfg.mli Normal file
View File

@ -0,0 +1,48 @@
module type PrintableType = sig
type t
val pp : out_channel -> t -> unit
val pp_list : out_channel -> t list -> unit
end
module Node : sig
type t = {
id: int;
}
val compare : t -> t -> int
val create : unit -> t
end
module NodeMap : sig
include Map.S with type key = Node.t
val add_to_list_last : key -> 'a -> 'a list t -> 'a list t
end
module NodeSet : Set.S with type elt = Node.t
type 'a cfginternal = {
empty: bool;
nodes: NodeSet.t;
edges: (Node.t * (Node.t option)) NodeMap.t;
reverse_edges: (Node.t list) NodeMap.t;
input_val: int option;
input_output_var: (string * string) option;
initial: Node.t option;
terminal: Node.t option;
content: 'a list NodeMap.t;
}
module type C = sig
type elt
type t = elt cfginternal
val empty : t
val merge : t -> t -> Node.t -> Node.t -> t
val concat : t -> t -> t
val add_to_last_node : elt -> t -> t
val pp : out_channel -> t -> unit
end
module Make (M: PrintableType) : C with type elt = M.t

196
lib/analysis/Dataflow.ml Normal file
View File

@ -0,0 +1,196 @@
module type C = sig
type elt
type internal
type internal_node = {
internal_in: internal list;
internal_out: internal list;
internal_between: (internal list * internal list) list;
}
type cfgt = elt Cfg.cfginternal
type t = {
t: cfgt;
internal_var: internal_node Cfg.NodeMap.t;
}
val from_cfg : cfgt -> t
val to_cfg : t -> cfgt
val fixed_point :
?init : (elt list -> internal_node) ->
?update : (t -> Cfg.Node.t -> internal_node) ->
t ->
t
val pp : out_channel -> t -> unit
end
module Make (M: Cfg.PrintableType) (I: Cfg.PrintableType) = struct
type elt = M.t
type internal = I.t
type internal_node = {
internal_in: internal list;
internal_out: internal list;
internal_between: (internal list * internal list) list;
}
let compare_internal_node (a:internal_node) (b:internal_node) : bool =
match Utility.equality a.internal_in b.internal_in,
Utility.equality a.internal_out b.internal_out,
(List.fold_left2 (fun acc (ain, aout) (bin, bout)
-> acc &&
(Utility.equality ain bin) &&
(Utility.equality aout bout)
) true a.internal_between b.internal_between)
with
| true, true, true -> true
| _, _, _ -> false
type cfgt = elt Cfg.cfginternal
type t = {
t: cfgt;
internal_var: internal_node Cfg.NodeMap.t;
}
let compare_internal a b =
Cfg.NodeMap.fold
(fun node bi acc ->
match Cfg.NodeMap.find_opt node a with
None -> false
| Some ai -> acc && compare_internal_node ai bi
) b true
let from_cfg (cfg: cfgt) : t =
{t = cfg; internal_var = Cfg.NodeMap.empty}
let to_cfg ({t; _}: t) : cfgt =
t
open Cfg
let pp (ppf: out_channel) (c: t) : unit = (
Printf.fprintf ppf "Cfg:\n";
Printf.fprintf ppf "Nodes' ids: ";
List.iter (fun (x : Node.t) ->
Printf.fprintf ppf "%d " x.id) (NodeSet.to_list c.t.nodes);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Nodes' edges:\n";
List.iter (fun ((n, (a, b)) : (Node.t * (Node.t * Node.t option))) : unit ->
match b with
None -> Printf.fprintf ppf "\t%d -> %d\n" n.id a.id
| Some b -> Printf.fprintf ppf "\t%d -> %d, %d\n" n.id a.id b.id
) (NodeMap.to_list c.t.edges);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Nodes' back edges:\n";
List.iter (fun ((n, xs) : (Node.t * (Node.t list))) : unit ->
Printf.fprintf ppf "\t%d -> " n.id;
List.iter (fun (x: Node.t) -> Printf.fprintf ppf "%d, " x.id) xs;
Printf.fprintf ppf "\n"
) (NodeMap.to_list c.t.reverse_edges);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Input Value: ";
(match c.t.input_val with
Some i -> Printf.fprintf ppf "%d" i;
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Input and Output Vars: ";
(match c.t.input_output_var with
Some (i, o) -> Printf.fprintf ppf "(in: %s, out: %s)" i o;
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Initial node's id: ";
(match c.t.initial with
Some i -> Printf.fprintf ppf "%d" (i.id);
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Terminal node's id: ";
(match c.t.terminal with
Some i -> Printf.fprintf ppf "%d" (i.id);
| None -> Printf.fprintf ppf "None";);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Code:\n";
List.iter (fun ((n, stms) : Node.t * elt list) : unit ->
Printf.fprintf ppf "\tid %d --> %a\n%!" n.id M.pp_list stms
) (NodeMap.to_list c.t.content);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Analysis structure:\n";
List.iter (fun ((n, {internal_in; internal_out; internal_between})
: (Node.t * internal_node)) : unit ->
Printf.fprintf ppf "Node: %d\n" n.id;
Printf.fprintf ppf "Internal Input: ";
Printf.fprintf ppf "%a\n" I.pp_list internal_in;
Printf.fprintf ppf "Internal Output: ";
Printf.fprintf ppf "%a\n" I.pp_list internal_out;
Printf.fprintf ppf "Internal Between: ";
List.iter (fun (i, o) ->
Printf.fprintf ppf "IN: %a;" I.pp_list i;
Printf.fprintf ppf "OUT: %a;" I.pp_list o;)
internal_between;
Printf.fprintf ppf "\n";
) (NodeMap.to_list c.internal_var);
Printf.fprintf ppf "\n";
)
let fixed_point
?(init : (elt list -> internal_node) =
(fun _ -> {internal_in = [];
internal_out = [];
internal_between = []}))
?(update : (t -> Cfg.Node.t -> internal_node) =
(fun t n -> Cfg.NodeMap.find n t.internal_var))
(t: t)
: t =
(* init function is applied only once to each node content,
the update function takes the node and the whole structure and is
expected to return the updated structure for the appropriate node,
update function is applied to the resulting structure until no change is
observed with compareinternal function
*)
let rec aux t =
let newt =
{t with
internal_var = Cfg.NodeMap.mapi (fun n _ -> update t n) t.internal_var}
in
if compare_internal newt.internal_var t.internal_var
then newt
else aux newt
in
let content =
List.fold_left
(fun cfg node -> Cfg.NodeMap.add node {internal_in = [];
internal_out = [];
internal_between = []} cfg)
Cfg.NodeMap.empty
(Cfg.NodeSet.to_list t.t.nodes)
in
let code = (* we add back in the nodes with no code (there is no binding
in the t.t.content map) *)
Cfg.NodeMap.union (fun _n c _empty -> Some c)
t.t.content
(Cfg.NodeMap.of_list
(Cfg.NodeSet.to_list t.t.nodes |> List.map (fun c -> (c, []))))
in
let content = Cfg.NodeMap.union
(fun _key _empty code -> Some code)
content
(Cfg.NodeMap.map init code)
in
aux { t with internal_var = content }
end

31
lib/analysis/Dataflow.mli Normal file
View File

@ -0,0 +1,31 @@
module type C = sig
type elt
type internal
type internal_node = {
internal_in: internal list;
internal_out: internal list;
internal_between: (internal list * internal list) list;
}
type cfgt = elt Cfg.cfginternal
type t = {
t: cfgt;
internal_var: internal_node Cfg.NodeMap.t;
}
val from_cfg : cfgt -> t
val to_cfg : t -> cfgt
val fixed_point :
?init : (elt list -> internal_node) ->
?update : (t -> Cfg.Node.t -> internal_node) -> t -> t
val pp : out_channel -> t -> unit
end
module Make
(M: Cfg.PrintableType)
(I: Cfg.PrintableType)
: C with type elt = M.t and type internal = I.t

7
lib/analysis/dune Normal file
View File

@ -0,0 +1,7 @@
(library
(name analysis)
(public_name analysis)
(modules Cfg Dataflow)
(libraries utility))
(include_subdirs qualified)

5
lib/exercises/dune
View File

@ -1,5 +0,0 @@
(library
(name exercises)
(public_name exercises))
(include_subdirs qualified)

109
lib/exercises/exercises.ml
View File

@ -1,109 +0,0 @@
type a_exp =
Aval of int
| Plus of a_exp * a_exp
| Minus of a_exp * a_exp
| Times of a_exp * a_exp
| Of_bool of b_exp
and b_exp =
Bval of bool
| And of b_exp * b_exp
| Or of b_exp * b_exp
| Not of b_exp
| Minor of a_exp * a_exp
let rec eval_a_exp node =
match node with
Aval (i) -> i
| Plus (i, j) -> (eval_a_exp i) + (eval_a_exp j)
| Minus (i, j) -> (eval_a_exp i) - (eval_a_exp j)
| Times (i, j) -> (eval_a_exp i) * (eval_a_exp j)
| Of_bool b -> if (eval_b_exp b) then 1 else 0
and eval_b_exp node =
match node with
Bval (b) -> b
| And (a, b) -> (eval_b_exp a) && (eval_b_exp b)
| Or (a, b) -> (eval_b_exp a) || (eval_b_exp b)
| Not b -> not (eval_b_exp b)
| Minor (i, j) -> (eval_a_exp i) < (eval_a_exp j)
type 'a my_tree =
Leaf of 'a
| Node of ('a my_tree) list
let mod_list y =
(List.fold_left
(fun acc x ->
match acc with
| [a] when ((List.hd a) = x) -> [x :: a]
| a :: tl when ((List.hd a) = x) -> (x :: a) :: tl
| _ -> [x] :: acc)
[]
y)
|> List.rev
(* -------------------------------------------------------------------------- *)
let to_tup f g =
fun x -> match x with
(a, b) -> (f a, g b)
let partialsum l =
snd (List.fold_left_map (fun acc x -> (acc+x, acc+x)) 0 l)
type label =
string
type 'a finite_state_automata = {
l: label;
next: ('a finite_state_automata * 'a list) list;
final: bool;
}
let rec check_included input fsa =
match input with
[] -> fsa.final
| a::rest -> (
match List.find_opt (fun x -> List.mem a (snd x)) fsa.next with
None -> false
| Some x -> check_included rest (fst x)
)
(* -------------------------------------------------------------------------- *)
module StringMap = Map.Make(String)
type fsa = {
vertices: bool StringMap.t;
edges: (string * char) StringMap.t;
state: string;
}
let ex8 (instr: char list) (infsa: fsa) =
let rec helper_ex8 (i: char list) (ifsa: fsa) (current: string) =
match i with
[] -> (
match StringMap.find_opt current ifsa.vertices with
None -> false
| Some b -> b
)
| a::rest -> (
match StringMap.find_first_opt (fun _ -> true) (StringMap.filter (fun x (_, y) -> x = current && y = a) ifsa.edges) with
None -> false
| Some (_, (outedge, _)) -> helper_ex8 rest ifsa outedge
)
in helper_ex8 instr infsa infsa.state
type binary_tree =
Node of binary_tree * binary_tree
| Leaf of int
let ex9 b =
let rec helper_ex9 b' n =
match b' with
Leaf a -> a + n
| Node (r, l) -> (helper_ex9 r (helper_ex9 l n))
in helper_ex9 b 0
(* -------------------------------------------------------------------------- *)

60
lib/exercises/exercises.mli
View File

@ -1,60 +0,0 @@
type a_exp =
Aval of int
| Plus of a_exp * a_exp
| Minus of a_exp * a_exp
| Times of a_exp * a_exp
| Of_bool of b_exp
and b_exp =
Bval of bool
| And of b_exp * b_exp
| Or of b_exp * b_exp
| Not of b_exp
| Minor of a_exp * a_exp
val eval_a_exp: a_exp -> int
val eval_b_exp: b_exp -> bool
type 'a my_tree =
Leaf of 'a
| Node of ('a my_tree) list
val mod_list: 'a list -> 'a list list
(* --------------------------------------------------------------------------- *)
val to_tup : ('a -> 'b) -> ('c -> 'd) -> (('a * 'c) -> ('b * 'd))
val partialsum : int list -> int list
type label =
string
type 'a finite_state_automata = {
l: label;
next: ('a finite_state_automata * 'a list) list;
final: bool;
}
val check_included : 'a list -> 'a finite_state_automata -> bool
(* -------------------------------------------------------------------------- *)
module StringMap : Map.S with type key = string
type fsa = {
vertices: bool StringMap.t;
edges: (string * char) StringMap.t;
state: string;
}
val ex8 : char list -> fsa -> bool
type binary_tree =
Node of binary_tree * binary_tree
| Leaf of int
val ex9 : binary_tree -> int
(* -------------------------------------------------------------------------- *)

1
lib/miniFun/Lexer.mll
View File

@ -81,6 +81,7 @@ rule read = parse
(lexbuf.Lexing.lex_curr_p.Lexing.pos_lnum)
(lexbuf.Lexing.lex_curr_p.Lexing.pos_lnum)
))}
and comments level = parse
| "*)" {if level = 0
then read lexbuf

3
lib/miniFun/Parser.mly
View File

@ -24,7 +24,6 @@
%start prg
(* associativity in order of precedence *)
/*%right rightlowest */
%left lowest
%right TYPEFUNCTION
%left COMMA
@ -35,7 +34,7 @@
%left CMP CMPLESS CMPLESSEQ CMPGREATER CMPGREATEREQ
%left PLUS MINUS
%left TIMES DIVISION MODULO
%left POWER
%right POWER
%right BNOT RAND
%left FIRST SECOND
%left LAMBDA

21
lib/miniFun/Semantics.ml
View File

@ -5,14 +5,17 @@ Random.self_init ()
let (let*) = Result.bind
let rec evaluate (mem: memory) (command: t_exp) : (permittedValues, [> error]) result =
let rec evaluate (mem: memory) (command: t_exp) :
(permitted_values, [> error]) result =
match command with
Integer n -> Ok (IntegerPermitted n)
| Boolean b -> Ok (BooleanPermitted b)
| Variable v -> (
match VariableMap.find_opt v mem.assignments with
None -> Error (`AbsentAssignment ("The variable " ^ v ^ " is not defined."))
| Some a -> Ok a
| None ->
Error (`AbsentAssignment ("The variable " ^ v ^ " is not defined."))
| Some a ->
Ok a
)
| Tuple (x, y) -> (
let* xval = evaluate mem x in
@ -28,7 +31,7 @@ let rec evaluate (mem: memory) (command: t_exp) : (permittedValues, [> error]) r
)
| Application (f, x) -> (
let* evalf = evaluate mem f in
let* funcClosure = (
let* func_closure = (
match evalf with
FunctionPermitted ff -> Ok ff
| IntegerPermitted _ -> Error (`WrongType ("Function is not a function,"
@ -40,15 +43,15 @@ let rec evaluate (mem: memory) (command: t_exp) : (permittedValues, [> error]) r
) in
let* param = evaluate mem x in
let mem2 =
match funcClosure.recursiveness with
match func_closure.recursiveness with
None -> {assignments = (
VariableMap.add funcClosure.input param funcClosure.assignments)}
VariableMap.add func_closure.input param func_closure.assignments)}
| Some nameF -> {assignments = (
VariableMap.add funcClosure.input param funcClosure.assignments |>
VariableMap.add nameF (FunctionPermitted funcClosure)
VariableMap.add func_closure.input param func_closure.assignments |>
VariableMap.add nameF (FunctionPermitted func_closure)
)}
in
evaluate mem2 funcClosure.body
evaluate mem2 func_closure.body
)
| Plus (a, b) ->
let* aval = (

2
lib/miniFun/Semantics.mli
View File

@ -1,3 +1,3 @@
val evaluate : Types.memory -> Types.t_exp -> (Types.permittedValues, [> Types.error]) result
val evaluate : Types.memory -> Types.t_exp -> (Types.permitted_values, [> Types.error]) result
val reduce : Types.t_exp -> int -> (int, [> Types.error]) result

6
lib/miniFun/TypeChecker.ml
View File

@ -53,7 +53,8 @@ let evaluate_type_polimorphic (_program: t_exp) (_context: typingshape) : (typin
(* | LetIn (x, xval, rest) -> failwith "Not Implemented" *)
(* | LetFun (f, xs, typef, fbody, rest) -> failwith "Not Implemented" *)
let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype, [> typechecking_error]) result =
let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) :
(ftype, [> typechecking_error]) result =
match program with
Integer _ -> Ok IntegerType
| Boolean _ -> Ok BooleanType
@ -73,7 +74,8 @@ let rec evaluate_type (program: t_exp) (context: ftype VariableMap.t) : (ftype,
the type of the body using the bindings for the input *)
match typef with
FunctionType (tin, tout) -> (
let* typefbody = evaluate_type fbody (VariableMap.add x tin context) in
let* typefbody = evaluate_type fbody (VariableMap.add x tin context)
in
if (typefbody = tout) then
Ok typef
else

63
lib/miniFun/Types.ml
View File

@ -19,48 +19,49 @@ type typingshape = (* tuple of a simple type environment and a simple type *)
fenvironment * ftype
type t_exp =
Integer of int (* x := a *)
| Boolean of bool (* v *)
| Variable of variable (* x *)
| Tuple of t_exp * t_exp (* (a, b) *)
| Function of variable * ftype * t_exp (* lambda x: t. x *)
| Application of t_exp * t_exp (* x x *)
| Plus of t_exp * t_exp (* x + x *)
| Minus of t_exp * t_exp (* x - x *)
| Times of t_exp * t_exp (* x * x *)
| Division of t_exp * t_exp (* x / x *)
| Modulo of t_exp * t_exp (* x % x *)
| Power of t_exp * t_exp (* x ^ x *)
| PowerMod of t_exp * t_exp * t_exp (* (x ^ x) % x *)
| Rand of t_exp (* rand(0, x) *)
| BAnd of t_exp * t_exp (* x && x *)
| BOr of t_exp * t_exp (* x || x *)
| BNot of t_exp (* not x *)
| First of t_exp (* fst x *)
| Second of t_exp (* scn x *)
| Cmp of t_exp * t_exp (* x == x *)
| CmpLess of t_exp * t_exp (* x < x *)
| CmpLessEq of t_exp * t_exp (* x <= x *)
| CmpGreater of t_exp * t_exp (* x > x *)
| CmpGreaterEq of t_exp * t_exp (* x >= x *)
| IfThenElse of t_exp * t_exp * t_exp (* if b then c else c *)
| LetIn of variable * t_exp * t_exp (* let x = x in x *)
| LetFun of variable * variable * ftype * t_exp * t_exp (* let rec x. y: t. x in x*)
Integer of int (* x := a *)
| Boolean of bool (* v *)
| Variable of variable (* x *)
| Tuple of t_exp * t_exp (* (a, b) *)
| Function of variable * ftype * t_exp (* lambda x: t. x *)
| Application of t_exp * t_exp (* x x *)
| Plus of t_exp * t_exp (* x + x *)
| Minus of t_exp * t_exp (* x - x *)
| Times of t_exp * t_exp (* x * x *)
| Division of t_exp * t_exp (* x / x *)
| Modulo of t_exp * t_exp (* x % x *)
| Power of t_exp * t_exp (* x ^ x *)
| PowerMod of t_exp * t_exp * t_exp (* (x ^ x) % x *)
| Rand of t_exp (* rand(0, x) *)
| BAnd of t_exp * t_exp (* x && x *)
| BOr of t_exp * t_exp (* x || x *)
| BNot of t_exp (* not x *)
| First of t_exp (* fst x *)
| Second of t_exp (* scn x *)
| Cmp of t_exp * t_exp (* x == x *)
| CmpLess of t_exp * t_exp (* x < x *)
| CmpLessEq of t_exp * t_exp (* x <= x *)
| CmpGreater of t_exp * t_exp (* x > x *)
| CmpGreaterEq of t_exp * t_exp (* x >= x *)
| IfThenElse of t_exp * t_exp * t_exp (* if b then c else c *)
| LetIn of variable * t_exp * t_exp (* let x = x in x *)
| LetFun of variable * variable * ftype * t_exp * t_exp
(* let rec x. y: t. x in x*)
type permittedValues =
type permitted_values =
IntegerPermitted of int
| BooleanPermitted of bool
| TuplePermitted of permittedValues * permittedValues
| TuplePermitted of permitted_values * permitted_values
| FunctionPermitted of closure
and closure = {
input: variable;
body: t_exp;
assignments: permittedValues VariableMap.t;
assignments: permitted_values VariableMap.t;
recursiveness: variable option
}
type memory = {
assignments: permittedValues VariableMap.t
assignments: permitted_values VariableMap.t
}

8
lib/miniFun/Types.mli
View File

@ -73,20 +73,20 @@ type t_exp =
| LetIn of variable * t_exp * t_exp (* let x = x in x *)
| LetFun of variable * variable * ftype * t_exp * t_exp (* let rec x. y: t. x in x*)
type permittedValues =
type permitted_values =
IntegerPermitted of int
| BooleanPermitted of bool
| TuplePermitted of permittedValues * permittedValues
| TuplePermitted of permitted_values * permitted_values
| FunctionPermitted of closure
and closure = {
input: variable;
body: t_exp;
assignments: permittedValues VariableMap.t;
assignments: permitted_values VariableMap.t;
recursiveness: variable option
}
type memory = {
assignments: permittedValues VariableMap.t
assignments: permitted_values VariableMap.t
}

316
lib/miniImp/Cfg.ml
View File

@ -1,316 +0,0 @@
type simpleStatements =
| SimpleSkip
| SimpleAssignment of Types.variable * simpleArithmetic
| SimpleGuard of simpleBoolean
and simpleBoolean =
| SimpleBoolean of bool
| SimpleBAnd of simpleBoolean * simpleBoolean
| SimpleBOr of simpleBoolean * simpleBoolean
| SimpleBNot of simpleBoolean
| SimpleBCmp of simpleArithmetic * simpleArithmetic
| SimpleBCmpLess of simpleArithmetic * simpleArithmetic
| SimpleBCmpLessEq of simpleArithmetic * simpleArithmetic
| SimpleBCmpGreater of simpleArithmetic * simpleArithmetic
| SimpleBCmpGreaterEq of simpleArithmetic * simpleArithmetic
and simpleArithmetic =
| SimpleVariable of Types.variable
| SimpleInteger of int
| SimplePlus of simpleArithmetic * simpleArithmetic
| SimpleMinus of simpleArithmetic * simpleArithmetic
| SimpleTimes of simpleArithmetic * simpleArithmetic
| SimpleDivision of simpleArithmetic * simpleArithmetic
| SimpleModulo of simpleArithmetic * simpleArithmetic
| SimplePower of simpleArithmetic * simpleArithmetic
| SimplePowerMod of simpleArithmetic * simpleArithmetic * simpleArithmetic
| SimpleRand of simpleArithmetic
let printSingleStatement (ppf) (c: simpleStatements) : unit =
let rec helper_c (ppf) (c: simpleStatements) : unit =
match c with
| SimpleSkip -> Printf.fprintf ppf "Skip"
| SimpleAssignment (v, a) -> Printf.fprintf ppf "Assignment {%s, %a}" v helper_a a
| SimpleGuard (b) -> Printf.fprintf ppf "Guard {%a}" helper_b b
and helper_b (ppf) (c: simpleBoolean) : unit =
match c with
| SimpleBoolean b -> Printf.fprintf ppf "%b" b
| SimpleBAnd (b1, b2) -> Printf.fprintf ppf "{%a && %a}" helper_b b1 helper_b b2
| SimpleBOr (b1, b2) -> Printf.fprintf ppf "{%a || %a}" helper_b b1 helper_b b2
| SimpleBNot b -> Printf.fprintf ppf "{not %a}" helper_b b
| SimpleBCmp (a1, a2) -> Printf.fprintf ppf "{%a == %a}" helper_a a1 helper_a a2
| SimpleBCmpLess (a1, a2) -> Printf.fprintf ppf "{%a < %a}" helper_a a1 helper_a a2
| SimpleBCmpLessEq (a1, a2) -> Printf.fprintf ppf "{%a <= %a}" helper_a a1 helper_a a2
| SimpleBCmpGreater (a1, a2) -> Printf.fprintf ppf "{%a > %a}" helper_a a1 helper_a a2
| SimpleBCmpGreaterEq (a1, a2) -> Printf.fprintf ppf "{%a >= %a}" helper_a a1 helper_a a2
and helper_a (ppf) (c: simpleArithmetic) : unit =
match c with
| SimpleVariable (v) -> Printf.fprintf ppf "%s" v
| SimpleInteger (i) -> Printf.fprintf ppf "%d" i
| SimplePlus (a1, a2) -> Printf.fprintf ppf "{%a + %a}" helper_a a1 helper_a a2
| SimpleMinus (a1, a2) -> Printf.fprintf ppf "{%a - %a}" helper_a a1 helper_a a2
| SimpleTimes (a1, a2) -> Printf.fprintf ppf "{%a * %a}" helper_a a1 helper_a a2
| SimpleDivision (a1, a2) -> Printf.fprintf ppf "{%a / %a}" helper_a a1 helper_a a2
| SimpleModulo (a1, a2) -> Printf.fprintf ppf "{%a %% %a}" helper_a a1 helper_a a2
| SimplePower (a1, a2) -> Printf.fprintf ppf "{%a ^ %a}" helper_a a1 helper_a a2
| SimplePowerMod (a1, a2, a3) -> Printf.fprintf ppf "{powmod %a %a %a}" helper_a a1 helper_a a2 helper_a a3
| SimpleRand (a) -> Printf.fprintf ppf "{rand %a}" helper_a a
in
helper_c ppf c
let printSimpleStatements (ppf) (c: simpleStatements list) : unit =
List.iter (fun x -> printSingleStatement ppf x; Printf.printf "; ") c
let globalIdNode = ref 0;
module Node = struct
type t = {
id: int
}
let compare a b = compare a.id b.id
let newNode () =
globalIdNode := !globalIdNode + 1;
{id = !globalIdNode}
end
;;
module NodeMap = Map.Make(Node)
module NodeSet = Set.Make(Node)
module Cfg = struct
type t = {
empty: bool;
nodes: NodeSet.t;
edges: (Node.t * (Node.t option)) NodeMap.t;
reverseedges: (Node.t list) NodeMap.t;
initial: Node.t option;
terminal: Node.t option;
code: (simpleStatements list) NodeMap.t
}
let newCfg () =
{ empty = true;
nodes = NodeSet.empty;
edges = NodeMap.empty;
reverseedges = NodeMap.empty;
initial = None;
terminal = None;
code = NodeMap.empty }
let mergeCfg (cfg1: t) (cfg2: t) (entryNode: Node.t) (exitNode: Node.t) : t =
match (cfg1.empty, cfg2.empty) with
true, _ -> cfg2
| _, true -> cfg1
| false, false ->
let cfg1initial = Option.get cfg1.initial in
let cfg2initial = Option.get cfg2.initial in
let cfg1terminal = Option.get cfg1.terminal in
let cfg2terminal = Option.get cfg2.terminal in
{ empty = false;
nodes = NodeSet.union cfg1.nodes cfg2.nodes |>
NodeSet.add entryNode |>
NodeSet.add exitNode;
edges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
cfg1.edges cfg2.edges |>
NodeMap.add entryNode (cfg1initial, Some cfg2initial) |>
NodeMap.add cfg1terminal (exitNode, None) |>
NodeMap.add cfg2terminal (exitNode, None);
reverseedges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
cfg1.reverseedges cfg2.reverseedges |>
NodeMap.add_to_list cfg1initial entryNode |>
NodeMap.add_to_list cfg2initial entryNode |>
NodeMap.add_to_list exitNode cfg1terminal |>
NodeMap.add_to_list exitNode cfg2terminal;
initial = Some entryNode;
terminal = Some exitNode;
code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.")
cfg1.code cfg2.code
}
let concatCfg (cfg1: t) (cfg2: t) : t =
match (cfg1.empty, cfg2.empty) with
true, _ -> cfg2
| _, true -> cfg1
| false, false ->
let cfg1initial = Option.get cfg1.initial in
let cfg2initial = Option.get cfg2.initial in
let cfg1terminal = Option.get cfg1.terminal in
let cfg2terminal = Option.get cfg2.terminal in
{ empty = false;
nodes = NodeSet.union cfg1.nodes cfg2.nodes;
edges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
cfg1.edges cfg2.edges |>
NodeMap.add cfg1terminal (cfg2initial, None);
reverseedges = NodeMap.union (fun _ -> failwith "Failed merging edges of cfg.")
cfg1.reverseedges cfg2.reverseedges |>
NodeMap.add_to_list cfg2initial cfg1terminal;
initial = Some cfg1initial;
terminal = Some cfg2terminal;
code = NodeMap.union (fun _ -> failwith "Failed merging code of cfg.")
cfg1.code cfg2.code
}
let addToLastNode (newcode: simpleStatements) (cfg: t) : t =
match cfg.empty with
| true -> let newnode = Node.newNode () in
{ empty = false;
nodes = NodeSet.singleton newnode;
edges = NodeMap.empty;
reverseedges = NodeMap.empty;
initial = Some newnode;
terminal = Some newnode;
code = NodeMap.singleton newnode [newcode]
}
| false ->
let prevcfgterminal = Option.get cfg.terminal in
{ cfg with
code = (NodeMap.add_to_list
prevcfgterminal
newcode
cfg.code) }
let pp (ppf) (c: t) : unit =
Printf.fprintf ppf "Nodes' ids: ";
List.iter (fun (x : Node.t) -> Printf.fprintf ppf "%d " x.id) (NodeSet.to_list c.nodes);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Nodes' edges:\n";
List.iter (fun ((n, (a, b)) : (Node.t * (Node.t * Node.t option))) : unit ->
match b with None -> Printf.fprintf ppf "\t%d -> %d\n" n.id a.id
| Some b -> Printf.fprintf ppf "\t%d -> %d, %d\n" n.id a.id b.id
) (NodeMap.to_list c.edges);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Nodes' back edges:\n";
List.iter (fun ((n, xs) : (Node.t * (Node.t list))) : unit ->
Printf.fprintf ppf "\t%d -> " n.id;
List.iter (fun (x: Node.t) -> Printf.fprintf ppf "%d, " x.id) xs;
Printf.fprintf ppf "\n"
) (NodeMap.to_list c.reverseedges);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Initial node's id: ";
Printf.fprintf ppf "%d" ((Option.get c.initial).id);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Terminal node's id: ";
Printf.fprintf ppf "%d" ((Option.get c.terminal).id);
Printf.fprintf ppf "\n";
Printf.fprintf ppf "Code:\n";
List.iter (fun ((n, stms) : Node.t * simpleStatements list) : unit ->
Printf.fprintf ppf "\tid %d --> %a\n%!" n.id printSimpleStatements (List.rev stms)
) (NodeMap.to_list c.code);
Printf.fprintf ppf "\n";
end
;;
let rec convert_c (prevcfg: Cfg.t) (prg: Types.c_exp) : Cfg.t =
match prg with
| Skip -> prevcfg |> Cfg.addToLastNode SimpleSkip
| Assignment (x, a) -> prevcfg |> Cfg.addToLastNode (SimpleAssignment (x, convert_a a))
| Sequence (c1, c2) ->
let cfg1 = convert_c prevcfg c1 in
let cfg2 = convert_c cfg1 c2 in
cfg2
| If (b, c1, c2) ->
let convertedb = convert_b b in
let cfg1 = convert_c (Cfg.newCfg ()) c1 in
let cfg2 = convert_c (Cfg.newCfg ()) c2 in
let entrynode = Node.newNode () in
let exitnode = Node.newNode () in
let newcfg = Cfg.mergeCfg cfg1 cfg2 entrynode exitnode in
let mergedcfg = Cfg.concatCfg prevcfg newcfg in
{ mergedcfg with
code = mergedcfg.code |>
NodeMap.add_to_list entrynode (SimpleGuard convertedb) |>
NodeMap.add_to_list exitnode (SimpleSkip) }
| While (b, c) ->
let convertedb = convert_b b in
let cfg = convert_c (Cfg.newCfg ()) c in
let cfginitial = Option.get cfg.initial in
let cfgterminal = Option.get cfg.terminal in
let entrynode = Node.newNode () in
let guardnode = Node.newNode () in
let exitnode = Node.newNode () in
{ empty = false;
nodes = cfg.nodes |>
NodeSet.add entrynode |>
NodeSet.add guardnode |>
NodeSet.add exitnode;
edges = cfg.edges |>
NodeMap.add entrynode (guardnode, None) |>
NodeMap.add guardnode (cfginitial, Some exitnode) |>
NodeMap.add cfgterminal (guardnode, None);
reverseedges = cfg.reverseedges |>
NodeMap.add_to_list guardnode entrynode |>
NodeMap.add_to_list cfginitial guardnode |>
NodeMap.add_to_list exitnode guardnode |>
NodeMap.add_to_list guardnode cfgterminal;
initial = Some entrynode;
terminal = Some exitnode;
code = NodeMap.add_to_list guardnode (SimpleGuard (convertedb)) cfg.code |>
NodeMap.add_to_list exitnode (SimpleSkip)
} |> Cfg.concatCfg prevcfg
| For (assignment, guard, increment, body) ->
let cfgassignment = convert_c (Cfg.newCfg ()) assignment in
let convertedguard = convert_b guard in
let cfgincrement = convert_c (Cfg.newCfg ()) increment in
let cfgbody = convert_c (Cfg.newCfg ()) body in
let prevassignment = Cfg.concatCfg prevcfg cfgassignment in
let bodyincrement = Cfg.concatCfg cfgbody cfgincrement in
let cfginitial = Option.get bodyincrement.initial in
let cfgterminal = Option.get bodyincrement.terminal in
let guardnode = Node.newNode () in
let exitnode = Node.newNode () in
{ empty = false;
nodes = bodyincrement.nodes |>
NodeSet.add guardnode |>
NodeSet.add exitnode;
edges = bodyincrement.edges |>
NodeMap.add guardnode (cfginitial, Some exitnode) |>
NodeMap.add cfgterminal (guardnode, None);
reverseedges = bodyincrement.reverseedges |>
NodeMap.add_to_list cfginitial guardnode |>
NodeMap.add_to_list exitnode guardnode |>
NodeMap.add_to_list guardnode cfgterminal;
initial = Some guardnode;
terminal = Some exitnode;
code = NodeMap.add_to_list guardnode (SimpleGuard (convertedguard)) bodyincrement.code |>
NodeMap.add_to_list exitnode (SimpleSkip)
} |> Cfg.concatCfg prevassignment
and convert_b (prg: Types.b_exp) : simpleBoolean =
match prg with
| Boolean (b) -> SimpleBoolean b
| BAnd (b1, b2) -> SimpleBAnd (convert_b b1, convert_b b2)
| BOr (b1, b2) -> SimpleBOr (convert_b b1, convert_b b2)
| BNot (b) -> SimpleBNot (convert_b b)
| BCmp (a1, a2) -> SimpleBCmp (convert_a a1, convert_a a2)
| BCmpLess (a1, a2) -> SimpleBCmpLess (convert_a a1, convert_a a2)
| BCmpLessEq (a1, a2) -> SimpleBCmpLessEq (convert_a a1, convert_a a2)
| BCmpGreater (a1, a2) -> SimpleBCmpGreater (convert_a a1, convert_a a2)
| BCmpGreaterEq (a1, a2) -> SimpleBCmpGreaterEq (convert_a a1, convert_a a2)
and convert_a (prg: Types.a_exp) : simpleArithmetic =
match prg with
| Variable x -> SimpleVariable x
| Integer n -> SimpleInteger n
| Plus (a1, a2) -> SimplePlus (convert_a a1, convert_a a2)
| Minus (a1, a2) -> SimpleMinus (convert_a a1, convert_a a2)
| Times (a1, a2) -> SimpleTimes (convert_a a1, convert_a a2)
| Division (a1, a2) -> SimpleDivision (convert_a a1, convert_a a2)
| Modulo (a1, a2) -> SimpleModulo (convert_a a1, convert_a a2)
| Power (a1, a2) -> SimplePower (convert_a a1, convert_a a2)
| PowerMod (a1, a2, a3) -> SimplePowerMod (convert_a a1, convert_a a2, convert_a a3)
| Rand (a) -> SimpleRand (convert_a a)
let convert (prg: Types.p_exp) : Cfg.t =
match prg with
| Main (_, _, exp) ->
convert_c (Cfg.newCfg ()) exp

40
lib/miniImp/Cfg.mli
View File

@ -1,40 +0,0 @@
type simpleStatements =
| SimpleSkip
| SimpleAssignment of Types.variable * simpleArithmetic
| SimpleGuard of simpleBoolean
and simpleBoolean =
| SimpleBoolean of bool
| SimpleBAnd of simpleBoolean * simpleBoolean
| SimpleBOr of simpleBoolean * simpleBoolean
| SimpleBNot of simpleBoolean
| SimpleBCmp of simpleArithmetic * simpleArithmetic
| SimpleBCmpLess of simpleArithmetic * simpleArithmetic
| SimpleBCmpLessEq of simpleArithmetic * simpleArithmetic
| SimpleBCmpGreater of simpleArithmetic * simpleArithmetic
| SimpleBCmpGreaterEq of simpleArithmetic * simpleArithmetic
and simpleArithmetic =
| SimpleVariable of Types.variable
| SimpleInteger of int
| SimplePlus of simpleArithmetic * simpleArithmetic
| SimpleMinus of simpleArithmetic * simpleArithmetic
| SimpleTimes of simpleArithmetic * simpleArithmetic
| SimpleDivision of simpleArithmetic * simpleArithmetic
| SimpleModulo of simpleArithmetic * simpleArithmetic
| SimplePower of simpleArithmetic * simpleArithmetic
| SimplePowerMod of simpleArithmetic * simpleArithmetic * simpleArithmetic
| SimpleRand of simpleArithmetic
module Node : sig
type t
val compare : t -> t -> int
end
module NodeMap : Map.S with type key = Node.t
module NodeSet : Set.S with type elt = Node.t
module Cfg : sig
type t
val pp : out_channel -> t -> unit
end
val convert : Types.p_exp -> Cfg.t

215
lib/miniImp/CfgImp.ml Normal file
View File

@ -0,0 +1,215 @@
open Analysis
open Analysis.Cfg
module SimpleStatements = struct
type t =
| SimpleSkip
| SimpleAssignment of Types.variable * simpleArithmetic
| SimpleGuard of simpleBoolean
and simpleBoolean =
| SimpleBoolean of bool
| SimpleBAnd of simpleBoolean * simpleBoolean
| SimpleBOr of simpleBoolean * simpleBoolean
| SimpleBNot of simpleBoolean
| SimpleBCmp of simpleArithmetic * simpleArithmetic
| SimpleBCmpLess of simpleArithmetic * simpleArithmetic
| SimpleBCmpLessEq of simpleArithmetic * simpleArithmetic
| SimpleBCmpGreater of simpleArithmetic * simpleArithmetic
| SimpleBCmpGreaterEq of simpleArithmetic * simpleArithmetic
and simpleArithmetic =
| SimpleVariable of Types.variable
| SimpleInteger of int
| SimplePlus of simpleArithmetic * simpleArithmetic
| SimpleMinus of simpleArithmetic * simpleArithmetic
| SimpleTimes of simpleArithmetic * simpleArithmetic
| SimpleDivision of simpleArithmetic * simpleArithmetic
| SimpleModulo of simpleArithmetic * simpleArithmetic
| SimplePower of simpleArithmetic * simpleArithmetic
| SimpleRand of simpleArithmetic
let pp (ppf: out_channel) (c: t) : unit =
let rec helper_c (ppf) (c: t) : unit =
match c with
| SimpleSkip ->
Printf.fprintf ppf "Skip"
| SimpleAssignment (v, a) ->
Printf.fprintf ppf "Assignment {%s, %a}" v helper_a a
| SimpleGuard (b) ->
Printf.fprintf ppf "Guard {%a}" helper_b b
and helper_b (ppf) (c: simpleBoolean) : unit =
match c with
| SimpleBoolean b ->
Printf.fprintf ppf "%b" b
| SimpleBAnd (b1, b2) ->
Printf.fprintf ppf "{%a && %a}" helper_b b1 helper_b b2
| SimpleBOr (b1, b2) ->
Printf.fprintf ppf "{%a || %a}" helper_b b1 helper_b b2
| SimpleBNot b ->
Printf.fprintf ppf "{not %a}" helper_b b
| SimpleBCmp (a1, a2) ->
Printf.fprintf ppf "{%a == %a}" helper_a a1 helper_a a2
| SimpleBCmpLess (a1, a2) ->
Printf.fprintf ppf "{%a < %a}" helper_a a1 helper_a a2
| SimpleBCmpLessEq (a1, a2) ->
Printf.fprintf ppf "{%a <= %a}" helper_a a1 helper_a a2
| SimpleBCmpGreater (a1, a2) ->
Printf.fprintf ppf "{%a > %a}" helper_a a1 helper_a a2
| SimpleBCmpGreaterEq (a1, a2) ->
Printf.fprintf ppf "{%a >= %a}" helper_a a1 helper_a a2
and helper_a (ppf) (c: simpleArithmetic) : unit =
match c with
| SimpleVariable (v) ->
Printf.fprintf ppf "%s" v
| SimpleInteger (i) ->
Printf.fprintf ppf "%d" i
| SimplePlus (a1, a2) ->
Printf.fprintf ppf "{%a + %a}" helper_a a1 helper_a a2
| SimpleMinus (a1, a2) ->
Printf.fprintf ppf "{%a - %a}" helper_a a1 helper_a a2
| SimpleTimes (a1, a2) ->
Printf.fprintf ppf "{%a * %a}" helper_a a1 helper_a a2
| SimpleDivision (a1, a2) ->
Printf.fprintf ppf "{%a / %a}" helper_a a1 helper_a a2
| SimpleModulo (a1, a2) ->
Printf.fprintf ppf "{%a %% %a}" helper_a a1 helper_a a2
| SimplePower (a1, a2) ->
Printf.fprintf ppf "{%a ^ %a}" helper_a a1 helper_a a2
| SimpleRand (a) ->
Printf.fprintf ppf "{rand %a}" helper_a a
in
helper_c ppf c
let pp_list (ppf: out_channel) (c: t list) : unit =
List.iter (fun x -> pp ppf x; Printf.printf "; ") c
end
module SSCfg = Cfg.Make(SimpleStatements)
let rec convert_c (prevcfg: SSCfg.t) (prg: Types.c_exp) : SSCfg.t =
let open SimpleStatements in
match prg with
| Skip -> (* we preserve the skips *)
prevcfg |> SSCfg.add_to_last_node SimpleSkip
| Assignment (x, a) -> (* we simply add the assignment to the terminal node *)
prevcfg |> SSCfg.add_to_last_node (SimpleAssignment (x, convert_a a))
| Sequence (c1, c2) -> (* we first convert the first sequence, then the second
using the previous as prevcfg *)
let cfg1 = convert_c prevcfg c1 in
let cfg2 = convert_c cfg1 c2 in
cfg2
| If (b, c1, c2) -> (* constructs two branches with a two new nodes *)
let converted_b = convert_b b in
let cfg1 = convert_c SSCfg.empty c1 in
let cfg2 = convert_c SSCfg.empty c2 in
let entrynode = Node.create () in
let exitnode = Node.create () in
let newcfg = SSCfg.merge cfg1 cfg2 entrynode exitnode in
let mergedcfg = SSCfg.concat prevcfg newcfg in
{ mergedcfg with
content = mergedcfg.content |>
NodeMap.add_to_list entrynode (SimpleGuard converted_b) |>
NodeMap.add_to_list exitnode (SimpleSkip) }
| While (b, c) -> (* constructs a loop, needs three new nodes *)
let converted_b = convert_b b in
let cfg = convert_c SSCfg.empty c in
let cfginitial = Option.get cfg.initial in
let cfgterminal = Option.get cfg.terminal in
let entrynode = Node.create () in
let guardnode = Node.create () in
let exitnode = Node.create () in
{ empty = false;
nodes = cfg.nodes |>
NodeSet.add entrynode |>
NodeSet.add guardnode |>
NodeSet.add exitnode;
edges = cfg.edges |>
NodeMap.add entrynode (guardnode, None) |>
NodeMap.add guardnode (cfginitial, Some exitnode) |>
NodeMap.add cfgterminal (guardnode, None);
reverse_edges = cfg.reverse_edges |>
NodeMap.add_to_list guardnode entrynode |>
NodeMap.add_to_list cfginitial guardnode |>
NodeMap.add_to_list exitnode guardnode |>
NodeMap.add_to_list guardnode cfgterminal;
input_val = prevcfg.input_val;
input_output_var = prevcfg.input_output_var;
initial = Some entrynode;
terminal = Some exitnode;
content = cfg.content |>
NodeMap.add_to_list guardnode (SimpleGuard (converted_b)) |>
NodeMap.add_to_list exitnode (SimpleSkip)
} |> SSCfg.concat prevcfg
| For (assignment, guard, increment, body) -> (* constructs a loop, needs
two new nodes *)
let cfgassignment = convert_c SSCfg.empty assignment in
let convertedguard = convert_b guard in
let cfgincrement = convert_c SSCfg.empty increment in
let cfgbody = convert_c SSCfg.empty body in
let prevassignment = SSCfg.concat prevcfg cfgassignment in
let bodyincrement = SSCfg.concat cfgbody cfgincrement in
let cfginitial = Option.get bodyincrement.initial in
let cfgterminal = Option.get bodyincrement.terminal in
let guardnode = Node.create () in
let exitnode = Node.create () in
{ empty = false;
nodes = bodyincrement.nodes |>
NodeSet.add guardnode |>
NodeSet.add exitnode;
edges = bodyincrement.edges |>
NodeMap.add guardnode (cfginitial, Some exitnode) |>
NodeMap.add cfgterminal (guardnode, None);
reverse_edges = bodyincrement.reverse_edges |>
NodeMap.add_to_list cfginitial guardnode |>
NodeMap.add_to_list exitnode guardnode |>
NodeMap.add_to_list guardnode cfgterminal;
input_val = prevcfg.input_val;
input_output_var = prevcfg.input_output_var;
initial = Some guardnode;
terminal = Some exitnode;
content = bodyincrement.content |>
NodeMap.add_to_list guardnode (SimpleGuard (convertedguard)) |>
NodeMap.add_to_list exitnode (SimpleSkip)
} |> SSCfg.concat prevassignment
and convert_b (prg: Types.b_exp) : SimpleStatements.simpleBoolean =
match prg with
| Boolean (b) -> SimpleBoolean b
| BAnd (b1, b2) -> SimpleBAnd (convert_b b1, convert_b b2)
| BOr (b1, b2) -> SimpleBOr (convert_b b1, convert_b b2)
| BNot (b) -> SimpleBNot (convert_b b)
| BCmp (a1, a2) -> SimpleBCmp (convert_a a1, convert_a a2)
| BCmpLess (a1, a2) -> SimpleBCmpLess (convert_a a1, convert_a a2)
| BCmpLessEq (a1, a2) -> SimpleBCmpLessEq (convert_a a1, convert_a a2)
| BCmpGreater (a1, a2) -> SimpleBCmpGreater (convert_a a1, convert_a a2)
| BCmpGreaterEq (a1, a2) -> SimpleBCmpGreaterEq (convert_a a1, convert_a a2)
and convert_a (prg: Types.a_exp) : SimpleStatements.simpleArithmetic =
match prg with
| Variable x -> SimpleVariable x
| Integer n -> SimpleInteger n
| Plus (a1, a2) -> SimplePlus (convert_a a1, convert_a a2)
| Minus (a1, a2) -> SimpleMinus (convert_a a1, convert_a a2)
| Times (a1, a2) -> SimpleTimes (convert_a a1, convert_a a2)
| Division (a1, a2) -> SimpleDivision (convert_a a1, convert_a a2)
| Modulo (a1, a2) -> SimpleModulo (convert_a a1, convert_a a2)
| Power (a1, a2) -> SimplePower (convert_a a1, convert_a a2)
| PowerMod (_) -> failwith "Cannot convert PowerMod into Simple Instruction"
| Rand (a) -> SimpleRand (convert_a a)
let convert (prg: Types.p_exp) : SSCfg.t =
let prg = ReplacePowerMod.rewrite_instructions prg in
match prg with
| Main (i, o, exp) ->
{(convert_c SSCfg.empty exp) with input_output_var = Some (i, o)}
let convert_io (i: int) (prg: Types.p_exp) : SSCfg.t =
let prg = ReplacePowerMod.rewrite_instructions prg in
{(convert prg) with input_val = Some i}

36
lib/miniImp/CfgImp.mli Normal file
View File

@ -0,0 +1,36 @@
open Analysis
module SimpleStatements : sig
type t =
| SimpleSkip
| SimpleAssignment of Types.variable * simpleArithmetic
| SimpleGuard of simpleBoolean
and simpleBoolean =
| SimpleBoolean of bool
| SimpleBAnd of simpleBoolean * simpleBoolean
| SimpleBOr of simpleBoolean * simpleBoolean
| SimpleBNot of simpleBoolean
| SimpleBCmp of simpleArithmetic * simpleArithmetic
| SimpleBCmpLess of simpleArithmetic * simpleArithmetic
| SimpleBCmpLessEq of simpleArithmetic * simpleArithmetic
| SimpleBCmpGreater of simpleArithmetic * simpleArithmetic
| SimpleBCmpGreaterEq of simpleArithmetic * simpleArithmetic
and simpleArithmetic =
| SimpleVariable of Types.variable
| SimpleInteger of int
| SimplePlus of simpleArithmetic * simpleArithmetic
| SimpleMinus of simpleArithmetic * simpleArithmetic
| SimpleTimes of simpleArithmetic * simpleArithmetic
| SimpleDivision of simpleArithmetic * simpleArithmetic
| SimpleModulo of simpleArithmetic * simpleArithmetic
| SimplePower of simpleArithmetic * simpleArithmetic
| SimpleRand of simpleArithmetic
val pp : out_channel -> t -> unit
val pp_list : out_channel -> t list -> unit
end
module SSCfg : Cfg.C with type elt = SimpleStatements.t
val convert : Types.p_exp -> SSCfg.t
val convert_io : int -> Types.p_exp -> SSCfg.t

975
lib/miniImp/CfgRISC.ml Normal file
View File

@ -0,0 +1,975 @@
open Analysis
module RISCSimpleStatements = struct
type register = {
index: string
}
type t =
| Nop
| BRegOp of brop * register * register * register
| BImmOp of biop * register * int * register
| URegOp of urop * register * register
| Load of register * register
| LoadI of int * register
| Store of register * register
and brop =
| Add
| Sub
| Mult
| Div
| Mod
| Pow
| And
| Or
| Eq
| Less
| LessEq
| More
| MoreEq
and biop =
| AddI
| SubI
| MultI
| DivI
| ModI
| PowI
| AndI
| OrI
| EqI
| LessI
| LessEqI
| MoreI
| MoreEqI
and urop =
| Not
| Copy
| Rand
let pp (ppf: out_channel) (v: t) : unit =
let rec pp_t (ppf: out_channel) (v: t) : unit =
match v with
Nop ->
Printf.fprintf ppf "Nop"
| BRegOp (b, r1, r2, r3) ->
Printf.fprintf ppf "%a r%s r%s => r%s"
pp_brop b r1.index r2.index r3.index
| BImmOp (b, r1, i, r3) ->
Printf.fprintf ppf "%a r%s %d => r%s" pp_biop b r1.index i r3.index
| URegOp (u, r1, r2) ->
Printf.fprintf ppf "%a r%s => r%s" pp_urop u r1.index r2.index
| Load (r1, r2) ->
Printf.fprintf ppf "Load r%s => r%s" r1.index r2.index
| LoadI (i, r2) ->
Printf.fprintf ppf "LoadI %d => r%s" i r2.index
| Store (r1, r2) ->
Printf.fprintf ppf "Store r%s => r%s" r1.index r2.index
and pp_brop (ppf: out_channel) (v: brop) : unit =
match v with
Add -> Printf.fprintf ppf "Add"
| Sub -> Printf.fprintf ppf "Sub"
| Mult -> Printf.fprintf ppf "Mult"
| Div -> Printf.fprintf ppf "Div"
| Mod -> Printf.fprintf ppf "Mod"
| Pow -> Printf.fprintf ppf "Pow"
| And -> Printf.fprintf ppf "And"
| Or -> Printf.fprintf ppf "Or"
| Eq -> Printf.fprintf ppf "Eq"
| Less -> Printf.fprintf ppf "Less"
| LessEq -> Printf.fprintf ppf "LessEq"
| More -> Printf.fprintf ppf "More"
| MoreEq -> Printf.fprintf ppf "MoreEq"
and pp_biop (ppf: out_channel) (v: biop) : unit =
match v with
AddI -> Printf.fprintf ppf "AddI"
| SubI -> Printf.fprintf ppf "SubI"
| MultI -> Printf.fprintf ppf "MultI"
| DivI -> Printf.fprintf ppf "DivI"
| ModI -> Printf.fprintf ppf "ModI"
| PowI -> Printf.fprintf ppf "PowI"
| AndI -> Printf.fprintf ppf "AndI"
| OrI -> Printf.fprintf ppf "OrI"
| EqI -> Printf.fprintf ppf "EqI"
| LessI -> Printf.fprintf ppf "LessI"
| LessEqI -> Printf.fprintf ppf "LessEqI"
| MoreI -> Printf.fprintf ppf "MoreI"
| MoreEqI -> Printf.fprintf ppf "MoreEqI"
and pp_urop (ppf: out_channel) (v: urop) : unit =
match v with
Not -> Printf.fprintf ppf "Nop"
| Copy -> Printf.fprintf ppf "Copy"
| Rand -> Printf.fprintf ppf "Rand"
in
pp_t ppf v
let pp_list (ppf: out_channel) (l: t list) : unit =
List.iter (fun x -> pp ppf x; Printf.printf "; ") l
end
module RISCCfg = Cfg.Make(RISCSimpleStatements)
let globalcounter = ref 0
module RegisterMap = struct
type m = {
assignments: RISCSimpleStatements.register Types.VariableMap.t
}
let set_register (x: Types.variable) (v: RISCSimpleStatements.register) (m: m)
: m =
{assignments = Types.VariableMap.add x v m.assignments}
let get_or_set_register (x: Types.variable) (m: m)
: RISCSimpleStatements.register * m =
match Types.VariableMap.find_opt x m.assignments with
None -> (
globalcounter := !globalcounter + 1;
({index = string_of_int !globalcounter},
{assignments =
Types.VariableMap.add x
({index = (string_of_int !globalcounter)}
: RISCSimpleStatements.register)
m.assignments}))
| Some i -> (i, m)
let get_fresh_register (m: m)
: RISCSimpleStatements.register * m * Types.variable =
globalcounter := !globalcounter + 1;
let freshvariable = string_of_int !globalcounter in
({index = string_of_int !globalcounter},
{assignments =
Types.VariableMap.add freshvariable
({index = string_of_int !globalcounter}
: RISCSimpleStatements.register)
m.assignments},
freshvariable)
let empty : m =
{assignments = Types.VariableMap.empty}
end
(* converts a simple statement into RISC simple statements *)
let rec c_ss_t
(ss: CfgImp.SimpleStatements.t)
(m: RegisterMap.m)
(convertedcode: RISCSimpleStatements.t list)
: RISCSimpleStatements.t list * RegisterMap.m =
match ss with
SimpleSkip -> (convertedcode @ [Nop], m)
| SimpleAssignment (v, sa) -> (
let r1, m = RegisterMap.get_or_set_register v m in
c_ss_sa sa m convertedcode r1
)
| SimpleGuard (b) -> (
let returnreg, m, _returnregvar = RegisterMap.get_fresh_register m in
c_ss_sb b m convertedcode returnreg
)
(* converts a boolean simple statement into RISC simple statements, requires
the register where the result sould be put into, does a lookahead to optimize
with operations where an integer is one side of the operation *)
and c_ss_sb
(ss: CfgImp.SimpleStatements.simpleBoolean)
(m: RegisterMap.m)
(convertedcode: RISCSimpleStatements.t list)
(register: RISCSimpleStatements.register)
: RISCSimpleStatements.t list * RegisterMap.m =
match ss with
SimpleBoolean (b) -> (
let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
if b then
(convertedcode @ [LoadI (1, partialresreg)], m)
else
(convertedcode @ [LoadI (0, partialresreg)], m)
)
| SimpleBAnd (b1, b2) -> (
match (b1, b2) with
| (SimpleBoolean (true), b)
| (b, SimpleBoolean (true)) -> (
c_ss_sb b m convertedcode register
)
| (SimpleBoolean (false), _)
| (_, SimpleBoolean (false)) -> (
(convertedcode @ [LoadI (0, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sb b1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sb b2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (And, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleBOr (b1, b2) -> (
match (b1, b2) with
| (SimpleBoolean (false), b)
| (b, SimpleBoolean (false)) -> (
c_ss_sb b m convertedcode register
)
| (SimpleBoolean (true), _)
| (_, SimpleBoolean (true)) -> (
(LoadI (1, register) :: convertedcode, m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sb b1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sb b2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (Or, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleBNot (b) -> (
match (b) with
| SimpleBoolean (b) -> (
if b then
(LoadI (0, register) :: convertedcode, m)
else
(LoadI (1, register) :: convertedcode, m)
)
| _ -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sb b m convertedcode partialresreg in
(convertedcode @ [URegOp (Not, partialresreg, register)], m)
)
)
| SimpleBCmp (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x))
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (EqI, xreg, i, register)], m)
)
| (SimpleInteger (i), a)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (EqI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (Eq, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a)
| (a, SimpleVariable (x)) -> (
let xreg, m =
RegisterMap.get_or_set_register x m
in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Eq, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (Eq, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleBCmpLess (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (MoreI, xreg, i, register)], m)
)
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (LessI, xreg, i, register)], m)
)
| (SimpleInteger (i), a) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (MoreI, partialresreg, i, register)], m)
)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (LessI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (Less, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Less, xreg, partialresreg, register)], m)
)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Less, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (Less, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleBCmpLessEq (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (MoreEqI, xreg, i, register)], m)
)
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (LessEqI, xreg, i, register)], m)
)
| (SimpleInteger (i), a) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (MoreEqI, partialresreg, i, register)], m)
)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (LessEqI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (LessEq, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (LessEq, xreg, partialresreg, register)], m)
)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (LessEq, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (LessEq, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleBCmpGreater (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (LessI, xreg, i, register)], m)
)
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (MoreI, xreg, i, register)], m)
)
| (SimpleInteger (i), a) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (LessI, partialresreg, i, register)], m)
)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (MoreI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (More, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (More, xreg, partialresreg, register)], m)
)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (More, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (More, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleBCmpGreaterEq (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (LessEqI, xreg, i, register)], m)
)
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (MoreEqI, xreg, i, register)], m)
)
| (SimpleInteger (i), a) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (LessEqI, partialresreg, i, register)], m)
)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (MoreEqI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (MoreEq, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (MoreEq, xreg, partialresreg, register)], m)
)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (MoreEq, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (MoreEq, partialresreg1, partialresreg2, register)], m)
)
)
(* converts a arithmetic simple statement into RISC simple statements, requires
the register where the result sould be put into, does a lookahead to optimize
with operations where an integer is one side of the operation *)
and c_ss_sa
(ss: CfgImp.SimpleStatements.simpleArithmetic)
(m: RegisterMap.m)
(convertedcode: RISCSimpleStatements.t list)
(register: RISCSimpleStatements.register)
: RISCSimpleStatements.t list * RegisterMap.m =
match ss with
SimpleVariable (x) -> (
let r1, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [URegOp (Copy, r1, register)], m)
)
| SimpleInteger (i) -> (
(convertedcode @ [LoadI (i, register)], m)
)
| SimplePlus (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x))
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (AddI, xreg, i, register)], m)
)
| (SimpleInteger (i), a)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (AddI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (Add, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Add, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (Add, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleMinus (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
(convertedcode @
[LoadI (i, partialresreg);
BRegOp (Sub, partialresreg, xreg, register)], m)
)
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (SubI, xreg, i, register)], m)
)
| (SimpleInteger (i), a) -> (
let partialresregi, m, _partialresvari =
RegisterMap.get_fresh_register m
in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @
[LoadI (i, partialresregi);
BRegOp (Sub, partialresregi, partialresreg, register)], m)
)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (SubI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (Sub, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Sub, xreg, partialresreg, register)], m)
)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Sub, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (Sub, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleTimes (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x))
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (MultI, xreg, i, register)], m)
)
| (SimpleInteger (i), a)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (MultI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (Mult, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Mult, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (Mult, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleDivision (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
(convertedcode @
[LoadI (i, partialresreg);
BRegOp (Div, partialresreg, xreg, register)], m)
)
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (DivI, xreg, i, register)], m)
)
| (SimpleInteger (i), a) -> (
let partialresregi, m, _partialresvari =
RegisterMap.get_fresh_register m
in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @
[LoadI (i, partialresregi);
BRegOp (Div, partialresregi, partialresreg, register)], m)
)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (DivI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (Div, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Div, xreg, partialresreg, register)], m)
)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Div, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (Div, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleModulo (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
(convertedcode @
[LoadI (i, partialresreg);
BRegOp (Mod, partialresreg, xreg, register)], m)
)
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (ModI, xreg, i, register)], m)
)
| (SimpleInteger (i), a) -> (
let partialresregi, m, _partialresvari =
RegisterMap.get_fresh_register m
in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @
[LoadI (i, partialresregi);
BRegOp (Mod, partialresregi, partialresreg, register)], m)
)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (ModI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (Mod, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Mod, xreg, partialresreg, register)], m)
)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Mod, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (Mod, partialresreg1, partialresreg2, register)], m)
)
)
| SimplePower (a1, a2) -> (
match (a1, a2) with
| (SimpleInteger (i), SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
(convertedcode @
[LoadI (i, partialresreg);
BRegOp (Pow, partialresreg, xreg, register)], m)
)
| (SimpleVariable (x), SimpleInteger (i)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [BImmOp (PowI, xreg, i, register)], m)
)
| (SimpleInteger (i), a) -> (
let partialresregi, m, _partialresvari =
RegisterMap.get_fresh_register m
in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @
[LoadI (i, partialresregi);
BRegOp (Pow, partialresregi, partialresreg, register)], m)
)
| (a, SimpleInteger (i)) -> (
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BImmOp (PowI, partialresreg, i, register)], m)
)
| (SimpleVariable (x), SimpleVariable (y)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let yreg, m = RegisterMap.get_or_set_register y m in
(convertedcode @ [BRegOp (Pow, xreg, yreg, register)], m)
)
| (SimpleVariable (x), a) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Pow, xreg, partialresreg, register)], m)
)
| (a, SimpleVariable (x)) -> (
let xreg, m = RegisterMap.get_or_set_register x m in
let partialresreg, m, _partialresvar =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [BRegOp (Pow, partialresreg, xreg, register)], m)
)
| (_, _) -> (
let partialresreg1, m, _partialresvar1 =
RegisterMap.get_fresh_register m
in
let partialresreg2, m, _partialresvar2 =
RegisterMap.get_fresh_register m
in
let convertedcode, m = c_ss_sa a1 m convertedcode partialresreg1 in
let convertedcode, m = c_ss_sa a2 m convertedcode partialresreg2 in
(convertedcode @
[BRegOp (Pow, partialresreg1, partialresreg2, register)], m)
)
)
| SimpleRand (a) -> (
let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
(convertedcode @ [URegOp (Rand, partialresreg, register)], m)
)
let convert_ss
(m: RegisterMap.m)
(value: CfgImp.SimpleStatements.t list)
(node: Cfg.Node.t)
(risccode: RISCSimpleStatements.t list Cfg.NodeMap.t)
: RISCSimpleStatements.t list Cfg.NodeMap.t * RegisterMap.m =
(* we iterate over the list of simple statements and convert each operation to
the equivalent three address operations, we need to propagate the
association between variables and registers so we choose a fold instead of
a mapreduce *)
let instructions, m = List.fold_left
(fun (convertedcode, m) code -> c_ss_t code m convertedcode)
([], m) value
in
(Cfg.NodeMap.add node instructions risccode, m)
let helper_convert
(c: CfgImp.SimpleStatements.t list Cfg.NodeMap.t)
(m: RegisterMap.m)
: RISCSimpleStatements.t list Cfg.NodeMap.t =
(* *)
(* we use NodeMap.fold since order is not important, we assume that every
has an associated register and we ignore use before assignment errors *)
let risccode, _ = Cfg.NodeMap.fold
(fun node value (risccode, m) -> convert_ss m value node risccode)
c (Cfg.NodeMap.empty, m)
in
risccode
let convert (prg: CfgImp.SSCfg.t) : RISCCfg.t =
let ({ empty: bool;
nodes: Cfg.NodeSet.t;
edges: (Cfg.Node.t * (Cfg.Node.t option)) Cfg.NodeMap.t;
reverse_edges: (Cfg.Node.t list) Cfg.NodeMap.t;
input_val: int option;
input_output_var: (string * string) option;
initial: Cfg.Node.t option;
terminal: Cfg.Node.t option;
content: CfgImp.SimpleStatements.t list Cfg.NodeMap.t
}: CfgImp.SSCfg.t) = prg
in
let initial_bindings =
match input_output_var with
| Some (i, o) -> (
if i = o then
RegisterMap.empty |>
RegisterMap.set_register i {index = "in"}
else
RegisterMap.empty |>
RegisterMap.set_register i {index = "in"} |>
RegisterMap.set_register o {index = "out"}
)
| None ->
RegisterMap.empty
in
{ empty = empty;
nodes = nodes;
edges = edges;
reverse_edges = reverse_edges;
input_val = input_val;
input_output_var = (
match input_output_var with
| Some (i, o) -> (
if i = o then
Some ("in", "in")
else
Some ("in", "out")
)
| None -> Some ("in", "out")
);
initial = initial;
terminal = terminal;
content = helper_convert content initial_bindings;
}

55
lib/miniImp/CfgRISC.mli Normal file
View File

@ -0,0 +1,55 @@
open Analysis
module RISCSimpleStatements : sig
type register = {
index: string
}
type t =
| Nop
| BRegOp of brop * register * register * register
| BImmOp of biop * register * int * register
| URegOp of urop * register * register
| Load of register * register
| LoadI of int * register
| Store of register * register
and brop =
| Add
| Sub
| Mult
| Div
| Mod
| Pow
| And
| Or
| Eq
| Less
| LessEq
| More
| MoreEq
and biop =
| AddI
| SubI
| MultI
| DivI
| ModI
| PowI
| AndI
| OrI
| EqI
| LessI
| LessEqI
| MoreI
| MoreEqI
and urop =
| Not
| Copy
| Rand
val pp : out_channel -> t -> unit
val pp_list : out_channel -> t list -> unit
end
module RISCCfg : Cfg.C with type elt = RISCSimpleStatements.t
val convert : CfgImp.SSCfg.t -> RISCCfg.t

2
lib/miniImp/Parser.mly
View File

@ -32,7 +32,7 @@
%left DIVISION
%left MODULO
%left TIMES
%left POWER
%right POWER
%left DO
%%

344
lib/miniImp/RISC.ml Normal file
View File

@ -0,0 +1,344 @@
open Analysis
let globalCounterLabel = ref 0
let nextLabel () : string =
globalCounterLabel := !globalCounterLabel + 1;
"l" ^ (string_of_int !globalCounterLabel)
module RISCAssembly = struct
type register = {
index : string
}
type label = string
type risci =
| Nop
| BRegOp of brop * register * register * register
| BImmOp of biop * register * int * register
| URegOp of urop * register * register
| Load of register * register
| LoadI of int * register
| Store of register * register
| Jump of label
| CJump of register * label * label
| Label of label
and brop =
| Add
| Sub
| Mult
| Div
| Mod
| Pow
| And
| Or
| Eq
| Less
| LessEq
| More
| MoreEq
and biop =
| AddI
| SubI
| MultI
| DivI
| ModI
| PowI
| AndI
| OrI
| EqI
| LessI
| LessEqI
| MoreI
| MoreEqI
and urop =
| Not
| Copy
| Rand
type t = {
code : risci list;
inputval: int option;
inputoutputreg: (register * register) option;
}
let pp_risci (ppf: out_channel) (v: risci) : unit =
let rec pp_risci (ppf: out_channel) (v: risci) : unit =
match v with
| Nop ->
Printf.fprintf ppf "\tNop\n"
| BRegOp (b, r1, r2, r3) ->
Printf.fprintf ppf "\t%a r%s r%s => r%s\n"
pp_brop b r1.index r2.index r3.index
| BImmOp (b, r1, i, r3) ->
Printf.fprintf ppf "\t%a r%s %d => r%s\n" pp_biop b r1.index i r3.index
| URegOp (u, r1, r2) ->
Printf.fprintf ppf "\t%a r%s => r%s\n" pp_urop u r1.index r2.index
| Load (r1, r2) ->
Printf.fprintf ppf "\tLoad r%s => r%s\n" r1.index r2.index
| LoadI (i, r2) ->
Printf.fprintf ppf "\tLoadI %d => r%s\n" i r2.index
| Store (r1, r2) ->
Printf.fprintf ppf "\tStore r%s => r%s\n" r1.index r2.index
| Jump (label) ->
Printf.fprintf ppf "\tJump %s\n" label
| CJump (r, l1, l2) ->
Printf.fprintf ppf "\tCJump r%s => %s, %s\n" r.index l1 l2
| Label (label) ->
Printf.fprintf ppf "%s:" label
and pp_brop (ppf: out_channel) (v: brop) : unit =
match v with
Add -> Printf.fprintf ppf "Add"
| Sub -> Printf.fprintf ppf "Sub"
| Mult -> Printf.fprintf ppf "Mult"
| Div -> Printf.fprintf ppf "Div"
| Mod -> Printf.fprintf ppf "Mod"
| Pow -> Printf.fprintf ppf "Pow"
| And -> Printf.fprintf ppf "And"
| Or -> Printf.fprintf ppf "Or"
| Eq -> Printf.fprintf ppf "Eq"
| Less -> Printf.fprintf ppf "Less"
| LessEq -> Printf.fprintf ppf "LessEq"
| More -> Printf.fprintf ppf "More"
| MoreEq -> Printf.fprintf ppf "MoreEq"
and pp_biop (ppf: out_channel) (v: biop) : unit =
match v with
AddI -> Printf.fprintf ppf "AddI"
| SubI -> Printf.fprintf ppf "SubI"
| MultI -> Printf.fprintf ppf "MultI"
| DivI -> Printf.fprintf ppf "DivI"
| ModI -> Printf.fprintf ppf "ModI"
| PowI -> Printf.fprintf ppf "PowI"
| AndI -> Printf.fprintf ppf "AndI"
| OrI -> Printf.fprintf ppf "OrI"
| EqI -> Printf.fprintf ppf "EqI"
| LessI -> Printf.fprintf ppf "LessI"
| LessEqI -> Printf.fprintf ppf "LessEqI"
| MoreI -> Printf.fprintf ppf "MoreI"
| MoreEqI -> Printf.fprintf ppf "MoreEqI"
and pp_urop (ppf: out_channel) (v: urop) : unit =
match v with
Not -> Printf.fprintf ppf "Nop"
| Copy -> Printf.fprintf ppf "Copy"
| Rand -> Printf.fprintf ppf "Rand"
in
pp_risci ppf v
let pp (ppf: out_channel) (t: t) : unit =
Printf.fprintf ppf "Input Val: ";
( match t.inputval with
None -> Printf.fprintf ppf "None\n"
| Some i -> Printf.fprintf ppf "Some %d\n" i );
Printf.fprintf ppf "Input/Output Registers: ";
( match t.inputoutputreg with
| None ->
Printf.fprintf ppf "None\n"
| Some (i, o) ->
Printf.fprintf ppf "[i: Some r%s, o: Some r%s]\n" i.index o.index);
Printf.fprintf ppf "Code:\n";
List.iter (pp_risci ppf) t.code
end
let convert_cfgrisc_risci (i: CfgRISC.RISCSimpleStatements.t list) :
(RISCAssembly.risci list) =
let rec aux (i: CfgRISC.RISCSimpleStatements.t)
: RISCAssembly.risci =
match i with
| Nop -> Nop
| BRegOp (brop, r1, r2, r3) -> BRegOp (aux_brop brop,
{index = r1.index},
{index = r2.index},
{index = r3.index})
| BImmOp (biop, r1, imm, r3) -> BImmOp (aux_biop biop,
{index = r1.index},
imm,
{index = r3.index})
| URegOp (urop, r1, r3) -> URegOp (aux_urop urop,
{index = r1.index},
{index = r3.index})
| Load (r1, r3) -> Load ({index = r1.index},
{index = r3.index})
| LoadI (imm, r3) -> LoadI (imm,
{index = r3.index})
| Store (r1, r3) -> Store ({index = r1.index},
{index = r3.index})
and aux_brop (brop: CfgRISC.RISCSimpleStatements.brop)
: RISCAssembly.brop =
match brop with
| Add -> Add
| Sub -> Sub
| Mult -> Mult
| Div -> Div
| Mod -> Mod
| Pow -> Pow
| And -> And
| Or -> Or
| Eq -> Eq
| Less -> Less
| LessEq -> LessEq
| More -> More
| MoreEq -> MoreEq
and aux_biop (biop: CfgRISC.RISCSimpleStatements.biop)
: RISCAssembly.biop =
match biop with
| AddI -> AddI
| SubI -> SubI
| MultI -> MultI
| DivI -> DivI
| ModI -> ModI
| PowI -> PowI
| AndI -> AndI
| OrI -> OrI
| EqI -> EqI
| LessI -> LessI
| LessEqI -> LessEqI
| MoreI -> MoreI
| MoreEqI -> MoreEqI
and aux_urop (urop: CfgRISC.RISCSimpleStatements.urop)
: RISCAssembly.urop =
match urop with
| Not -> Not
| Copy -> Copy
| Rand -> Rand
in
List.map aux i
let next_common_successor
(prg: CfgRISC.RISCCfg.t)
(node1: Cfg.Node.t)
(node2: Cfg.Node.t)
: Cfg.Node.t option =
(* Assume the two input nodes are the two branches of an if then else
statement, then create the two lists that represent the runs until the
terminal node by choosing always the false statement in guard statements
(if the guard is for a while statement it gets ignored, if it is for an
if then else it chooses one of the branches) then find the first common
node in the lists
*)
let rec walk (node: Cfg.Node.t) : Cfg.Node.t list =
node :: match Cfg.NodeMap.find_opt node prg.edges with
| None -> []
| Some (edge, None) -> (walk edge)
| Some (_, Some edge) -> (walk edge)
in
let list1 = walk node1 in
let list2 = walk node2 in
let common = List.filter (fun x -> List.mem x list2) list1 in
match common with
[] -> None
| a::_ -> Some a
let rec helper_convert
(prg: CfgRISC.RISCCfg.t)
(current_node: Cfg.Node.t)
(already_visited: Cfg.Node.t list)
: (RISCAssembly.risci list) * (Cfg.Node.t list) =
(* takes the program, the current node and a list of already visited nodes to
compute the linearized three address instructions and the list of
previoulsy visited nodes plus the newly visited nodes. Stops as soon if
node has already been visited or if no nodes are next *)
if List.mem current_node already_visited then
([], already_visited)
else (
let nextnodes = (Cfg.NodeMap.find_opt current_node prg.edges) in
let currentcode =
(match (Cfg.NodeMap.find_opt current_node prg.content) with
| None -> []
| Some x -> convert_cfgrisc_risci x)
in
match nextnodes with
| Some (nextnode1, None) ->
let res, vis =
helper_convert
prg
nextnode1
(current_node :: already_visited)
in
(currentcode @ res, vis)
| Some (nextnode1, Some nextnode2) -> (
let ncs = next_common_successor prg nextnode1 nextnode2 in
match ncs with
| None -> (* should never happen since the terminal node should always be
rechable *)
failwith "Topology got a little mixed up"
| Some ncs -> (
if (ncs.id = nextnode2.id)
then (* while or for loop, three labels are necessary *)
let label1 = nextLabel () in
let label2 = nextLabel () in
let label3 = nextLabel () in
let res1, _ =
(helper_convert prg nextnode1
(current_node :: nextnode2 :: already_visited)) in
let res2, vis2 =
(helper_convert prg nextnode2
(current_node :: nextnode1 :: already_visited)) in
match List.nth currentcode ((List.length currentcode) - 1) with
| BRegOp (_, _, _, r)
| BImmOp (_, _, _, r)
| URegOp (_, _, r)
| Load (_, r)
| Store (r, _)
| LoadI (_, r) -> (([Label label1]
: RISCAssembly.risci list) @
currentcode @
([CJump (r, label2, label3); Label label2]
: RISCAssembly.risci list) @
res1 @
([Jump label1; Label label3]
: RISCAssembly.risci list) @
res2
, vis2)
| _ -> failwith "Missing instruction at branch"
else (* if branches, three labels are necessary *)
let label1 = nextLabel () in
let label2 = nextLabel () in
let label3 = nextLabel () in
let res1, vis1 =
helper_convert
prg
nextnode1
(current_node :: ncs :: already_visited)
in
let res2, _ = helper_convert prg nextnode2 vis1 in
let res3, vis3 =
helper_convert prg ncs (current_node :: already_visited)
in
match List.nth currentcode ((List.length currentcode) - 1) with
| BRegOp (_, _, _, r)
| BImmOp (_, _, _, r)
| URegOp (_, _, r)
| Load (_, r)
| Store (r, _)
| LoadI (_, r) -> (currentcode @
([CJump (r, label1, label2); Label label1]
: RISCAssembly.risci list) @
res1 @
([Jump label3; Label label2]
: RISCAssembly.risci list) @
res2 @
([Label label3]
: RISCAssembly.risci list) @
res3
, vis3)
| _ -> failwith "Missing instruction at branch"
)
)
| None -> (currentcode, current_node :: already_visited)
)
let convert (prg: CfgRISC.RISCCfg.t) : RISCAssembly.t =
{code = (helper_convert prg (Option.get prg.initial) [] |> fst |>
List.append ([Label "main"] : RISCAssembly.risci list));
inputval = prg.input_val;
inputoutputreg =
match prg.input_output_var with
None -> None
| Some (i, o) -> Some ({index = i}, {index = o})
}

61
lib/miniImp/RISC.mli Normal file
View File

@ -0,0 +1,61 @@
module RISCAssembly : sig
type register = {
index : string
}
type label = string
type risci =
| Nop
| BRegOp of brop * register * register * register
| BImmOp of biop * register * int * register
| URegOp of urop * register * register
| Load of register * register
| LoadI of int * register
| Store of register * register
| Jump of label
| CJump of register * label * label
| Label of label
and brop =
| Add
| Sub
| Mult
| Div
| Mod
| Pow
| And
| Or
| Eq
| Less
| LessEq
| More
| MoreEq
and biop =
| AddI
| SubI
| MultI
| DivI
| ModI
| PowI
| AndI
| OrI
| EqI
| LessI
| LessEqI
| MoreI
| MoreEqI
and urop =
| Not
| Copy
| Rand
type t = {
code : risci list;
inputval: int option;
inputoutputreg: (register * register) option;
}
val pp_risci : out_channel -> risci -> unit
val pp : out_channel -> t -> unit
end
val convert : CfgRISC.RISCCfg.t -> RISCAssembly.t

226
lib/miniImp/RISCSemantics.ml Normal file
View File

@ -0,0 +1,226 @@
module Register = struct
type t = {index: string}
let compare a b = compare a.index b.index
end
module CodeMap = Map.Make(String)
module RegisterMap = Map.Make(Register)
module MemoryMap = Map.Make(Int)
module RISCArchitecture = struct
type t = {
code: RISC.RISCAssembly.risci list CodeMap.t;
registers: int RegisterMap.t;
memory: int MemoryMap.t;
outputreg: Register.t;
}
end
let convert (prg: RISC.RISCAssembly.t)
: RISC.RISCAssembly.risci list CodeMap.t =
(* takes as input a sequence of RISC commands and computes a map to the right
labels for easier execution *)
let rec aux
(prg: RISC.RISCAssembly.risci list)
(current: RISC.RISCAssembly.risci list)
(current_label: string)
(map: RISC.RISCAssembly.risci list CodeMap.t)
: (RISC.RISCAssembly.risci list CodeMap.t) =
match prg with
| [] -> (CodeMap.union
(fun _ _ _ -> failwith "Two labels are the same")
(CodeMap.singleton current_label current)
map)
| Label l :: tl -> aux tl ([]) l
(CodeMap.union
(fun _ _ _ -> failwith "Two labels are the same")
(CodeMap.singleton current_label current)
map)
| instr :: tl -> aux tl (current @ [instr]) current_label map
in
match prg.code with
| Label "main" :: tl -> aux tl [] "main" CodeMap.empty
| _ -> failwith "Program should begind with label main"
let label_order (prg: RISC.RISCAssembly.t) : string list =
let rec aux
(prg: RISC.RISCAssembly.risci list)
: string list =
match prg with
[] -> []
| Label l :: tl -> l :: (aux tl)
| _ :: tl -> (aux tl)
in
aux (prg.code)
let reduce_instructions (prg: RISCArchitecture.t) (lo: string list) : int =
let match_operator_r (brop: RISC.RISCAssembly.brop) =
match brop with
| Add -> (+)
| Sub -> (-)
| Mult -> ( * )
| Div -> (/)
| Mod -> (mod)
| Pow -> (Utility.pow)
| And -> (Utility.int_and)
| Or -> (Utility.int_or)
| Eq -> (Utility.int_eq)
| Less -> (Utility.int_less)
| LessEq -> (Utility.int_less_eq)
| More -> (Utility.int_more)
| MoreEq -> (Utility.int_more_eq)
in
let match_operator_i (biop: RISC.RISCAssembly.biop) =
match biop with
| AddI -> (+)
| SubI -> (-)
| MultI -> ( * )
| DivI -> (/)
| ModI -> (mod)
| PowI -> (Utility.pow)
| AndI -> (Utility.int_and)
| OrI -> (Utility.int_or)
| EqI -> (Utility.int_eq)
| LessI -> (Utility.int_less)
| LessEqI -> (Utility.int_less_eq)
| MoreI -> (Utility.int_more)
| MoreEqI -> (Utility.int_more_eq)
in
let rec aux
(prg: RISCArchitecture.t)
(current: RISC.RISCAssembly.risci list)
(current_label: string)
: RISCArchitecture.t =
match current with
| [] -> (
(* falls to the next label *)
match List.find_index ((=) current_label) lo with
None -> prg (* should never happen *)
| Some i ->
if i + 1 < (List.length lo) then
aux
prg
(CodeMap.find (List.nth lo (i+1)) prg.code)
(List.nth lo (i+1))
else
prg
)
| Nop :: tl ->
aux prg tl current_label
| BRegOp (brop, r1, r2, r3) :: tl -> (
let n = (match_operator_r brop)
(RegisterMap.find {index = r1.index} prg.registers)
(RegisterMap.find {index = r2.index} prg.registers)
in
aux { prg with
registers = RegisterMap.add {index = r3.index} n prg.registers}
tl current_label
)
| BImmOp (biop, r1, i, r3) :: tl -> (
let n = (match_operator_i biop)
(RegisterMap.find {index = r1.index} prg.registers)
i
in
aux { prg with
registers = RegisterMap.add {index = r3.index} n prg.registers}
tl current_label
)
| URegOp (urop, r1, r3) :: tl -> (
match urop with
| Copy -> (
let n = RegisterMap.find {index = r1.index} prg.registers in
aux { prg with
registers =
RegisterMap.add {index = r3.index} n prg.registers }
tl current_label
)
| Not -> (
let n = Utility.int_not
(RegisterMap.find {index = r1.index} prg.registers)
in
aux { prg with
registers =
RegisterMap.add {index = r3.index} n prg.registers }
tl current_label
)
| Rand -> (
let n = Random.int
(RegisterMap.find {index = r1.index} prg.registers)
in
aux { prg with
registers =
RegisterMap.add {index = r3.index} n prg.registers }
tl current_label
)
)
| Load (r1, r3) :: tl -> (
let n =
MemoryMap.find
(RegisterMap.find {index = r1.index} prg.registers)
prg.memory
in
aux { prg with
registers = RegisterMap.add {index = r3.index} n prg.registers}
tl current_label
)
| LoadI (i, r3) :: tl -> (
let n = i
in
aux { prg with
registers = RegisterMap.add {index = r3.index} n prg.registers}
tl current_label
)
| Store (r1, r3) :: tl -> (
let n = RegisterMap.find {index = r1.index} prg.registers in
let n1 = RegisterMap.find {index = r3.index} prg.registers in
aux
{ prg with memory = MemoryMap.add n1 n prg.memory }
tl
current_label
)
| Jump l :: _ -> aux prg (CodeMap.find l prg.code) l
| CJump (r, l1, l2) :: _ -> (
let br = (RegisterMap.find {index = r.index} prg.registers) > 0 in
if br
then
aux prg (CodeMap.find l1 prg.code) l1
else
aux prg (CodeMap.find l2 prg.code) l2
)
| Label _ :: tl -> aux prg tl current_label
in
match
RegisterMap.find_opt
prg.outputreg
(aux prg (CodeMap.find "main" prg.code) "main").registers
with
Some x -> x
| None -> failwith "Output register not found"
let reduce (prg: RISC.RISCAssembly.t) : int =
(* takes assembly and execute it *)
reduce_instructions
{code = convert prg;
registers = (
match prg.inputoutputreg with
| None ->
RegisterMap.singleton
{index = "in"}
(Option.value prg.inputval ~default:0)
| Some (i, _) ->
RegisterMap.singleton
{index = i.index}
(Option.value prg.inputval ~default:0)
);
memory = MemoryMap.empty;
outputreg = (
match prg.inputoutputreg with
| None -> {index = "out"}
| Some (_, o) -> {index = o.index}
)
}
(label_order prg)

5
lib/miniImp/RISCSemantics.mli Normal file
View File

@ -0,0 +1,5 @@
module RISCArchitecture : sig
type t
end
val reduce : RISC.RISCAssembly.t -> int

20
lib/miniImp/Semantics.ml
View File

@ -53,8 +53,10 @@ and evaluate_a (mem: memory) (exp_a: a_exp) : (int, [> error]) result =
match exp_a with
Variable v -> (
match VariableMap.find_opt v mem.assignments with
None -> Error (`AbsentAssignment ("The variable " ^ v ^ " is not defined."))
| Some a -> Ok a
| None ->
Error (`AbsentAssignment ("The variable " ^ v ^ " is not defined."))
| Some a ->
Ok a
)
| Integer n -> Ok n
| Plus (exp_a1, exp_a2) -> (
@ -148,9 +150,13 @@ and evaluate_b (mem: memory) (exp_b: b_exp) : (bool, [> error]) result =
let reduce (program: p_exp) (iin : int) : (int, [> error]) result =
match program with
Main (vin, vout, expression) -> (
let mem : memory = {assignments = (VariableMap.empty |> VariableMap.add vin iin)} in
let* resultmem : memory = evaluate mem expression in
match VariableMap.find_opt vout resultmem.assignments with
None -> Error (`AbsentAssignment ("The output variable is not defined (" ^ vout ^ ")"))
| Some a -> Ok a
let mem : memory =
{ assignments = (VariableMap.empty |> VariableMap.add vin iin) } in
let* result_mem : memory = evaluate mem expression in
match VariableMap.find_opt vout result_mem.assignments with
| None ->
Error (`AbsentAssignment
("The output variable is not defined (" ^ vout ^ ")"))
| Some a ->
Ok a
)

120
lib/miniImp/Types.ml
View File

@ -1,36 +1,106 @@
type variable = string
type p_exp =
Main of variable * variable * c_exp (* def main with input x output y as c *)
Main of variable * variable * c_exp
(* def main with input x output y as c *)
and c_exp =
Skip
| Assignment of variable * a_exp (* x := a *)
| Sequence of c_exp * c_exp (* c; c *)
| If of b_exp * c_exp * c_exp (* if b then c else c *)
| While of b_exp * c_exp (* while b do c *)
| For of c_exp * b_exp * c_exp * c_exp (* for (c; b; c) do c *)
| Assignment of variable * a_exp (* x := a *)
| Sequence of c_exp * c_exp (* c; c *)
| If of b_exp * c_exp * c_exp (* if b then c else c *)
| While of b_exp * c_exp (* while b do c *)
| For of c_exp * b_exp * c_exp * c_exp
(* for (c; b; c) do c *)
and b_exp =
Boolean of bool (* v *)
| BAnd of b_exp * b_exp (* b && b *)
| BOr of b_exp * b_exp (* b || b *)
| BNot of b_exp (* not b *)
| BCmp of a_exp * a_exp (* a == a *)
| BCmpLess of a_exp * a_exp (* a < a *)
| BCmpLessEq of a_exp * a_exp (* a <= a *)
| BCmpGreater of a_exp * a_exp (* a > a *)
| BCmpGreaterEq of a_exp * a_exp (* a >= a *)
Boolean of bool (* v *)
| BAnd of b_exp * b_exp (* b && b *)
| BOr of b_exp * b_exp (* b || b *)
| BNot of b_exp (* not b *)
| BCmp of a_exp * a_exp (* a == a *)
| BCmpLess of a_exp * a_exp (* a < a *)
| BCmpLessEq of a_exp * a_exp (* a <= a *)
| BCmpGreater of a_exp * a_exp (* a > a *)
| BCmpGreaterEq of a_exp * a_exp (* a >= a *)
and a_exp =
Variable of variable (* x *)
| Integer of int (* n *)
| Plus of a_exp * a_exp (* a + a *)
| Minus of a_exp * a_exp (* a - a *)
| Times of a_exp * a_exp (* a * a *)
| Division of a_exp * a_exp (* a / a *)
| Modulo of a_exp * a_exp (* a % a *)
| Power of a_exp * a_exp (* a ^ a *)
| PowerMod of a_exp * a_exp * a_exp (* a ^ a % a *)
| Rand of a_exp (* rand(0, a) *)
Variable of variable (* x *)
| Integer of int (* n *)
| Plus of a_exp * a_exp (* a + a *)
| Minus of a_exp * a_exp (* a - a *)
| Times of a_exp * a_exp (* a * a *)
| Division of a_exp * a_exp (* a / a *)
| Modulo of a_exp * a_exp (* a % a *)
| Power of a_exp * a_exp (* a ^ a *)
| PowerMod of a_exp * a_exp * a_exp (* a ^ a % a *)
| Rand of a_exp (* rand(0, a) *)
let pp_p_exp (ppf: Format.formatter) (p: p_exp) : unit =
let open Format in
let rec helper_c (ppf) (c: c_exp) : unit =
match c with
| Skip ->
fprintf ppf "Skip"
| Assignment (x, a) ->
fprintf ppf "%S := @[<h>%a@]" x helper_a a
| Sequence (c1, c2) ->
fprintf ppf "@[<hv>Sequence (@;<1 2>%a,@;<1 0>%a@;<0 0>)@]"
helper_c c1 helper_c c2
| If (b, c1, c2) ->
fprintf ppf
"@[<hv>If @[<h>%a@]@;<1 2>then (@[<hv>%a@])@;<1 2>else (@[<hv>%a@])@]"
helper_b b helper_c c1 helper_c c2
| While (b, c) ->
fprintf ppf "@[<hv>While @[<h>%a@] do@;<1 2>%a@]@;<0 0>"
helper_b b helper_c c
| For (c1, b, c2, c3) ->
fprintf ppf
"@[<h>For (@;<0 2>%a,@;<1 2>@[<h>%a@],@;<1 2>%a) do@]@;<1 4>%a@;<0 0>"
helper_c c1 helper_b b helper_c c2 helper_c c3
and helper_b (ppf) (b: b_exp) =
match b with
| Boolean (b) ->
fprintf ppf "%b" b
| BAnd (b1, b2) ->
fprintf ppf "(%a &&@;<1 2>%a)" helper_b b1 helper_b b2
| BOr (b1, b2) ->
fprintf ppf "(%a ||@;<1 2>%a)" helper_b b1 helper_b b2
| BNot (b) ->
fprintf ppf "(not %a)" helper_b b
| BCmp (a1, a2) ->
fprintf ppf "(%a ==@;<1 2>%a)" helper_a a1 helper_a a2
| BCmpLess (a1, a2) ->
fprintf ppf "(%a <@;<1 2>%a)" helper_a a1 helper_a a2
| BCmpLessEq (a1, a2) ->
fprintf ppf "(%a <=@;<1 2>%a)" helper_a a1 helper_a a2
| BCmpGreater (a1, a2) ->
fprintf ppf "(%a >@;<1 2>%a)" helper_a a1 helper_a a2
| BCmpGreaterEq (a1, a2) ->
fprintf ppf "(%a >=@;<1 2>%a)" helper_a a1 helper_a a2
and helper_a (ppf) (a: a_exp) =
match a with
| Variable v ->
fprintf ppf "%S" v
| Integer n ->
fprintf ppf "%i" n
| Plus (a1, a2) ->
fprintf ppf "%a +@;<1 2>%a" helper_a a1 helper_a a2
| Minus (a1, a2) ->
fprintf ppf "%a -@;<1 2>%a" helper_a a1 helper_a a2
| Times (a1, a2) ->
fprintf ppf "%a *@;<1 2>%a" helper_a a1 helper_a a2
| Division (a1, a2) ->
fprintf ppf "%a /@;<1 2>%a" helper_a a1 helper_a a2
| Modulo (a1, a2) ->
fprintf ppf "%a %%@;<1 2>%a" helper_a a1 helper_a a2
| Power (a1, a2) ->
fprintf ppf "(%a ^@;<1 2>%a)" helper_a a1 helper_a a2
| PowerMod (a1, a2, a3) ->
fprintf ppf "(%a ^ %a %% %a)" helper_a a1 helper_a a2 helper_a a3
| Rand (a) ->
fprintf ppf "Rand (%a)" helper_a a
in
match p with
| Main (i, o, exp) ->
fprintf ppf "def main with (input %S) (output %S) as @.%a" i o helper_c exp
module VariableMap = Map.Make(String)

53
lib/miniImp/Types.mli
View File

@ -1,36 +1,39 @@
type variable = string
type p_exp =
Main of variable * variable * c_exp (* def main with input x output y as c *)
Main of variable * variable * c_exp
(* def main with input x output y as c *)
and c_exp =
Skip
| Assignment of variable * a_exp (* x := a *)
| Sequence of c_exp * c_exp (* c; c *)
| If of b_exp * c_exp * c_exp (* if b then c else c *)
| While of b_exp * c_exp (* while b do c *)
| For of c_exp * b_exp * c_exp * c_exp (* for (c; b; c) do c *)
| Assignment of variable * a_exp (* x := a *)
| Sequence of c_exp * c_exp (* c; c *)
| If of b_exp * c_exp * c_exp (* if b then c else c *)
| While of b_exp * c_exp (* while b do c *)
| For of c_exp * b_exp * c_exp * c_exp
(* for (c; b; c) do c *)
and b_exp =
Boolean of bool (* v *)
| BAnd of b_exp * b_exp (* b && b *)
| BOr of b_exp * b_exp (* b || b *)
| BNot of b_exp (* not b *)
| BCmp of a_exp * a_exp (* a == a *)
| BCmpLess of a_exp * a_exp (* a < a *)
| BCmpLessEq of a_exp * a_exp (* a <= a *)
| BCmpGreater of a_exp * a_exp (* a > a *)
| BCmpGreaterEq of a_exp * a_exp (* a >= a *)
Boolean of bool (* v *)
| BAnd of b_exp * b_exp (* b && b *)
| BOr of b_exp * b_exp (* b || b *)
| BNot of b_exp (* not b *)
| BCmp of a_exp * a_exp (* a == a *)
| BCmpLess of a_exp * a_exp (* a < a *)
| BCmpLessEq of a_exp * a_exp (* a <= a *)
| BCmpGreater of a_exp * a_exp (* a > a *)
| BCmpGreaterEq of a_exp * a_exp (* a >= a *)
and a_exp =
Variable of variable (* x *)
| Integer of int (* n *)
| Plus of a_exp * a_exp (* a + a *)
| Minus of a_exp * a_exp (* a - a *)
| Times of a_exp * a_exp (* a * a *)
| Division of a_exp * a_exp (* a / a *)
| Modulo of a_exp * a_exp (* a % a *)
| Power of a_exp * a_exp (* a ^ a *)
| PowerMod of a_exp * a_exp * a_exp (* a ^ a % a *)
| Rand of a_exp (* rand(0, a) *)
Variable of variable (* x *)
| Integer of int (* n *)
| Plus of a_exp * a_exp (* a + a *)
| Minus of a_exp * a_exp (* a - a *)
| Times of a_exp * a_exp (* a * a *)
| Division of a_exp * a_exp (* a / a *)
| Modulo of a_exp * a_exp (* a % a *)
| Power of a_exp * a_exp (* a ^ a *)
| PowerMod of a_exp * a_exp * a_exp (* a ^ a % a *)
| Rand of a_exp (* rand(0, a) *)
val pp_p_exp : Format.formatter -> p_exp -> unit
module VariableMap : Map.S with type key = variable

270
lib/miniImp/definedVariables.ml Normal file
View File

@ -0,0 +1,270 @@
open Analysis
module Variable = struct
type t = string
let pp (ppf: out_channel) (v: t) : unit =
Printf.fprintf ppf "%s" v
let pp_list (ppf: out_channel) (vv: t list) : unit =
List.iter (Printf.fprintf ppf "%s, ") vv
let compare a b =
String.compare a b
end
module RISCCfg = CfgRISC.RISCCfg
module DVCfg = Dataflow.Make (CfgRISC.RISCSimpleStatements) (Variable)
module DVCeltSet = Set.Make(Variable)
let variables (instr : DVCfg.elt) : DVCfg.internal list =
let aux (acc: DVCeltSet.t) (instr: DVCfg.elt) =
match instr with
| Nop ->
acc
| BRegOp (_, r1, r2, r3) ->
DVCeltSet.add r1.index acc |>
DVCeltSet.add r2.index |>
DVCeltSet.add r3.index
| BImmOp (_, r1, _, r3)
| URegOp (_, r1, r3)
| Load (r1, r3)
| Store (r1, r3) ->
DVCeltSet.add r1.index acc |>
DVCeltSet.add r3.index
| LoadI (_, r3) ->
DVCeltSet.add r3.index acc
in
aux DVCeltSet.empty instr |> DVCeltSet.to_list
let variables_all (instructions : DVCfg.elt list) : DVCfg.internal list =
List.fold_left (fun (acc: DVCeltSet.t) (instr: DVCfg.elt) ->
DVCeltSet.union acc (variables instr |> DVCeltSet.of_list)
) DVCeltSet.empty instructions |> DVCeltSet.to_list
let variables_used (instr : DVCfg.elt) : DVCfg.internal list =
let aux (acc: DVCeltSet.t) (instr: DVCfg.elt) =
match instr with
| Nop
| LoadI (_, _) ->
acc
| Store (r1, r2)
| BRegOp (_, r1, r2, _) ->
DVCeltSet.add r1.index acc |>
DVCeltSet.add r2.index
| BImmOp (_, r1, _, _)
| URegOp (_, r1, _)
| Load (r1, _) ->
DVCeltSet.add r1.index acc
in
aux DVCeltSet.empty instr |> DVCeltSet.to_list
let variables_used_all (instructions : DVCfg.elt list) : DVCfg.internal list =
List.fold_left (fun (acc: DVCeltSet.t) (instr: DVCfg.elt) ->
DVCeltSet.union acc (variables_used instr |> DVCeltSet.of_list)
) DVCeltSet.empty instructions |> DVCeltSet.to_list
let variables_defined (instructions : DVCfg.elt) : DVCfg.internal list =
let aux (acc: DVCeltSet.t) (instr: DVCfg.elt) =
match instr with
| Nop
| Store (_, _) -> acc
| BRegOp (_, _, _, r3)
| BImmOp (_, _, _, r3)
| URegOp (_, _, r3)
| Load (_, r3)
| LoadI (_, r3) ->
DVCeltSet.add r3.index acc
in
aux DVCeltSet.empty instructions |> DVCeltSet.to_list
(* init function, assign the bottom to everything *)
let _init_bottom : (DVCfg.elt list -> DVCfg.internal_node) =
(fun l -> {internal_in = [];
internal_out = [];
internal_between = (List.init (List.length l) (fun _ -> ([], [])))}
)
(* init function, assign the top to everything *)
let init_top (all_variables) : (DVCfg.elt list -> DVCfg.internal_node) =
(fun l -> {internal_in = all_variables;
internal_out = all_variables;
internal_between = (List.init (List.length l)
(fun _ -> (all_variables, all_variables)))})
let lub (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internal_node =
let prev_internal_var = Cfg.NodeMap.find node t.internal_var in
let code = match Cfg.NodeMap.find_opt node t.t.content with
None -> []
| Some c -> c
in
let new_internal_between = (
List.map
(fun (code, (i, _o)) ->
(i, Utility.unique_union i (variables_defined code)))
(List.combine code prev_internal_var.internal_between)
) in
let new_internal_out =
match new_internal_between with
| [] ->
prev_internal_var.internal_in
| _ ->
let _, newinternalout = (Utility.last_list new_internal_between) in
newinternalout
in
{ prev_internal_var with
internal_between = new_internal_between;
internal_out = new_internal_out }
let lucf (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internal_node =
let prev_internal_var = Cfg.NodeMap.find node t.internal_var in
if Option.equal (=) (Some node) t.t.initial then
(* if L is initial set dvin to the "in" register *)
let new_internal_in = (
match t.t.input_output_var with
Some (i, _) -> [i]
| None -> []
) in
let new_internal_between = (
(* set the dvin of each to the previous dvout *)
match prev_internal_var.internal_between with
[] -> []
| [(_i, o)] -> [(new_internal_in, o)]
| (_i, o) :: btwrest ->
(new_internal_in, o) :: (
List.map (fun ((_i, o), (_previ, prevo)) -> (prevo, o))
(Utility.combine_twice btwrest prev_internal_var.internal_between)
)
) in
{ prev_internal_var with
internal_in = new_internal_in;
internal_between = new_internal_between }
else
(* if L is not initial set dvin to the intersection of the previous node's
dvouts *)
let prev_nodes = Cfg.NodeMap.find node t.t.reverse_edges in
let new_internal_in = (
match prev_nodes with
| [] ->
[]
| [prevnode] ->
(Cfg.NodeMap.find prevnode t.internal_var).internal_out
| [prevnode1; prevnode2] ->
Utility.unique_intersection
(Cfg.NodeMap.find prevnode1 t.internal_var).internal_out
(Cfg.NodeMap.find prevnode2 t.internal_var).internal_out
| prevnode :: restnodes ->
List.fold_left (* intersection of all previous nodes' dvout *)
(fun acc prevnode ->
Utility.unique_intersection
acc
(Cfg.NodeMap.find prevnode t.internal_var).internal_out)
(Cfg.NodeMap.find prevnode t.internal_var).internal_out
restnodes
) in
let new_internal_between =
match prev_internal_var.internal_between with
[] -> []
| [(_i, o)] -> [(new_internal_in, o)]
| (_i, o) :: btwrest ->
(new_internal_in, o) :: (
List.map (fun ((_i, o), (_previ, prevo)) -> (prevo, o))
(Utility.combine_twice btwrest prev_internal_var.internal_between)
)
in
{ prev_internal_var with
internal_in = new_internal_in;
internal_between = new_internal_between }
let update (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internal_node =
let newt =
{t with internal_var = (Cfg.NodeMap.add node (lucf t node) t.internal_var)}
in
lub newt node
let compute_defined_variables (cfg: RISCCfg.t) : DVCfg.t =
(* creates the DVCfg structure and finds the fixed point *)
let all_variables = List.fold_left
(fun acc (_, code) ->
Utility.unique_union acc (variables_all code))
[]
(Cfg.NodeMap.to_list cfg.content)
in
let all_variables =
match cfg.input_output_var with
| None -> all_variables
| Some (i, o) -> Utility.unique_union all_variables [i;o]
in
DVCfg.from_cfg cfg
|> DVCfg.fixed_point ~init:(init_top all_variables) ~update:update
let check_undefined_variables (dvcfg: DVCfg.t) : Variable.t list option =
(* returns all undefined variables previously computed *)
let aux (node: Cfg.Node.t) (dvcfg: DVCfg.t) : Variable.t list option =
let code = match Cfg.NodeMap.find_opt node dvcfg.t.content with
None -> []
| Some c -> c
in
let internal_var = Cfg.NodeMap.find node dvcfg.internal_var in
let vua = variables_used_all code in
let outvar =
match (Option.equal (=) (Some node) dvcfg.t.terminal,
dvcfg.t.input_output_var,
internal_var.internal_out) with
| (true, Some (_, outvar), vout) ->
if List.mem outvar vout
then None
else Some outvar
| (_, _, _) ->
None
in
if Utility.inclusion vua (internal_var.internal_in) then
match outvar with None -> None
| Some outvar -> Some [outvar]
else
(* the variable might be defined inside the block, so check all vin and
return true only if all variables are properly defined *)
let vua_between = List.map variables_used code in
let undef_vars = List.fold_left
(fun acc (codevars, (vin, _vout)) ->
(Utility.subtraction codevars vin) @ acc)
[]
(List.combine vua_between internal_var.internal_between)
in
match outvar, undef_vars with
None, [] -> None
| None, undef_vars -> Some undef_vars
| Some outvar, [] -> Some [outvar]
| Some outvar, undef_vars -> Some (outvar :: undef_vars)
in
Cfg.NodeSet.fold (fun node acc ->
match acc, (aux node dvcfg) with
None, None -> None
| None, Some x -> Some x
| Some acc, None -> Some acc
| Some acc, Some x -> Some (acc @ x)
) dvcfg.t.nodes None
let compute_cfg (dvcfg: DVCfg.t) : RISCCfg.t =
(* no change to the cfg so returned as is *)
DVCfg.to_cfg dvcfg

18
lib/miniImp/definedVariables.mli Normal file
View File

@ -0,0 +1,18 @@
open Analysis
module Variable : sig
type t
val pp : out_channel -> t -> unit
val pp_list : out_channel -> t list -> unit
end
module RISCCfg = CfgRISC.RISCCfg
module DVCfg : Dataflow.C with type elt = CfgRISC.RISCSimpleStatements.t
and type internal = Variable.t
val compute_defined_variables : RISCCfg.t -> DVCfg.t
val compute_cfg : DVCfg.t -> RISCCfg.t
val check_undefined_variables : DVCfg.t -> Variable.t list option

8
lib/miniImp/dune
View File

@ -10,7 +10,11 @@
(library
(name miniImp)
(public_name miniImp)
(modules Lexer Parser Types Semantics Cfg)
(libraries utility menhirLib))
(modules Lexer Parser Types Semantics
CfgImp ReplacePowerMod
CfgRISC DefinedVariables LiveVariables
ReduceRegisters
RISC RISCSemantics)
(libraries analysis utility menhirLib))
(include_subdirs qualified)

357
lib/miniImp/liveVariables.ml Normal file
View File

@ -0,0 +1,357 @@
open Analysis
module Variable = struct
type t = string
let pp (ppf: out_channel) (v: t) : unit =
Printf.fprintf ppf "%s" v
let pp_list (ppf: out_channel) (vv: t list) : unit =
List.iter (Printf.fprintf ppf "%s, ") vv
let compare a b =
String.compare a b
end
module RISCCfg = CfgRISC.RISCCfg
module DVCfg = Dataflow.Make (CfgRISC.RISCSimpleStatements) (Variable)
module DVCeltSet = Set.Make(Variable)
let variables_used (instr : DVCfg.elt)
: DVCfg.internal list =
let aux (acc: DVCeltSet.t) (instr: DVCfg.elt) =
match instr with
| Nop
| LoadI (_, _) ->
acc
| BRegOp (_, r1, r2, _)
| Store (r1, r2) ->
DVCeltSet.add r1.index acc |>
DVCeltSet.add r2.index
| BImmOp (_, r1, _, _)
| URegOp (_, r1, _)
| Load (r1, _) ->
DVCeltSet.add r1.index acc
in
aux DVCeltSet.empty instr |> DVCeltSet.to_list
let variables_defined (instructions : DVCfg.elt) : DVCfg.internal list =
let aux (acc: DVCeltSet.t) (instr: DVCfg.elt) =
match instr with
| Nop
| Store (_, _) -> acc
| BRegOp (_, _, _, r3)
| BImmOp (_, _, _, r3)
| URegOp (_, _, r3)
| Load (_, r3)
| LoadI (_, r3) ->
DVCeltSet.add r3.index acc
in
aux DVCeltSet.empty instructions |> DVCeltSet.to_list
let variables (instruction : DVCfg.elt) : DVCfg.internal list =
let aux (acc: DVCeltSet.t) (instr: DVCfg.elt) =
match instr with
| Nop -> acc
| Store (r1, r2) ->
DVCeltSet.add r1.index acc |>
DVCeltSet.add r2.index
| BRegOp (_, r1, r2, r3) ->
DVCeltSet.add r1.index acc |>
DVCeltSet.add r2.index |>
DVCeltSet.add r3.index
| BImmOp (_, r1, _, r3)
| URegOp (_, r1, r3)
| Load (r1, r3) ->
DVCeltSet.add r1.index acc |>
DVCeltSet.add r3.index
| LoadI (_, r3) ->
DVCeltSet.add r3.index acc
in
aux DVCeltSet.empty instruction |> DVCeltSet.to_list
let variables_all (instructions : DVCfg.elt list) : DVCfg.internal list =
List.fold_left (fun (acc: DVCeltSet.t) (instr: DVCfg.elt) ->
DVCeltSet.union acc (variables instr |> DVCeltSet.of_list)
) DVCeltSet.empty instructions |> DVCeltSet.to_list
(* init function, assign the bottom to everything *)
let init : (DVCfg.elt list -> DVCfg.internal_node) =
(fun l -> {internal_in = [];
internal_out = [];
internal_between = (List.init (List.length l) (fun _ -> ([], [])))}
)
let lub (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internal_node =
let prev_internal_var = Cfg.NodeMap.find node t.internal_var in
let code = match Cfg.NodeMap.find_opt node t.t.content with
None -> []
| Some c -> c
in
let new_internal_between = (
List.map
(fun (code, (_i, o)) ->
(Utility.unique_union
(variables_used code)
(Utility.subtraction o (variables_defined code)), o))
(Utility.combine_twice code prev_internal_var.internal_between)
) in
let new_internal_in =
match new_internal_between with
| [] -> prev_internal_var.internal_out
| (i, _)::_ -> i
in
{ prev_internal_var with
internal_between = new_internal_between;
internal_in = new_internal_in; }
let lucf (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internal_node =
let prev_internal_var = Cfg.NodeMap.find node t.internal_var in
let newinternalout = (
if Option.equal (=) (Some node) t.t.terminal then (
match t.t.input_output_var with
Some (_, o) -> [o]
| None -> []
) else (
let nextnodes = Cfg.NodeMap.find_opt node t.t.edges in
match nextnodes with
| None -> []
| Some (node, None) ->
(Cfg.NodeMap.find node t.internal_var).internal_in
| Some (node1, Some node2) ->
Utility.unique_union
(Cfg.NodeMap.find node1 t.internal_var).internal_in
(Cfg.NodeMap.find node2 t.internal_var).internal_in
)
) in
let new_internal_between = (
match List.rev prev_internal_var.internal_between with
| [] -> []
| (i, _o) :: btwrest ->
let btwrest = List.rev btwrest in
let newbtwrest = List.map2
(fun (i, _o) (nexti, _nexto) -> (i, nexti))
btwrest
(Utility.drop_first_element_list prev_internal_var.internal_between)
in
newbtwrest @ [(i, newinternalout)]
) in
{ prev_internal_var with
internal_out = newinternalout;
internal_between = new_internal_between; }
let update (t: DVCfg.t) (node: Cfg.Node.t) : DVCfg.internal_node =
let newt = {t with internal_var = (Cfg.NodeMap.add node
(lucf t node)
t.internal_var)} in
lub newt node
let compute_live_variables (cfg: RISCCfg.t) : DVCfg.t =
DVCfg.from_cfg cfg
|> DVCfg.fixed_point ~init:init ~update:update
module VariableMap = struct
include Map.Make(Variable)
let first_empty next start m l =
let bindings =
List.fold_left (
fun acc x ->
match find_opt x m with
| None -> acc
| Some x -> x :: acc) [] l |> List.sort Variable.compare in
let rec aux x =
if List.mem x bindings
then aux (next x)
else x
in
aux start
let first_empty_Variable m l =
let next = fun x -> x |> int_of_string |> (+) 1 |> string_of_int in
let start = "1" in
first_empty next start m l
let get_or_set_mapping m l r =
match find_opt r m with
| None -> (
let newr = first_empty_Variable m l in
let newm = add r newr m in
(newm, newr)
)
| Some r -> (m, r)
end
(* just rename the registers that dont share live status *)
let optimize_cfg (t: DVCfg.t) : DVCfg.t =
let replace_code ((vin, vout): Variable.t list * Variable.t list)
(a: Variable.t VariableMap.t)
(code: DVCfg.elt)
: (Variable.t VariableMap.t * DVCfg.elt) =
match code with
| Nop -> (
(a, Nop)
)
| BRegOp (brop, r1, r2, r3) -> (
let (newa, newr1) = VariableMap.get_or_set_mapping a vin r1.index in
let (newa, newr2) = VariableMap.get_or_set_mapping newa vin r2.index in
let (newa, newr3) = VariableMap.get_or_set_mapping newa vout r3.index in
(newa, BRegOp (brop, {index = newr1}, {index = newr2}, {index = newr3}))
)
| BImmOp (biop, r1, i, r3) -> (
let (newa, newr1) = VariableMap.get_or_set_mapping a vin r1.index in
let (newa, newr3) = VariableMap.get_or_set_mapping newa vout r3.index in
(newa, BImmOp (biop, {index = newr1}, i, {index = newr3}))
)
| URegOp (urop, r1, r3) -> (
let (newa, newr1) = VariableMap.get_or_set_mapping a vin r1.index in
let (newa, newr3) = VariableMap.get_or_set_mapping newa vout r3.index in
(newa, URegOp (urop, {index = newr1}, {index = newr3}))
)
| Load (r1, r3) -> (
let (newa, newr1) = VariableMap.get_or_set_mapping a vin r1.index in
let (newa, newr3) = VariableMap.get_or_set_mapping newa vout r3.index in
(newa, Load ({index = newr1}, {index = newr3}))
)
| LoadI (i, r3) -> (
let (newa, newr3) = VariableMap.get_or_set_mapping a vout r3.index in
(newa, LoadI (i, {index = newr3}))
)
| Store (r1, r3) -> (
let (newa, newr1) = VariableMap.get_or_set_mapping a vin r1.index in
let (newa, newr3) = VariableMap.get_or_set_mapping newa vout r3.index in
(newa, Store ({index = newr1}, {index = newr3}))
)
in
let aux
(assignments: Variable.t VariableMap.t)
(t: DVCfg.t)
(node: Cfg.Node.t)
: (Variable.t VariableMap.t * DVCfg.t) =
let livevars = Cfg.NodeMap.find node t.internal_var in
let code =
match Cfg.NodeMap.find_opt node t.t.content with
| None -> []
| Some x -> x
in
let new_code, new_assignments =
(List.fold_left2
(fun (acc, assignments) btw code ->
let na, nc = replace_code btw assignments code in
(acc @ [nc], na)
)
([], assignments)
livevars.internal_between
code)
in
let newcontent = Cfg.NodeMap.add
node
new_code
t.t.content
in
let newt = { t with t = { t.t with content = newcontent } } in
(new_assignments, newt)
in
(* ------------------- *)
(* at least the input variable should be in the mapping *)
let assignments =
match t.t.input_output_var with
None -> VariableMap.empty
| Some (i, _o) -> (
VariableMap.get_or_set_mapping VariableMap.empty [] i |> fst
)
in
let all_variables = List.fold_left
(fun acc (_, code) ->
Utility.unique_union acc (variables_all code))
[]
(Cfg.NodeMap.to_list t.t.content)
in
let mapping =
(* for each variable we get the union of all in and out that contains it
then we find a register such that it's not in conflict *)
List.fold_left (fun assignments v -> (
(* union of all in and out such that v is in the set *)
let union : 'a list =
List.fold_left
(fun (acc: 'a list) (node, (x: DVCfg.internal_node)) ->
(* not interested in internalin or internalout since information
is mirrored into internalbetween *)
List.fold_left2
(fun acc (i, o) code ->
(* we also consider the out set if we "use" v as a
guard *)
match List.mem v i,
List.mem v o,
List.mem v (variables_defined code) with
| false, false, false -> acc
| true, false, false -> Utility.unique_union i acc
| false, false, true
| false, true, _ -> Utility.unique_union o acc
| true, false, true
| true, true, _ -> Utility.unique_union
(Utility.unique_union i o) acc
)
acc
x.internal_between
(Cfg.NodeMap.find_opt node t.t.content |>
Option.value ~default:[])
)
[]
(Cfg.NodeMap.to_list t.internal_var)
in
let assignments, _ =
VariableMap.get_or_set_mapping assignments union v in
assignments
)) assignments all_variables
in
let mapping, newt =
Cfg.NodeSet.fold (* for each node we replace all the variables with the
optimized ones *)
(fun node (assign, t) -> aux assign t node)
t.t.nodes
(mapping, t)
in
{ newt with
t = { newt.t with
input_output_var =
match newt.t.input_output_var with
None -> None
| Some (i, o) -> (
match VariableMap.find_opt i mapping,
VariableMap.find_opt o mapping with
| None, None -> Some (i, o)
| Some i, None -> Some (i, o)
| None, Some o -> Some (i, o)
| Some i, Some o -> Some (i, o)
)
}}
let compute_cfg (dvcfg: DVCfg.t) : RISCCfg.t =
DVCfg.to_cfg dvcfg

18
lib/miniImp/liveVariables.mli Normal file
View File

@ -0,0 +1,18 @@
open Analysis
module Variable : sig
type t
val pp : out_channel -> t -> unit
end
module RISCCfg = CfgRISC.RISCCfg
module DVCfg : Dataflow.C with type elt = CfgRISC.RISCSimpleStatements.t
and type internal = Variable.t
val compute_live_variables : RISCCfg.t -> DVCfg.t
val optimize_cfg : DVCfg.t -> DVCfg.t
val compute_cfg : DVCfg.t -> RISCCfg.t

444
lib/miniImp/reduceRegisters.ml Normal file
View File

@ -0,0 +1,444 @@
open Analysis
module Variable = struct
type t = string
let _pp (ppf: out_channel) (v: t) : unit =
Printf.fprintf ppf "%s" v
let _pplist (ppf: out_channel) (vv: t list) : unit =
List.iter (Printf.fprintf ppf "%s, ") vv
let compare a b =
String.compare a b
end
module RISCCfg = CfgRISC.RISCCfg
module VariableMap = Map.Make(Variable)
let variables_frequency (instr : RISCCfg.elt) : (Variable.t * int) list =
let add_one = (fun x -> match x with None -> Some 1 | Some x -> Some (x + 1))
in
let aux (acc: int VariableMap.t) (instr: RISCCfg.elt) : int VariableMap.t =
match instr with
| Nop ->
acc
| BRegOp (_, r1, r2, r3) ->
VariableMap.update r1.index add_one acc |>
VariableMap.update r2.index add_one |>
VariableMap.update r3.index add_one
| BImmOp (_, r1, _, r3)
| URegOp (_, r1, r3)
| Load (r1, r3)
| Store (r1, r3) ->
VariableMap.update r1.index add_one acc |>
VariableMap.update r3.index add_one
| LoadI (_, r3) ->
VariableMap.update r3.index add_one acc
in
aux VariableMap.empty instr |> VariableMap.to_list
(* computes syntactic frequency of all variables in the code *)
let variables_all_frequency (instructions : RISCCfg.elt list)
: (Variable.t * int) list =
List.fold_left
( fun (acc: int VariableMap.t) (instr: RISCCfg.elt) ->
VariableMap.union
(fun _v x y -> Some (x + y))
acc (variables_frequency instr |> VariableMap.of_list) )
VariableMap.empty instructions |> VariableMap.to_list
let reduce_registers (n: int) (cfg: RISCCfg.t) : RISCCfg.t =
(if n < 4 then (
failwith "ReduceRegisters: number of registers too small"
) else ());
(* we get all the variables with associated frequency (only syntactic use) *)
let all_variables = List.fold_left
(fun acc (_, code) ->
Utility.unique_union_assoc
(fun _n x y -> x + y) acc (variables_all_frequency code))
[]
(Cfg.NodeMap.to_list cfg.content)
in
(* add one to in and out variables *)
let all_variables =
match cfg.input_output_var with
| None -> all_variables
| Some (i, _o) -> (
match List.assoc_opt i all_variables with
| None -> (i, 1) :: all_variables
| Some f -> (i, f+1) :: (List.remove_assoc i all_variables)
)
in
let all_variables =
match cfg.input_output_var with
| None -> all_variables
| Some (_i, o) -> (
match List.assoc_opt o all_variables with
| None -> (o, 1) :: all_variables
| Some f -> (o, f+1) :: (List.remove_assoc o all_variables)
)
in
(* replace each operation with a list of operations that have the new
registers or load from memory *)
let replace_registers
(remappedregisters: Variable.t VariableMap.t)
(memorymap: int VariableMap.t)
(temporaryregisters: Variable.t list)
(code: RISCCfg.elt list)
: RISCCfg.elt list =
let tmpreg1: CfgRISC.RISCSimpleStatements.register =
{index = List.nth temporaryregisters 0} in
let tmpreg2: CfgRISC.RISCSimpleStatements.register =
{index = List.nth temporaryregisters 1} in
let aux (instruction: RISCCfg.elt) : RISCCfg.elt list =
match instruction with
| Nop -> [Nop]
| BRegOp (brop, r1, r2, r3) -> (
match ( VariableMap.find_opt r1.index remappedregisters,
VariableMap.find_opt r2.index remappedregisters,
VariableMap.find_opt r3.index remappedregisters,
VariableMap.find_opt r1.index memorymap,
VariableMap.find_opt r2.index memorymap,
VariableMap.find_opt r3.index memorymap )
with
| Some r1, Some r2, Some r3, _, _, _ ->
[BRegOp (brop, {index = r1}, {index = r2}, {index = r3})]
| Some r1, None, Some r3, _, Some m2, _ ->
[LoadI (m2, tmpreg2);
Load (tmpreg2, tmpreg2);
BRegOp (brop, {index = r1}, tmpreg2, {index = r3})]
| None, Some r2, Some r3, Some m1, _, _ ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
BRegOp (brop, tmpreg1, {index = r2}, {index = r3})]
| None, None, Some r3, Some m1, Some m2, _ ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
LoadI (m2, tmpreg2);
Load (tmpreg2, tmpreg2);
BRegOp (brop, tmpreg1, tmpreg2, {index = r3})]
| Some r1, Some r2, None, _, _, Some m3 ->
[BRegOp (brop, {index = r1}, {index = r2}, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| Some r1, None, None, _, Some m2, Some m3 ->
[LoadI (m2, tmpreg2);
Load (tmpreg2, tmpreg2);
BRegOp (brop, {index = r1}, tmpreg2, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| None, Some r2, None, Some m1, _, Some m3 ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
BRegOp (brop, tmpreg1, {index = r2}, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| None, None, None, Some m1, Some m2, Some m3 ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
LoadI (m2, tmpreg2);
Load (tmpreg2, tmpreg2);
BRegOp (brop, tmpreg1, tmpreg2, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| _ -> [BRegOp (brop,
{index = r1.index},
{index = r2.index},
{index = r3.index})]
)
| BImmOp (biop, r1, i, r3) -> (
match ( VariableMap.find_opt r1.index remappedregisters,
VariableMap.find_opt r3.index remappedregisters,
VariableMap.find_opt r1.index memorymap,
VariableMap.find_opt r3.index memorymap )
with
| Some r1, Some r3, _, _ ->
[BImmOp (biop, {index = r1}, i, {index = r3})]
| Some r1, None, _, Some m3 ->
[BImmOp (biop, {index = r1}, i, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| None, Some r3, Some m1, _ ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
BImmOp (biop, tmpreg1, i, {index = r3})]
| None, None, Some m1, Some m3 ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
BImmOp (biop, tmpreg1, i, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| _ -> failwith ("ReduceRegisters: fail to partition a set, some" ^
" registers have no binding.")
)
| URegOp (urop, r1, r3) ->(
match ( VariableMap.find_opt r1.index remappedregisters,
VariableMap.find_opt r3.index remappedregisters,
VariableMap.find_opt r1.index memorymap,
VariableMap.find_opt r3.index memorymap )
with
| Some r1, Some r3, _, _ ->
[URegOp (urop, {index = r1}, {index = r3})]
| Some r1, None, _, Some m3 ->
[URegOp (urop, {index = r1}, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| None, Some r3, Some m1, _ ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
URegOp (urop, tmpreg1, {index = r3})]
| None, None, Some m1, Some m3 ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
URegOp (urop, tmpreg1, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| _ -> failwith ("ReduceRegisters: fail to partition a set, some" ^
" registers have no binding.")
)
| Load (r1, r3) -> (
match ( VariableMap.find_opt r1.index remappedregisters,
VariableMap.find_opt r3.index remappedregisters,
VariableMap.find_opt r1.index memorymap,
VariableMap.find_opt r3.index memorymap )
with
| Some r1, Some r3, _, _ ->
[Load ({index = r1}, {index = r3})]
| Some r1, None, _, Some m3 ->
[Load ({index = r1}, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| None, Some r3, Some m1, _ ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
Load (tmpreg1, {index = r3})]
| None, None, Some m1, Some m3 ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
Load (tmpreg1, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| _ -> failwith ("ReduceRegisters: fail to partition a set, some" ^
" registers have no binding.")
)
| LoadI (i, r3) -> (
(* we want to store an integer in memory immediately (strange, but
unless better heuristic to choose the variables to replace we are
stuck) *)
match ( VariableMap.find_opt r3.index remappedregisters,
VariableMap.find_opt r3.index memorymap )
with
| Some r3, _ ->
[LoadI (i, {index = r3})]
| None, Some m3 ->
[LoadI (i, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| _ -> failwith ("ReduceRegisters: fail to partition a set, some" ^
" registers have no binding.")
)
| Store (r1, r3) -> (
(* we want to maybe store an address in memory (very confusing,
but maybe possible) *)
match ( VariableMap.find_opt r1.index remappedregisters,
VariableMap.find_opt r3.index remappedregisters,
VariableMap.find_opt r1.index memorymap,
VariableMap.find_opt r3.index memorymap )
with
| Some r1, Some r3, _, _ ->
[Store ({index = r1}, {index = r3})]
| Some r1, None, _, Some m3 ->
[Store ({index = r1}, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| None, Some r3, Some m1, _ ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
Store (tmpreg1, {index = r3})]
| None, None, Some m1, Some m3 ->
[LoadI (m1, tmpreg1);
Load (tmpreg1, tmpreg1);
Store (tmpreg1, tmpreg2);
LoadI (m3, tmpreg1);
Store (tmpreg2, tmpreg1)]
| _ -> failwith ("ReduceRegisters: fail to partition a set, some" ^
" registers have no binding.")
)
in
List.map aux code |> List.concat
in
(* partition the variables into two sets, most frequent and least frequent
then apply the transformation *)
let aux (cfg: RISCCfg.t) (all_variables: (string * int) list) =
(* we keep the first two variables free for immediate use *)
let most_frequent, least_frequent =
List.sort (fun (_a, fa) (_b, fb) -> Int.compare fb fa) all_variables
|> Utility.take (n-2)
in
let most_frequent, _frequencies = List.split most_frequent in
let least_frequent, _frequencies = List.split least_frequent in
(* we map the most frequent to new registers, so that the first two are
always free *)
let most_frequent_mapping = (* +3 because starts at 0, but we want to start
at 1*)
List.mapi
(fun n v -> (v, (string_of_int (n+3): Variable.t)))
most_frequent
|> VariableMap.of_list
in
(* we map the least to memory *)
let least_frequent_mapping =
List.mapi (fun n v -> (v, (n: int))) least_frequent
|> VariableMap.of_list
in
(* we need to replace both at the same time, because we might have mapped
some registers to already used registers, so a double pass might not
differentiate the two *)
(* special care must be taken for the in and out registers *)
let newcfg = {
cfg with
content = Cfg.NodeMap.map
( fun x ->
replace_registers
most_frequent_mapping
least_frequent_mapping
["1"; "2"]
x
) cfg.content}
in
if newcfg.input_output_var = None
then newcfg (* if no input or output variables we ignore *)
else
let i, o = Option.get newcfg.input_output_var in
match (VariableMap.find_opt i most_frequent_mapping,
VariableMap.find_opt o most_frequent_mapping,
VariableMap.find_opt i least_frequent_mapping,
VariableMap.find_opt o least_frequent_mapping,
newcfg.initial,
newcfg.terminal )
with (*we check if in and out are simply remapped or are put in memory*)
| Some i, Some o, _, _, _, _ ->
{ newcfg with input_output_var = Some (i, o) }
| Some i, None, _, Some _, _, None ->
(* we check for the terminal node, if not present we are very confused
and dont modify the out variable *)
{ newcfg with input_output_var = Some (i, o)}
| Some i, None, _, Some mo, _, Some n ->
(* since the output simbol is in memory we need to first retrive it
and then put the result in a temporary register *)
let terminal_content = (
match Cfg.NodeMap.find_opt n newcfg.content with
| None -> []
| Some x -> x
) @ [LoadI (mo, {index = "2"});
Load ({index = "2"}, {index = "2"})]
in
let content =
Cfg.NodeMap.add n terminal_content newcfg.content
in
{ newcfg with
input_output_var = Some (i, "2");
content = content
}
| None, Some o, Some _, _, _, None ->
{ newcfg with input_output_var = Some (i, o) }
| None, Some o, Some mi, _, _, Some n -> (
(* the input simbol should be stored in memory *)
let initialcontent =
[(LoadI (mi, {index = "2"}) : RISCCfg.elt);
Store ({index = "1"}, {index = "2"})] @ (
match Cfg.NodeMap.find_opt n newcfg.content with
| None -> []
| Some x -> x
)
in
let content = Cfg.NodeMap.add n initialcontent newcfg.content in
{ newcfg with
input_output_var = Some ("1", o);
content = content
}
)
| None, None, Some _, Some _, None, None ->
{ newcfg with input_output_var = Some (i, o) }
| None, None, Some _, Some mo, None, Some n ->
(* both simbols should be in memory *)
let terminalcontent = (
match Cfg.NodeMap.find_opt n newcfg.content with
| None -> []
| Some x -> x
) @ [LoadI (mo, {index = "2"});
Load ({index = "2"}, {index = "2"})]
in
let content =
Cfg.NodeMap.add n terminalcontent newcfg.content
in
{ newcfg with
input_output_var = Some (i, "2");
content = content
}
| None, None, Some mi, Some _, Some n, None ->
(* both simbols should be in memory *)
let initialcontent =
[(LoadI (mi, {index = "2"}) : RISCCfg.elt);
Store ({index = "1"}, {index = "2"})] @ (
match Cfg.NodeMap.find_opt n newcfg.content with
| None -> []
| Some x -> x
)
in
let content = Cfg.NodeMap.add n initialcontent newcfg.content in
{ newcfg with
input_output_var = Some ("1", o);
content = content
}
| None, None, Some mi, Some mo, Some ni, Some no ->
(* both simbols should be in memory *)
let initialcontent =
[(LoadI (mi, {index = "2"}) : RISCCfg.elt);
Store ({index = "1"}, {index = "2"})] @ (
match Cfg.NodeMap.find_opt ni newcfg.content with
| None -> []
| Some x -> x
)
in
let terminalcontent = (
match Cfg.NodeMap.find_opt no newcfg.content with
| None -> []
| Some x -> x
) @ [LoadI (mo, {index = "2"});
Load ({index = "2"}, {index = "2"})]
in
let content =
Cfg.NodeMap.add ni initialcontent newcfg.content
in
let content =
Cfg.NodeMap.add no terminalcontent content
in
{ newcfg with
input_output_var = Some ("1", "2");
content = content
}
| _ -> failwith ("ReduceRegisters: fail to partition a set, some" ^
" registers have no binding.")
in
( if List.length all_variables <= n
then cfg
else aux cfg all_variables )

3
lib/miniImp/reduceRegisters.mli Normal file
View File

@ -0,0 +1,3 @@
module RISCCfg = CfgRISC.RISCCfg
val reduce_registers : int -> RISCCfg.t -> RISCCfg.t

262
lib/miniImp/replacePowerMod.ml Normal file
View File

@ -0,0 +1,262 @@
let rewrite_instructions (prg: Types.p_exp) : Types.p_exp =
(* function takes a program and replaces all occurrences of powermod with
simpler instructions *)
let Main (i, o, prg) = prg in
let rec contains_rewrite (prg: Types.c_exp) : Types.a_exp option =
(* if the ast contains powermod anywhere returns the powermod, otherwise
returns none *)
match prg with
| Skip -> None
| Assignment (_, a) -> contains_rewrite_a a
| Sequence (c1, c2) -> (
match contains_rewrite c1, contains_rewrite c2 with
| None, None -> None
| Some a, _
| _, Some a -> Some a
)
| If (b, c1, c2) -> (
match contains_rewrite_b b,
contains_rewrite c1,
contains_rewrite c2
with
| None, None, None -> None
| Some a, _, _
| _, Some a, _
| _, _, Some a -> Some a
)
| While (b, c) -> (
match contains_rewrite_b b, contains_rewrite c with
| None, None -> None
| Some a, _
| _, Some a -> Some a
)
| For (c1, b, c2, c3) -> (
match contains_rewrite c1,
contains_rewrite_b b,
contains_rewrite c2,
contains_rewrite c3
with
| None, None, None, None -> None
| Some a, _, _, _
| _, Some a, _, _
| _, _, Some a, _
| _, _, _, Some a -> Some a
)
and contains_rewrite_b (b: Types.b_exp) : Types.a_exp option =
match b with
| Boolean (_) -> None
| BAnd (b1, b2)
| BOr (b1, b2) -> (
match contains_rewrite_b b1, contains_rewrite_b b2 with
None, None -> None
| Some a, _
| _, Some a -> Some a
)
| BNot (b) -> contains_rewrite_b b
| BCmp (a1, a2)
| BCmpLess (a1, a2)
| BCmpLessEq (a1, a2)
| BCmpGreater (a1, a2)
| BCmpGreaterEq (a1, a2) -> (
match contains_rewrite_a a1, contains_rewrite_a a2 with
None, None -> None
| Some a, _
| _, Some a -> Some a
)
and contains_rewrite_a (a: Types.a_exp) : Types.a_exp option =
match a with
| Variable _
| Integer _ -> None
| Plus (a1, a2)
| Minus (a1, a2)
| Times (a1, a2)
| Division (a1, a2)
| Modulo (a1, a2)
| Power (a1, a2) -> (
match contains_rewrite_a a1, contains_rewrite_a a2 with
None, None -> None
| Some a, _
| _, Some a -> Some a
)
| PowerMod (_) -> Some a
| Rand (a) -> contains_rewrite_a a
in
(* obtain the list of used variables so that fresh ones can be created *)
let rec uv (prg: Types.c_exp) : Types.variable list =
match prg with
| Skip -> []
| Assignment (x, _) -> [x]
| Sequence (c1, c2) -> uv c1 @ uv c2
| If (_, c1, c2) -> uv c1 @ uv c2
| While (_, c) -> uv c
| For (c1, _, c2, c3) -> uv c1 @ uv c2 @ uv c3
in
let usedvariables = i :: o :: (uv prg) in
let counter = ref 0 in
let new_fresh_var (pref: string) : Types.variable =
let rec h () =
let candidate = pref ^ (string_of_int !counter) in
if (List.mem candidate usedvariables) then (
counter := !counter + 1;
h ()
) else (
counter := !counter + 1;
candidate
)
in
h ()
in
(* functions that replace a pattern in a subexpression *)
let rec replace_occurrence_a
(pattern: Types.a_exp)
(replace: Types.a_exp)
(a: Types.a_exp)
: Types.a_exp =
if a = pattern then
replace
else (
let r_o_a = replace_occurrence_a pattern replace in
match a with
| Variable _
| Integer _ -> a
| Plus (a1, a2) -> Plus (r_o_a a1, r_o_a a2)
| Minus (a1, a2) -> Minus (r_o_a a1, r_o_a a2)
| Times (a1, a2) -> Times (r_o_a a1, r_o_a a2)
| Division (a1, a2) -> Division (r_o_a a1, r_o_a a2)
| Modulo (a1, a2) -> Modulo (r_o_a a1, r_o_a a2)
| Power (a1, a2) -> Power (r_o_a a1, r_o_a a2)
| PowerMod (a1, a2, a3) -> PowerMod (r_o_a a1, r_o_a a2, r_o_a a3)
| Rand (a) -> Rand (r_o_a a)
)
and replace_occurrence_b
(pattern: Types.a_exp)
(replace: Types.a_exp)
(b: Types.b_exp)
: Types.b_exp =
let r_o_b = replace_occurrence_b pattern replace in
let r_o_a = replace_occurrence_a pattern replace in
match b with
| Boolean _ -> b
| BAnd (b1, b2) -> BAnd (r_o_b b1, r_o_b b2)
| BOr (b1, b2) -> BOr (r_o_b b1, r_o_b b2)
| BNot (b) -> BNot (r_o_b b)
| BCmp (a1, a2) -> BCmp (r_o_a a1, r_o_a a2)
| BCmpLess (a1, a2) -> BCmpLess (r_o_a a1, r_o_a a2)
| BCmpLessEq (a1, a2) -> BCmpLessEq (r_o_a a1, r_o_a a2)
| BCmpGreater (a1, a2) -> BCmpGreater (r_o_a a1, r_o_a a2)
| BCmpGreaterEq (a1, a2) -> BCmpGreaterEq (r_o_a a1, r_o_a a2)
in
(* function that creates the equivalent code for a powermod using simpler
instructions *)
let partial freshres a1 a2 a3 : Types.c_exp =
let freshpow = new_fresh_var "pow" in
let freshexp = new_fresh_var "exp" in
let freshmod = new_fresh_var "mod" in
Sequence (
Sequence (
Sequence (
Assignment (freshpow, a1),
Assignment (freshexp, a2)),
Sequence (
Assignment (freshmod, a3),
Assignment (freshres, Integer 1))),
Sequence (
If (BCmpLess (Variable freshexp, Integer 0),
Assignment (freshexp, Minus (Integer 0, Variable freshexp)),
Skip),
While (
BCmpGreater (Variable freshexp, Integer 0),
Sequence (
If (BCmp (Integer 1, Modulo (Variable freshexp, Integer 2)),
Assignment (freshres,
Modulo (Times (Variable freshres,
Variable freshpow),
Variable freshmod)),
Skip),
Sequence (
Assignment (freshpow,
Modulo (Times (Variable freshpow,
Variable freshpow),
Variable freshmod)),
Assignment (freshexp, Division (Variable freshexp, Integer 2))
)))))
in
let replace_pwm (pwm: Types.a_exp) (p: Types.c_exp) : Types.c_exp =
match pwm, p with
| PowerMod (a1, a2, a3), Assignment (x, a) ->
let freshres = new_fresh_var "res" in
Sequence (
partial freshres a1 a2 a3,
Assignment(x, replace_occurrence_a pwm (Variable freshres) a)
)
| PowerMod (a1, a2, a3), If (b, ifa1, ifa2) ->
let freshres = new_fresh_var "res" in
Sequence (
partial freshres a1 a2 a3,
If (replace_occurrence_b pwm (Variable freshres) b, ifa1, ifa2)
)
| PowerMod (a1, a2, a3), While (b, wa) ->
let freshres = new_fresh_var "res" in
Sequence (
partial freshres a1 a2 a3,
While (replace_occurrence_b pwm (Variable freshres) b, wa)
)
| PowerMod (a1, a2, a3), For (fora1, b, fora2, fora3) ->
let freshres = new_fresh_var "res" in
Sequence (
partial freshres a1 a2 a3,
For ( fora1,
replace_occurrence_b pwm (Variable freshres) b,
fora2,
fora3 )
)
| _ -> failwith "PowerMod is not present"
in
let rec rw_a (prg: Types.c_exp) : Types.c_exp =
match prg with
| Skip -> Skip
| Assignment (x, a) -> (
match contains_rewrite_a a with
None -> Assignment (x, a)
| Some (PowerMod (a1, a2, a3)) -> (
replace_pwm (PowerMod (a1, a2, a3)) prg
)
| Some _ -> failwith "Found powmod then lost it."
)
| Sequence (c1, c2) -> Sequence (rw_a c1, rw_a c2)
| If (b, c1, c2) -> (
match contains_rewrite_b b with
None -> If (b, rw_a c1, rw_a c2)
| Some (PowerMod (a1, a2, a3)) ->
replace_pwm (PowerMod (a1, a2, a3)) prg
| Some _ -> failwith "Found powmod then lost it."
)
| While (b, c) -> (
match contains_rewrite_b b with
None -> While (b, rw_a c)
| Some (PowerMod (a1, a2, a3)) ->
replace_pwm (PowerMod (a1, a2, a3)) prg
| Some _ -> failwith "Found powmod then lost it."
)
| For (c1, b, c2, c3) -> (
match contains_rewrite_b b with
None -> For (rw_a c1, b, rw_a c2, rw_a c3)
| Some (PowerMod (a1, a2, a3)) ->
replace_pwm (PowerMod (a1, a2, a3)) prg
| Some _ -> failwith "Found powmod then lost it."
)
in
(* we first check that at least one powermod is present *)
if Option.is_none (contains_rewrite prg) then
Main (i, o, prg)
else
Main (i, o, rw_a prg)

1
lib/miniImp/replacePowerMod.mli Normal file
View File

@ -0,0 +1 @@
val rewrite_instructions : Types.p_exp -> Types.p_exp

149
lib/utility/utility.ml
View File

@ -12,7 +12,6 @@ let rec powmod a d = function
let b = (powmod a d (n / 2)) mod d in
(((b * b) mod d) * (if n mod 2 = 0 then 1 else a)) mod d
let alphabet = "abcdefghijklmnopqrstuvwxyz"
let base = 26
@ -23,3 +22,151 @@ let rec fromIntToString (x: int) : string =
String.get alphabet x |> String.make 1
else
(fromIntToString (x/base - 1)) ^ (String.get alphabet (x mod base) |> String.make 1)
let int_and a b =
match (a>0, b>0) with
true, true -> 1
| _, _ -> 0
let int_or a b =
match (a>0, b>0) with
false, false -> 0
| _, _ -> 1
let int_eq a b =
if a = b then 1 else 0
let int_less a b =
if a < b then 1 else 0
let int_less_eq a b =
if a <= b then 1 else 0
let int_more a b =
if a > b then 1 else 0
let int_more_eq a b =
if a >= b then 1 else 0
let int_not a =
if a > 0 then 0 else 1
(* converts an integer to a list of chars such that it is pretty and linear *)
(* let rec fromIntToString (alphabet: string) (x: int) : string = *)
(* let base = String.length alphabet in *)
(* if x < 0 then *)
(* "" *)
(* else if x < base then *)
(* String.get alphabet x |> String.make 1 *)
(* else *)
(* (fromIntToString (alphabet) (x/base - 1)) ^ *)
(* (String.get alphabet (x mod base) |> String.make 1) *)
(* true if every element of la is in lb *)
let inclusion la lb =
let rec aux la =
function
[] -> true
| b::lb ->
List.mem b la && aux la lb
in
aux lb la
(* true if lb includes la and la includes lb *)
let equality la lb =
inclusion la lb && inclusion lb la
(* computes the result of la \setminus lb *)
let subtraction la lb =
let rec aux la =
function
[] -> la
| b::lb ->
aux (List.filter ((<>) b) la) lb
in
aux la lb
(* returns only the unique elements of l *)
let unique l =
let rec aux l acc =
match l with
| [] ->
List.rev acc
| h :: t ->
if List.mem h acc
then aux t acc
else aux t (h :: acc)
in
aux l []
(* returns the unique elements of the concat of the lists *)
let unique_union la lb =
la @ lb |> unique
(* returns all elements both in la and in lb *)
let unique_intersection la lb =
let rec aux la acc =
match la with
[] -> acc
| a::la ->
if List.mem a lb
then aux la (a::acc)
else aux la acc
in
aux la [] |> unique
(* given two lists of associations combines them and if an item is the same,
a provided function is applied to the associated values to create the new
association *)
let unique_union_assoc f l1 l2 =
let rec aux l acc =
match l with
| [] ->
acc
| (h1, h2) :: t ->
( match List.find_opt (fun (a, _) -> a = h1) acc with
| None -> aux t ((h1, h2) :: acc)
| Some (_h1, h3) -> aux
t
((h1, f h1 h2 h3) :: (List.remove_assoc h1 acc)) )
in
aux l2 (aux l1 [])
(* returns a list with at most n items and the rest in the second *)
let rec take (n: int) (l: 'a list) : ('a list * 'a list) =
if n = 0
then ([], l)
else
match l with
| [] -> ([], [])
| i::ls ->
let (t1, t2) = (take (n - 1) ls) in
((i :: t1), (t2))
(* takes a list and returns the same list without the first element;
different from List.tl since returns the empty list if there are not enough
items*)
let drop_first_element_list =
function
| [] -> []
| _::l -> l
(* retuns the last element of a list *)
let rec last_list l =
match l with
[] -> failwith "Utility.last_list, not enough items"
| [a] -> a
| _::ll -> last_list ll
(* combines two lists into a list of tuples; different from List.combine since
lengths do not need to be equal, the functions return a list with length
equal to the minimum of the input lists *)
let rec combine_twice la lb =
match (la, lb) with
| [], [] -> []
| [a], [b] -> [a, b]
| a::la, b::lb -> (a, b) :: (combine_twice la lb)
| _ -> []
>>>>>>> cfg

30
lib/utility/utility.mli
View File

@ -1,5 +1,31 @@
val pow : int -> int -> int
val pow : int -> int -> int
val powmod : int -> int -> int -> int
val fromIntToString : int -> string
val int_and : int -> int -> int
val int_or : int -> int -> int
val int_eq : int -> int -> int
val int_less : int -> int -> int
val int_less_eq : int -> int -> int
val int_more : int -> int -> int
val int_more_eq : int -> int -> int
val int_not : int -> int
(* val fromIntToString : string -> int -> string *)
val inclusion : 'a list -> 'a list -> bool
val equality : 'a list -> 'a list -> bool
val subtraction : 'a list -> 'a list -> 'a list
val unique_union : 'a list -> 'a list -> 'a list
val unique_intersection : 'a list -> 'a list -> 'a list
val unique_union_assoc : ('a -> 'b -> 'b -> 'b) -> ('a * 'b) list -> ('a * 'b) list -> ('a * 'b) list
val take : int -> 'a list -> ('a list * 'a list)
val drop_first_element_list : 'a list -> 'a list
val last_list : 'a list -> 'a
val combine_twice : 'a list -> 'b list -> ('a * 'b) list