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

Semantics for RISC code

Browse Source
This commit is contained in:
elvis
2024-12-03 17:18:42 +01:00
parent efa6ed21c9
commit 08a8d07422
20 changed files with 771 additions and 86 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
lib/miniImp/CfgImp.ml
View File

@ -179,13 +179,15 @@ and convert_a (prg: Types.a_exp) : SimpleStatements.simpleArithmetic =
| 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)
| 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 inputOutputVar = Some (i, o)}
let convert_io (prg: Types.p_exp) (i: int) : SSCfg.t =
let convert_io (i: int) (prg: Types.p_exp) : SSCfg.t =
let prg = ReplacePowerMod.rewrite_instructions prg in
{(convert prg) with inputVal = Some i}

2
lib/miniImp/CfgImp.mli
View File

@ -32,4 +32,4 @@ end
module SSCfg : Cfg.C with type elt = SimpleStatements.t
val convert : Types.p_exp -> SSCfg.t
val convert_io : Types.p_exp -> int -> SSCfg.t
val convert_io : int -> Types.p_exp -> SSCfg.t

79
lib/miniImp/CfgRISC.ml
View File

@ -1,6 +1,6 @@
module RISCSimpleStatements = struct
type register = {
index: int
index: string
}
type t =
@ -48,12 +48,12 @@ module RISCSimpleStatements = struct
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%d r%d => r%d" pp_brop b r1.index r2.index r3.index
| BImmOp (b, r1, i, r3) -> Printf.fprintf ppf "%a r%d %d => r%d" pp_biop b r1.index i r3.index
| URegOp (u, r1, r2) -> Printf.fprintf ppf "%a r%d => r%d" pp_urop u r1.index r2.index
| Load (r1, r2) -> Printf.fprintf ppf "Load r%d => r%d" r1.index r2.index
| LoadI (r2, i) -> Printf.fprintf ppf "LoadI %d => r%d" i r2.index
| Store (r1, r2) -> Printf.fprintf ppf "Store r%d => r%d" r1.index r2.index
| 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 (r2, i) -> 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"
@ -101,25 +101,34 @@ module RISCCfg = Cfg.Make(RISCSimpleStatements)
let globalcounter = ref 0
module RegisterMap = struct
type m = {
assignments: int Types.VariableMap.t
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 = !globalcounter},
{assignments = Types.VariableMap.add x !globalcounter m.assignments}))
| Some i -> ({index = i}, m)
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 = !globalcounter},
({index = string_of_int !globalcounter},
{assignments =
Types.VariableMap.add freshvariable !globalcounter m.assignments},
Types.VariableMap.add freshvariable
({index = string_of_int !globalcounter}: RISCSimpleStatements.register)
m.assignments},
freshvariable)
let empty : m =
@ -436,7 +445,7 @@ and c_ss_sa
match ss with
SimpleVariable (x) -> (
let r1, m = RegisterMap.get_or_set_register x m in
(convertedcode @ [Load (r1, register)], m)
(convertedcode @ [URegOp (Copy, r1, register)], m)
)
| SimpleInteger (i) -> (
(convertedcode @ [LoadI (register, i)], m)
@ -695,7 +704,9 @@ and c_ss_sa
(convertedcode @ [BRegOp (Pow, partialresreg1, partialresreg2, register)], m)
)
)
| SimplePowerMod (_a1, _a2, _a3) -> failwith "Not implemented Powermod"
| SimplePowerMod (_a1, _a2, _a3) -> (
failwith "not implemented"
)
| SimpleRand (a) -> (
let partialresreg, m, _partialresvar = RegisterMap.get_fresh_register m in
let convertedcode, m = c_ss_sa a m convertedcode partialresreg in
@ -713,9 +724,7 @@ let convert_ss
association between variables and registers so we choose a fold instead of
a mapreduce *)
let instructions, m = List.fold_left
(fun (convertedcode, m) code -> (
Printf.printf "considering: %a\n" CfgImp.SimpleStatements.pp code;
c_ss_t code m convertedcode))
(fun (convertedcode, m) code -> c_ss_t code m convertedcode)
([], m) value
in
(Cfg.NodeMap.add node instructions risccode, m)
@ -744,13 +753,23 @@ let convert (prg: CfgImp.SSCfg.t) : RISCCfg.t =
initial: Cfg.Node.t option;
terminal: Cfg.Node.t option;
content: CfgImp.SimpleStatements.t list Cfg.NodeMap.t
} -> { empty = empty;
nodes = nodes;
edges = edges;
reverseEdges = reverseEdges;
inputVal = inputVal;
inputOutputVar = inputOutputVar;
initial = initial;
terminal = terminal;
content = helper content RegisterMap.empty;
}
} ->
let initial_bindings =
match inputOutputVar with
| Some (i, o) ->
RegisterMap.empty |>
RegisterMap.set_register i {index = "in"} |>
RegisterMap.set_register o {index = "out"}
| None ->
RegisterMap.empty
in
{ empty = empty;
nodes = nodes;
edges = edges;
reverseEdges = reverseEdges;
inputVal = inputVal;
inputOutputVar = inputOutputVar;
initial = initial;
terminal = terminal;
content = helper content initial_bindings;
}

2
lib/miniImp/CfgRISC.mli
View File

@ -1,6 +1,6 @@
module RISCSimpleStatements : sig
type register = {
index: int
index: string
}
type t =

61
lib/miniImp/RISC.ml
View File

@ -6,11 +6,10 @@ let nextLabel () : string =
module RISCAssembly = struct
type register = {
index : int
index : string
}
type label =
string
type label = string
type risci =
| Nop
@ -56,20 +55,23 @@ module RISCAssembly = struct
| Copy
| Rand
type t = risci list
type t = {
code : risci list;
inputval: int option
}
let pp (ppf: out_channel) (t: t) : unit =
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%d r%d => r%d\n" pp_brop b r1.index r2.index r3.index
| BImmOp (b, r1, i, r3) -> Printf.fprintf ppf "\t%a r%d %d => r%d\n" pp_biop b r1.index i r3.index
| URegOp (u, r1, r2) -> Printf.fprintf ppf "\t%a r%d => r%d\n" pp_urop u r1.index r2.index
| Load (r1, r2) -> Printf.fprintf ppf "\tLoad r%d => r%d\n" r1.index r2.index
| LoadI (r2, i) -> Printf.fprintf ppf "\tLoadI %d => r%d\n" i r2.index
| Store (r1, r2) -> Printf.fprintf ppf "\tStore r%d => r%d\n" r1.index r2.index
| 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 (r2, i) -> 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%d => %s, %s\n" r.index l1 l2
| 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
@ -107,10 +109,18 @@ module RISCAssembly = struct
| Copy -> Printf.fprintf ppf "Copy"
| Rand -> Printf.fprintf ppf "Rand"
in
List.iter (pp_risci ppf) t
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 "Code:\n";
List.iter (pp_risci ppf) t.code
end
let convert_cfgrisc_risci (i: CfgRISC.RISCSimpleStatements.t list) : (RISCAssembly.t) =
let convert_cfgrisc_risci (i: CfgRISC.RISCSimpleStatements.t list) : (RISCAssembly.risci list) =
let rec helper (i: CfgRISC.RISCSimpleStatements.t) : RISCAssembly.risci =
match i with
| Nop -> Nop
@ -196,7 +206,7 @@ let rec helper
(prg: CfgRISC.RISCCfg.t)
(currentnode: Cfg.Node.t)
(alreadyVisited: Cfg.Node.t list)
: RISCAssembly.t * 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
@ -235,14 +245,14 @@ let rec helper
| BImmOp (_, _, _, r)
| URegOp (_, _, r)
| Load (_, r)
| LoadI (r, _) -> (([Label label1] : RISCAssembly.t) @
| LoadI (r, _) -> (([Label label1] : RISCAssembly.risci list) @
currentcode @
([CJump (r, label2, label3); Label label2] : RISCAssembly.t) @
([CJump (r, label2, label3); Label label2] : RISCAssembly.risci list) @
res1 @
([Jump label1; Label label3] : RISCAssembly.t) @
([Jump label1; Label label3] : RISCAssembly.risci list) @
res2
, vis2)
| _ -> failwith "Missing instruction"
| _ -> failwith "Missing instruction at branch"
else (* if branches, three labels are necessary *)
let label1 = nextLabel () in
let label2 = nextLabel () in
@ -257,19 +267,20 @@ let rec helper
| URegOp (_, _, r)
| Load (_, r)
| LoadI (r, _) -> (currentcode @
([CJump (r, label1, label2); Label label1] : RISCAssembly.t) @
([CJump (r, label1, label2); Label label1] : RISCAssembly.risci list) @
res1 @
([Jump label3; Label label2] : RISCAssembly.t) @
([Jump label3; Label label2] : RISCAssembly.risci list) @
res2 @
([Label label3] : RISCAssembly.t) @
([Label label3] : RISCAssembly.risci list) @
res3
, vis3)
| _ -> failwith "Missing instruction"
| _ -> failwith "Missing instruction at branch"
)
)
| None -> (currentcode, currentnode :: alreadyVisited)
)
let convert (prg: CfgRISC.RISCCfg.t) : RISCAssembly.t =
let res, _ = helper prg (Option.get prg.initial) [] in
res
{code = (helper prg (Option.get prg.initial) [] |> fst |>
List.append ([Label "main"] : RISCAssembly.risci list));
inputval = prg.inputVal}

10
lib/miniImp/RISC.mli
View File

@ -1,9 +1,9 @@
module RISCAssembly : sig
type register = {
index : int
index : string
}
type label
type label = string
type risci =
| Nop
| BRegOp of brop * register * register * register
@ -48,8 +48,12 @@ module RISCAssembly : sig
| Copy
| Rand
type t = risci list
type t = {
code : risci list;
inputval: int option
}
val pp_risci : out_channel -> risci -> unit
val pp : out_channel -> t -> unit
end

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

@ -0,0 +1,177 @@
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
}
end
let convert (prg: RISC.RISCAssembly.t) : RISC.RISCAssembly.risci list CodeMap.t =
let rec helper
(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 -> helper tl ([]) l
(CodeMap.union
(fun _ _ _ -> failwith "Two labels are the same")
(CodeMap.singleton current_label current)
map)
| instr :: tl -> helper tl (current @ [instr]) current_label map
in
match prg.code with
| Label "main" :: tl -> helper tl [] "main" CodeMap.empty
| _ -> failwith "Program should begind with label main"
let label_order (prg: RISC.RISCAssembly.t) : string list =
let rec helper
(prg: RISC.RISCAssembly.risci list)
: string list =
match prg with
[] -> []
| Label l :: tl -> l :: (helper tl)
| _ :: tl -> (helper tl)
in
helper (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 helper
(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
helper prg (CodeMap.find (List.nth lo (i+1)) prg.code) (List.nth lo (i+1))
else
prg
)
| Nop :: tl -> helper 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
helper {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
helper {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
helper {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
helper {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
helper {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
helper {prg with registers = RegisterMap.add {index = r3.index} n prg.registers} tl current_label
)
| LoadI (r1, i) :: tl -> (
let n = i
in
helper {prg with registers = RegisterMap.add {index = r1.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
helper {prg with memory = MemoryMap.add n1 n prg.memory} tl current_label
)
| Jump l :: _ -> helper 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
helper prg (CodeMap.find l1 prg.code) l1
else
helper prg (CodeMap.find l2 prg.code) l2
)
| Label _ :: tl -> helper prg tl current_label
in
RegisterMap.find
{index = "out"}
(helper prg (CodeMap.find "main" prg.code) "main").registers
let reduce (prg: RISC.RISCAssembly.t) : int =
reduce_instructions {code = convert prg;
registers =
RegisterMap.singleton
{index = "in"}
(Option.value prg.inputval ~default:0);
memory = MemoryMap.empty} (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

36
lib/miniImp/Types.ml
View File

@ -31,6 +31,42 @@ and a_exp =
| 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 rec helper_c (ppf) (c: c_exp) : unit =
match c with
Skip -> Format.fprintf ppf "Skip"
| Assignment (x, a) -> Format.fprintf ppf "%S := @[<h>%a@]" x helper_a a
| Sequence (c1, c2) -> Format.fprintf ppf "@[<hv>Sequence (@;<1 2>%a,@;<1 0>%a@;<0 0>)@]" helper_c c1 helper_c c2
| If (b, c1, c2) -> Format.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) -> Format.fprintf ppf "@[<hv>While @[<h>%a@] do@;<1 2>%a@]@;<0 0>" helper_b b helper_c c
| For (c1, b, c2, c3) -> Format.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) -> Format.fprintf ppf "%b" b
| BAnd (b1, b2) -> Format.fprintf ppf "(%a &&@;<1 2>%a)" helper_b b1 helper_b b2
| BOr (b1, b2) -> Format.fprintf ppf "(%a ||@;<1 2>%a)" helper_b b1 helper_b b2
| BNot (b) -> Format.fprintf ppf "(not %a)" helper_b b
| BCmp (a1, a2) -> Format.fprintf ppf "(%a ==@;<1 2>%a)" helper_a a1 helper_a a2
| BCmpLess (a1, a2) -> Format.fprintf ppf "(%a <@;<1 2>%a)" helper_a a1 helper_a a2
| BCmpLessEq (a1, a2) -> Format.fprintf ppf "(%a <=@;<1 2>%a)" helper_a a1 helper_a a2
| BCmpGreater (a1, a2) -> Format.fprintf ppf "(%a >@;<1 2>%a)" helper_a a1 helper_a a2
| BCmpGreaterEq (a1, a2) -> Format.fprintf ppf "(%a >=@;<1 2>%a)" helper_a a1 helper_a a2
and helper_a (ppf) (a: a_exp) =
match a with
Variable v -> Format.fprintf ppf "%S" v
| Integer n -> Format.fprintf ppf "%i" n
| Plus (a1, a2) -> Format.fprintf ppf "%a +@;<1 2>%a" helper_a a1 helper_a a2
| Minus (a1, a2) -> Format.fprintf ppf "%a -@;<1 2>%a" helper_a a1 helper_a a2
| Times (a1, a2) -> Format.fprintf ppf "%a *@;<1 2>%a" helper_a a1 helper_a a2
| Division (a1, a2) -> Format.fprintf ppf "%a /@;<1 2>%a" helper_a a1 helper_a a2
| Modulo (a1, a2) -> Format.fprintf ppf "%a %%@;<1 2>%a" helper_a a1 helper_a a2
| Power (a1, a2) -> Format.fprintf ppf "(%a ^@;<1 2>%a)" helper_a a1 helper_a a2
| PowerMod (a1, a2, a3) -> Format.fprintf ppf "(%a ^ %a %% %a)" helper_a a1 helper_a a2 helper_a a3
| Rand (a) -> Format.fprintf ppf "Rand (%a)" helper_a a
in
match p with
| Main (i, o, exp) ->
Format.fprintf ppf "def main with (input %S) (output %S) as @.%a" i o helper_c exp
module VariableMap = Map.Make(String)

1
lib/miniImp/Types.mli
View File

@ -31,6 +31,7 @@ and a_exp =
| 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

5
lib/miniImp/dune
View File

@ -10,7 +10,10 @@
(library
(name miniImp)
(public_name miniImp)
(modules Lexer Parser Types Semantics CfgImp CfgRISC RISC)
(modules Lexer Parser Types Semantics
CfgImp ReplacePowerMod
CfgRISC
RISC RISCSemantics)
(libraries cfg utility menhirLib))
(include_subdirs qualified)

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

@ -0,0 +1,246 @@
let rewrite_instructions (prg: Types.p_exp) : Types.p_exp =
(* function takes a program and replaces all occurrences of powermod with
simpler instructions *)
let i, o, prg = (
match prg with
| Main (i, o, exp) -> i, o, exp
) 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

28
lib/utility/utility.ml
View File

@ -12,6 +12,34 @@ 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 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
let rec fromIntToString (alphabet: string) (x: int) : string =
let base = String.length alphabet in
if x < 0 then

9
lib/utility/utility.mli
View File

@ -2,4 +2,13 @@ val pow : int -> int -> int
val powmod : int -> int -> int -> int
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