diff options
Diffstat (limited to 'minijazz')
34 files changed, 2585 insertions, 0 deletions
diff --git a/minijazz/mjc.byte b/minijazz/mjc.byte Binary files differnew file mode 100755 index 0000000..a07f380 --- /dev/null +++ b/minijazz/mjc.byte diff --git a/minijazz/src/README.txt b/minijazz/src/README.txt new file mode 100644 index 0000000..858383b --- /dev/null +++ b/minijazz/src/README.txt @@ -0,0 +1,18 @@ +**** Compilation ****** + +Pour compiler MiniJazz, utilisez la commande suivante: + > ocamlbuild mjc.byte + +**** Utilisation ********* + +Il suffit de lancer le compilateur en lui donnant un fichier .mj: + > ./mjc.byte test/nadder.mj +Cela genere un fichier test/nadder.net contennat une net-list non ordonnee. + +Pour obtenir les options du compilateur, utilisez l'option '-h': + > ./mjc.byte -h +Une option importante est -m qui doit etre suivi du nom du bloc principal du circuit. +Par defaut, le compilateur recherche un bloc appele 'main' + + +Pour la description du langage MiniJazz et du langage de net-list, voir le sujet du TP1. diff --git a/minijazz/src/_tags b/minijazz/src/_tags new file mode 100644 index 0000000..cffa4c6 --- /dev/null +++ b/minijazz/src/_tags @@ -0,0 +1,4 @@ +<global/dep.ml>: pkg_ocamlgraph +<**/*.{byte,native}>: use_unix, use_str, pkg_menhirLib, pkg_ocamlgraph +<global> or <parser> or <main> or <analysis> or <simulator> or <assembler> or <netlist> or <netlist_simulator>: include +true: use_menhir diff --git a/minijazz/src/analysis/callgraph.ml b/minijazz/src/analysis/callgraph.ml new file mode 100644 index 0000000..d1fab8f --- /dev/null +++ b/minijazz/src/analysis/callgraph.ml @@ -0,0 +1,198 @@ +open Ast +open Mapfold +open Static +open Static_utils +open Location +open Errors + +(** Inlines all nodes with static paramaters. *) + +let expect_bool env se = + let se = simplify env se in + match se.se_desc with + | SBool v -> v + | _ -> Format.eprintf "Expected a boolean@."; raise Error + +let expect_int env se = + let se = simplify env se in + match se.se_desc with + | SInt v -> v + | _ -> Format.eprintf "Expected an integer@."; raise Error + +let simplify_ty env ty = match ty with + | TBitArray se -> TBitArray (simplify env se) + | _ -> ty + +(** Find a node by name*) +let nodes_list = ref [] +let find_node f = + List.find (fun n -> f = n.n_name) !nodes_list + +let vars_of_pat env pat = + let exp_of_ident id = + try + let ty = IdentEnv.find id env in + mk_exp ~ty:ty (Evar id) + with + | Not_found -> Format.eprintf "Not in env: %a@." Ident.print_ident id; assert false + in + let rec _vars_of_pat acc pat = match pat with + | Evarpat id -> (exp_of_ident id)::acc + | Etuplepat l -> List.fold_left (fun acc id -> (exp_of_ident id)::acc) acc l + in + _vars_of_pat [] pat + +let ident_of_exp e = match e.e_desc with + | Evar x -> x + | _ -> assert false + +let rename env vd = + let e = mk_exp ~ty:vd.v_ty (Evar (Ident.copy vd.v_ident)) in + IdentEnv.add vd.v_ident e env + +let build_params m names values = + List.fold_left2 (fun m { p_name = n } v -> NameEnv.add n v m) m names values + +let build_exp m vds values = + List.fold_left2 (fun m { v_ident = n } e -> IdentEnv.add n e m) m vds values + +let build_env env vds = + List.fold_left (fun env vd -> IdentEnv.add vd.v_ident vd.v_ty env) env vds + +let rec find_local_vars b = match b with + | BEqs (_, vds) -> vds + | BIf (_, trueb, falseb) -> (find_local_vars trueb) @ (find_local_vars falseb) + +(** Substitutes idents with new names, static params with their values *) +let do_subst_block m subst b = + let translate_ident subst id = + try + ident_of_exp (IdentEnv.find id subst) + with + | Not_found -> id + in + let static_exp funs (subst, m) se = + simplify m se, (subst, m) + in + let exp funs (subst, m) e = + let e, _ = Mapfold.exp funs (subst, m) e in + match e.e_desc with + | Evar x -> + let e = if IdentEnv.mem x subst then IdentEnv.find x subst else e in + e, (subst, m) + | _ -> Mapfold.exp funs (subst, m) e + in + let pat funs (subst, m) pat = match pat with + | Evarpat id -> Evarpat (translate_ident subst id), (subst, m) + | Etuplepat ids -> Etuplepat (List.map (translate_ident subst) ids), (subst, m) + in + let var_dec funs (subst, m) vd = + (* iterate on the type *) + let vd, _ = Mapfold.var_dec funs (subst, m) vd in + { vd with v_ident = translate_ident subst vd.v_ident }, (subst, m) + in + let funs = + { Mapfold.defaults with static_exp = static_exp; exp = exp; + pat = pat; var_dec = var_dec } + in + let b, _ = Mapfold.block_it funs (subst, m) b in + b + +let check_params loc m param_names params cl = + let env = build_params NameEnv.empty param_names params in + let cl = List.map (simplify env) cl in + try + check_true m cl + with Unsatisfiable(c) -> + Format.eprintf "%aThe following constraint is not satisfied: %a@." + print_location loc Printer.print_static_exp c; + raise Error + +let rec inline_node loc env m call_stack f params args pat = + (* Check that the definition is sound *) + if List.mem (f, params) call_stack then ( + Format.eprintf "The definition of %s is circular.@." f; + raise Error + ); + let call_stack = (f, params)::call_stack in + + (* do the actual work *) + let n = find_node f in + check_params loc m n.n_params params n.n_constraints; + let m = build_params m n.n_params params in + let subst = build_exp IdentEnv.empty n.n_inputs args in + let subst = build_exp subst n.n_outputs (List.rev (vars_of_pat env pat)) in + let locals = find_local_vars n.n_body in + let subst = List.fold_left rename subst locals in + let b = do_subst_block m subst n.n_body in + let b = Normalize.block b in + b, call_stack + +and translate_eq env m subst call_stack (eqs, vds) ((pat, e) as eq) = + match e.e_desc with + (* Inline all nodes or only those with params or declared inline + if no_inline_all = true *) + | Ecall(f, params, args) -> + (try + let n = find_node f in + if not !Cli_options.no_inline_all + || not (Misc.is_empty params) + || n.n_inlined = Inlined then + let params = List.map (simplify m) params in + let b, call_stack = inline_node e.e_loc env m call_stack f params args pat in + let new_eqs, new_vds = translate_block env m subst call_stack b in + new_eqs@eqs, new_vds@vds + else + eq::eqs, vds + with + | Not_found -> eq::eqs, vds (* Predefined function*) + ) + | _ -> eq::eqs, vds + +and translate_eqs env m subst call_stack acc eqs = + List.fold_left (translate_eq env m subst call_stack) acc eqs + +and translate_block env m subst call_stack b = + match b with + | BEqs (eqs, vds) -> + let vds = List.map (fun vd -> { vd with v_ty = simplify_ty m vd.v_ty }) vds in + let env = build_env env vds in + translate_eqs env m subst call_stack ([], vds) eqs + | BIf(se, trueb, elseb) -> + if expect_bool m se then + translate_block env m subst call_stack trueb + else + translate_block env m subst call_stack elseb + +let node m n = + (*Init state*) + let call_stack = [(n.n_name, [])] in + (*Do the translation*) + let env = build_env IdentEnv.empty n.n_inputs in + let env = build_env env n.n_outputs in + let eqs, vds = translate_block env m IdentEnv.empty call_stack n.n_body in + { n with n_body = BEqs (eqs, vds) } + +let build_cd env cd = + NameEnv.add cd.c_name cd.c_value env + +let program p = + nodes_list := p.p_nodes; + let m = List.fold_left build_cd NameEnv.empty p.p_consts in + if !Cli_options.no_inline_all then ( + (* Find the nodes without static parameters *) + let nodes = List.filter (fun n -> Misc.is_empty n.n_params) p.p_nodes in + let nodes = List.map (fun n -> node m n) nodes in + { p with p_nodes = nodes } + ) else ( + try + let n = List.find (fun n -> n.n_name = !Cli_options.main_node) p.p_nodes in + if n.n_params <> [] then ( + Format.eprintf "The main node '%s' cannot have static parameters@." n.n_name; + raise Error + ); + { p with p_nodes = [node m n] } + with Not_found -> + Format.eprintf "Cannot find the main node '%s'@." !Cli_options.main_node; + raise Error + ) diff --git a/minijazz/src/analysis/normalize.ml b/minijazz/src/analysis/normalize.ml new file mode 100644 index 0000000..52db539 --- /dev/null +++ b/minijazz/src/analysis/normalize.ml @@ -0,0 +1,40 @@ +open Ast +open Mapfold + +let mk_eq e = + let id = Ident.fresh_ident "_l" in + let eq = (Evarpat id, e) in + let vd = mk_var_dec id e.e_ty in + Evar id, vd, eq + +(* Put all the arguments in separate equations *) +let exp funs (eqs, vds) e = match e.e_desc with + | Econst _ | Evar _ -> e, (eqs, vds) + | _ -> + let e, (eqs, vds) = Mapfold.exp funs (eqs, vds) e in + let desc, vd, eq = mk_eq e in + { e with e_desc = desc }, (eq::eqs, vd::vds) + +let equation funs (eqs, vds) (pat, e) = + match e.e_desc with + | Econst _ | Evar _ -> (pat, e), (eqs, vds) + | _ -> + let _, ((_, e)::eqs, _::vds) = Mapfold.exp_it funs (eqs, vds) e in + (pat, e), (eqs, vds) + +let block funs acc b = match b with + | BEqs(eqs, vds) -> + let eqs, (new_eqs, new_vds) = Misc.mapfold (Mapfold.equation_it funs) ([], []) eqs in + BEqs(new_eqs@eqs, new_vds@vds), acc + | BIf _ -> raise Mapfold.Fallback + +let program p = + let funs = { Mapfold.defaults with exp = exp; equation = equation; block = block } in + let p, _ = Mapfold.program_it funs ([], []) p in + p + +(* Used by Callgraph *) +let block b = + let funs = { Mapfold.defaults with exp = exp; equation = equation; block = block } in + let b, _ = Mapfold.block_it funs ([], []) b in + b diff --git a/minijazz/src/analysis/scoping.ml b/minijazz/src/analysis/scoping.ml new file mode 100644 index 0000000..0fefd5b --- /dev/null +++ b/minijazz/src/analysis/scoping.ml @@ -0,0 +1,99 @@ +open Ast +open Mapfold +open Static +open Static_utils +open Location +open Errors + +(** Simplifies static expression in the program. *) +let simplify_program p = + let const_dec funs cenv cd = + let v = subst cenv cd.c_value in + let cenv = NameEnv.add cd.c_name v cenv in + { cd with c_value = v }, cenv + in + let static_exp funs cenv se = + let se = subst cenv se in + (match se.se_desc with + | SVar id -> + (* Constants with se.se_loc = no_location are generated and should not be checked *) + if not (NameEnv.mem id cenv) && not (se.se_loc == no_location) then ( + Format.eprintf "%aThe constant name '%s' is unbound@." + print_location se.se_loc id; + raise Error + ) + | _ -> () + ); + se, cenv + in + let node_dec funs cenv nd = + let cenv' = + List.fold_left + (fun cenv p -> NameEnv.add p.p_name (mk_static_var p.p_name) cenv) + cenv nd.n_params + in + let nd, _ = Mapfold.node_dec funs cenv' nd in + nd, cenv + in + let funs = + { Mapfold.defaults with const_dec = const_dec; + static_exp = static_exp; node_dec = node_dec } + in + let p, _ = Mapfold.program_it funs NameEnv.empty p in + p + +(** Checks the name used in the program are defined. + Adds var_decs for all variables defined in a block. *) +let check_names p = + let rec pat_vars s pat = match pat with + | Evarpat id -> IdentSet.add id s + | Etuplepat ids -> List.fold_left (fun s id -> IdentSet.add id s) s ids + in + let build_set vds = + List.fold_left (fun s vd -> IdentSet.add vd.v_ident s) IdentSet.empty vds + in + let block funs (s, _) b = match b with + | BEqs(eqs, _) -> + let defnames = List.fold_left (fun s (pat, _) -> pat_vars s pat) IdentSet.empty eqs in + let ls = IdentSet.diff defnames s in (* remove outputs from the set *) + let vds = IdentSet.fold (fun id l -> (mk_var_dec id invalid_type)::l) ls [] in + let new_s = IdentSet.union s defnames in + let eqs,_ = Misc.mapfold (Mapfold.equation_it funs) (new_s, IdentSet.empty) eqs in + BEqs (eqs, vds), (s, defnames) + | BIf(se, trueb, falseb) -> + let trueb, (_, def_true) = Mapfold.block_it funs (s, IdentSet.empty) trueb in + let falseb, (_, def_false) = Mapfold.block_it funs (s, IdentSet.empty) falseb in + let defnames = IdentSet.inter def_true def_false in + BIf(se, trueb, falseb), (s, defnames) + in + let exp funs (s, defnames) e = match e.e_desc with + | Evar id -> + if not (IdentSet.mem id s) then ( + Format.eprintf "%aThe identifier '%a' is unbound@." + print_location e.e_loc Ident.print_ident id; + raise Error + ); + e, (s, defnames) + | _ -> Mapfold.exp funs (s, defnames) e + in + let node n = + let funs = { Mapfold.defaults with block = block; exp = exp } in + let s = build_set (n.n_inputs@n.n_outputs) in + let n_body, (_, defnames) = Mapfold.block_it funs (s, IdentSet.empty) n.n_body in + (* check for undefined outputs *) + let undefined_outputs = + List.filter (fun vd -> not (IdentSet.mem vd.v_ident defnames)) n.n_outputs + in + if undefined_outputs <> [] then ( + Format.eprintf "%aThe following outputs are not defined: %a@." + print_location n.n_loc Printer.print_var_decs undefined_outputs; + raise Error + ); + { n with n_body = n_body } + in + { p with p_nodes = List.map node p.p_nodes } + + +let program p = + let p = simplify_program p in + check_names p diff --git a/minijazz/src/analysis/simplify.ml b/minijazz/src/analysis/simplify.ml new file mode 100644 index 0000000..f7cbb5c --- /dev/null +++ b/minijazz/src/analysis/simplify.ml @@ -0,0 +1,42 @@ +open Ast +open Static + +let is_not_zero ty = match ty with + | TBitArray { se_desc = SInt 0 } -> false + | _ -> true + +let rec simplify_exp e = match e.e_desc with + (* replace x[i..j] with [] if j < i *) + | Ecall("slice", + [{ se_desc = SInt min }; + { se_desc = SInt max }; n], _) when max < min -> + { e with e_desc = Econst (VBitArray (Array.make 0 false)) } + (* replace x[i..i] with x[i] *) + | Ecall("slice", [min; max; n], args) when min = max -> + let new_e = { e with e_desc = Ecall("select", [min; n], args) } in + simplify_exp new_e + (* replace x.[] or [].x with x *) + | Ecall("concat", _, [{ e_ty = TBitArray { se_desc = SInt 0 } }; e1]) + | Ecall("concat", _, [e1; { e_ty = TBitArray { se_desc = SInt 0 } }]) -> + e1 + | Ecall(f, params, args) -> + { e with e_desc = Ecall(f, params, List.map simplify_exp args) } + | _ -> e + +let simplify_eq (pat,e) = + (pat, simplify_exp e) + +let rec block b = match b with + | BEqs(eqs, vds) -> + let eqs = List.map simplify_eq eqs in + (* remove variables with size 0 *) + let vds = List.filter (fun vd -> is_not_zero vd.v_ty) vds in + let eqs = List.filter (fun (_, e) -> is_not_zero e.e_ty) eqs in + BEqs(eqs, vds) + | BIf(se, trueb, elseb) -> BIf(se, block trueb, block elseb) + +let node n = + { n with n_body = block n.n_body } + +let program p = + { p with p_nodes = List.map node p.p_nodes } diff --git a/minijazz/src/analysis/typing.ml b/minijazz/src/analysis/typing.ml new file mode 100644 index 0000000..0212b95 --- /dev/null +++ b/minijazz/src/analysis/typing.ml @@ -0,0 +1,375 @@ +open Ast +open Static +open Static_utils +open Printer +open Errors +open Misc +open Mapfold + +exception Unify + +type error_kind = + | Args_arity_error of int * int + | Params_arity_error of int * int + | Result_arity_error of int * int + | Type_error of ty * ty + | Static_type_error of static_ty * static_ty + | Static_constraint_false of static_exp + +exception Typing_error of error_kind + +let error k = raise (Typing_error k) + +let message loc err = match err with + | Args_arity_error (found, expected) -> + Format.eprintf "%aWrong number of arguments (found '%d'; expected '%d')@." + Location.print_location loc found expected + | Result_arity_error (found, expected) -> + Format.eprintf "%aWrong number of outputs (found '%d'; expected '%d')@." + Location.print_location loc found expected + | Params_arity_error (found, expected) -> + Format.eprintf "%aWrong number of static parameters (found '%d'; expected '%d')@." + Location.print_location loc found expected + | Type_error (found_ty, exp_ty) -> + Format.eprintf "%aThis expression has type '%a' but '%a' was expected@." + Location.print_location loc print_type found_ty print_type exp_ty + | Static_type_error (found_ty, exp_ty) -> + Format.eprintf "%aThis static expression has type '%a' but '%a' was expected@." + Location.print_location loc print_static_type found_ty print_static_type exp_ty + | Static_constraint_false se -> + Format.eprintf "%aThe following constraint is not satisfied: %a@." + Location.print_location loc print_static_exp se + + +type signature = + { s_inputs : ty list; + s_outputs : ty list; + s_params : name list; + s_constraints : static_exp list } + +module Modules = struct + let env = ref Ast.NameEnv.empty + + let add_sig ?(params = []) ?(constr = []) n inp outp = + let s = { s_inputs = inp; s_outputs = outp; s_params = params; s_constraints = constr } in + env := Ast.NameEnv.add n s !env + + let _ = + add_sig "and" [TBit;TBit] [TBit]; + add_sig "xor" [TBit;TBit] [TBit]; + add_sig "or" [TBit;TBit] [TBit]; + add_sig "not" [TBit] [TBit]; + add_sig "reg" [TBit] [TBit]; + add_sig "mux" [TBit;TBit;TBit] [TBit]; + add_sig ~params:["n"] "print" [TBitArray (mk_static_var "n"); TBit] [TBit]; + add_sig ~params:["n"] "input" [TBit] [TBitArray (mk_static_var "n")]; + let constr1 = mk_static_exp (SBinOp(SLess, mk_static_var "i", mk_static_var "n")) in + let constr2 = mk_static_exp (SBinOp(SLeq, mk_static_int 0, mk_static_var "i")) in + add_sig ~params:["i"; "n"] + ~constr:[constr1; constr2] + "select" [TBitArray (mk_static_var "n")] [TBit]; + let add = mk_static_exp (SBinOp(SAdd, mk_static_var "n1", mk_static_var "n2")) in + add_sig ~params:["n1"; "n2"; "n3"] + ~constr:[mk_static_exp (SBinOp (SEqual, mk_static_var "n3", add))] + "concat" [TBitArray (mk_static_var "n1"); TBitArray (mk_static_var "n2")] + [TBitArray (mk_static_var "n3")]; + (* slice : size = min <= max ? max - min + 1 : 0 *) + let size = + mk_static_exp + (SBinOp(SAdd, + mk_static_exp (SBinOp(SMinus, mk_static_var "max", mk_static_var "min")), + mk_static_int 1)) + in + let size = + mk_static_exp (SIf (mk_static_exp (SBinOp(SLeq, mk_static_var "min", mk_static_var "max")), + size, mk_static_int 0)) + in + let constr1 = mk_static_exp (SBinOp(SLeq, mk_static_int 0, mk_static_var "min")) in + let constr2 = mk_static_exp (SBinOp(SLess, mk_static_var "max", mk_static_var "n")) in + add_sig ~params:["min"; "max"; "n"] ~constr:[constr1; constr2] "slice" + [TBitArray (mk_static_var "n")] [TBitArray size] + + + let tys_of_vds vds = List.map (fun vd -> vd.v_ty) vds + + let add_node n constr = + let s = { s_inputs = tys_of_vds n.n_inputs; + s_outputs = tys_of_vds n.n_outputs; + s_params = List.map (fun p -> p.p_name) n.n_params; + s_constraints = constr } in + env := Ast.NameEnv.add n.n_name s !env + + let build_param_env param_names params = + List.fold_left2 + (fun env pn p -> NameEnv.add pn p env) + NameEnv.empty param_names params + + let subst_ty env ty = match ty with + | TBitArray se -> TBitArray (subst env se) + | _ -> ty + + let find_node n params = + try + let s = Ast.NameEnv.find n !env in + if List.length s.s_params <> List.length params then + error (Params_arity_error (List.length params, List.length s.s_params)); + let env = build_param_env s.s_params params in + let s = + { s with s_inputs = List.map (subst_ty env) s.s_inputs; + s_outputs = List.map (subst_ty env) s.s_outputs; + s_constraints = List.map (subst env) s.s_constraints } + in + s + with Not_found -> + Format.eprintf "Unbound node '%s'@." n; + raise Error +end + +let constr_list = ref [] +let add_constraint se = + constr_list := se :: !constr_list +let set_constraints cl = + constr_list := cl +let get_constraints () = + let v = !constr_list in + constr_list := []; v + +let fresh_static_var () = + SVar ("s_"^(Misc.gen_symbol ())) + +(* Functions on types*) + +let fresh_type = + let index = ref 0 in + let gen_index () = (incr index; !index) in + let fresh_type () = TVar (ref (TIndex (gen_index ()))) in + fresh_type + +(** returns the canonic (short) representant of [ty] + and update it to this value. *) +let rec ty_repr ty = match ty with + | TVar link -> + (match !link with + | TLink ty -> + let ty = ty_repr ty in + link := TLink ty; + ty + | _ -> ty) + | _ -> ty + +(** verifies that index is fresh in ck. *) +let rec occur_check index ty = + let ty = ty_repr ty in + match ty with + | TUnit | TBit | TBitArray _ -> () + | TVar { contents = TIndex n } when index <> n -> () + | TProd ty_list -> List.iter (occur_check index) ty_list + | _ -> raise Unify + +let rec unify ty1 ty2 = + let ty1 = ty_repr ty1 in + let ty2 = ty_repr ty2 in + if ty1 == ty2 then () + else + match (ty1, ty2) with + | TBitArray n, TBit | TBit, TBitArray n -> + add_constraint (mk_static_exp (SBinOp(SEqual, n, mk_static_int 1))) + | TBitArray n1, TBitArray n2 -> + add_constraint (mk_static_exp (SBinOp(SEqual, n1, n2))) + | TVar { contents = TIndex n1 }, TVar { contents = TIndex n2 } when n1 = n2 -> () + | TProd ty_list1, TProd ty_list2 -> + if List.length ty_list1 <> List.length ty_list2 then + error (Result_arity_error (List.length ty_list1, List.length ty_list2)); + List.iter2 unify ty_list1 ty_list2 + | TVar ({ contents = TIndex n } as link), ty + | ty, TVar ({ contents = TIndex n } as link) -> + occur_check n ty; + link := TLink ty + | _ -> raise Unify + +let prod ty_list = match ty_list with + | [ty] -> ty + | _ -> TProd ty_list + +(* Typing of static exps *) +let rec type_static_exp se = match se.se_desc with + | SInt _ | SVar _ -> STInt + | SBool _ -> STBool + | SBinOp((SAdd | SMinus | SMult | SDiv | SPower ), se1, se2) -> + expect_static_exp se1 STInt; + expect_static_exp se2 STInt; + STInt + | SBinOp((SEqual | SLess | SLeq | SGreater | SGeq), se1, se2) -> + expect_static_exp se1 STInt; + expect_static_exp se2 STInt; + STBool + | SIf (c, se1, se2) -> + expect_static_exp se1 STBool; + let ty1 = type_static_exp se1 in + expect_static_exp se2 ty1; + ty1 + +and expect_static_exp se ty = + let found_ty = type_static_exp se in + if found_ty <> ty then + error (Static_type_error (found_ty, ty)) + +let rec simplify_constr cl = match cl with + | [] -> [] + | c::cl -> + let c' = simplify NameEnv.empty c in + match c'.se_desc with + | SBool true -> simplify_constr cl + | SBool false -> error (Static_constraint_false c) + | _ -> c::(simplify_constr cl) + +let rec find_simplification_one c = match c.se_desc with + | SBinOp(SEqual, { se_desc = SVar s }, se) + | SBinOp(SEqual, se, { se_desc = SVar s }) -> + Some (s, se) + | SIf(_, se1, { se_desc = SBool true }) + | SIf(_, { se_desc = SBool true }, se1) -> + find_simplification_one se1 + | _ -> None + +let rec find_simplification params cl = match cl with + | [] -> None, [] + | c::cl -> + (match find_simplification_one c with + | Some (s, se) when not (List.mem s params) -> + Some (s, se), cl + | _ -> + let res, cl = find_simplification params cl in + res, c::cl) + +let solve_constr params cl = + let params = List.map (fun p -> p.p_name) params in + let subst_and_error env c = + let c' = subst env c in + match c'.se_desc with + | SBool false -> error (Static_constraint_false c) + | _ -> c' + in + let env = ref NameEnv.empty in + let rec solve_one cl = + let res, cl = find_simplification params cl in + match res with + | None -> cl + | Some (s, se) -> + env := NameEnv.add s se !env; + let cl = List.map (subst_and_error !env) cl in + solve_one cl + in + let cl = simplify_constr cl in + let cl = solve_one cl in + cl, !env + +(* Typing of expressions *) +let rec type_exp env e = + try + let desc, ty = match e.e_desc with + | Econst (VBit _) -> e.e_desc, TBit + | Econst (VBitArray a) -> e.e_desc, TBitArray (mk_static_int (Array.length a)) + | Evar id -> Evar id, IdentEnv.find id env + | Ereg e -> + let e = expect_exp env e TBit in + Ereg e, TBit + | Emem (MRom, addr_size, word_size, file, args) -> + (* addr_size > 0 *) + add_constraint (mk_static_exp (SBinOp (SLess, mk_static_int 0, addr_size))); + let read_addr = assert_1 args in + let read_addr = expect_exp env read_addr (TBitArray addr_size) in + Emem (MRom, addr_size, word_size, file, [read_addr]), TBitArray word_size + | Emem (MRam, addr_size, word_size, file, args) -> + (* addr_size > 0 *) + add_constraint (mk_static_exp (SBinOp (SLess, mk_static_int 0, addr_size))); + let read_addr, write_en, write_addr, data_in = assert_4 args in + let read_addr = expect_exp env read_addr (TBitArray addr_size) in + let write_addr = expect_exp env write_addr (TBitArray addr_size) in + let data_in = expect_exp env data_in (TBitArray word_size) in + let write_en = expect_exp env write_en TBit in + let args = [read_addr; write_en; write_addr; data_in] in + Emem (MRam, addr_size, word_size, file, args), TBitArray word_size + | Ecall (f, params, args) -> + let s = Modules.find_node f params in + (*check arity*) + if List.length s.s_inputs <> List.length args then + error (Args_arity_error (List.length args, List.length s.s_inputs)); + (*check types of all arguments*) + let args = List.map2 (expect_exp env) args s.s_inputs in + List.iter add_constraint s.s_constraints; + Ecall(f, params, args), prod s.s_outputs + in + { e with e_desc = desc; e_ty = ty }, ty + with + | Typing_error k -> message e.e_loc k; raise Error + +and expect_exp env e ty = + let e, found_ty = type_exp env e in + try + unify ty found_ty; + e + with + Unify -> error (Type_error (found_ty, ty)) + +let type_pat env pat = match pat with + | Evarpat x -> IdentEnv.find x env + | Etuplepat id_list -> prod (List.map (fun x -> IdentEnv.find x env) id_list) + +let type_eq env (pat, e) = + let pat_ty = type_pat env pat in + let e = expect_exp env e pat_ty in + (pat, e) + +let build env vds = + let build_one env vd = IdentEnv.add vd.v_ident vd.v_ty env in + List.fold_left build_one env vds + +let rec type_block env b = match b with + | BEqs(eqs, vds) -> + let vds = List.map (fun vd -> { vd with v_ty = fresh_type () }) vds in + let env = build env vds in + let eqs = List.map (type_eq env) eqs in + BEqs(eqs,vds) + | BIf(se, trueb, falseb) -> + expect_static_exp se STBool; + let prev_constr = get_constraints () in + let trueb = type_block env trueb in + let true_constr = + List.map (fun c -> mk_static_exp (SIf (se, c, mk_static_bool true))) (get_constraints ()) + in + let falseb = type_block env falseb in + let false_constr = + List.map (fun c -> mk_static_exp (SIf (se, mk_static_bool true, c))) (get_constraints ()) + in + set_constraints (prev_constr @ true_constr @ false_constr); + BIf(se, trueb, falseb) + +let ty_repr_block env b = + let static_exp funs acc se = simplify env se, acc in + let ty funs acc ty = + let ty = ty_repr ty in + (* go through types to substitute static exps *) + Mapfold.ty funs acc ty + in + let funs = { Mapfold.defaults with ty = ty; static_exp = static_exp } in + let b, _ = Mapfold.block_it funs () b in + b + +let node n = + try + Modules.add_node n []; + let env = build IdentEnv.empty n.n_inputs in + let env = build env n.n_outputs in + let body = type_block env n.n_body in + let constr = get_constraints () in + let constr, env = solve_constr n.n_params constr in + let body = ty_repr_block env body in + Modules.add_node n constr; + { n with n_body = body; n_constraints = constr } + with + Typing_error k -> message n.n_loc k; raise Error + +let program p = + let p_nodes = List.map node p.p_nodes in + { p with p_nodes = p_nodes } diff --git a/minijazz/src/global/_tags b/minijazz/src/global/_tags new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/minijazz/src/global/_tags diff --git a/minijazz/src/global/ast.ml b/minijazz/src/global/ast.ml new file mode 100644 index 0000000..cc29486 --- /dev/null +++ b/minijazz/src/global/ast.ml @@ -0,0 +1,107 @@ +open Location +open Static + +type ident = Ident.t +type name = string + +module IdentEnv = Map.Make (struct type t = ident let compare = compare end) +module IdentSet = Set.Make (struct type t = ident let compare = compare end) + +module NameEnv = Map.Make (struct type t = name let compare = compare end) +module NameSet = Set.Make (struct type t = name let compare = compare end) + +type ty = + | TUnit | TBit | TBitArray of static_exp | TProd of ty list + | TVar of link ref +and link = + | TIndex of int + | TLink of ty +let invalid_type = TUnit + +type mem_kind = MRom | MRam + +type value = + | VBit of bool + | VBitArray of bool array + +type edesc = + | Econst of value + | Evar of ident + | Ereg of exp + | Ecall of name * static_exp list * exp list + (* function * params * args *) + | Emem of mem_kind * static_exp * static_exp * string option * exp list + (* ro * address size * word size * input file * args *) + +and exp = { + e_desc : edesc; + e_ty : ty; + e_loc: location; +} + +type pat = + | Evarpat of ident + | Etuplepat of ident list + +type equation = pat * exp + +type var_dec = { + v_ident : ident; + v_ty : ty; +} + +type param = { + p_name : name; +} + +type block = + | BEqs of equation list * var_dec list + | BIf of static_exp * block * block + +type inlined_status = Inlined | NotInlined + +type node_dec = { + n_name : name; + n_loc: location; + n_inlined : inlined_status; + n_inputs : var_dec list; + n_outputs : var_dec list; + n_params : param list; + n_constraints : static_exp list; + n_body : block; + n_probes : ident list; +} + +type const_dec = { + c_name : name; + c_loc : location; + c_value : static_exp; +} + +type program = { + p_consts : const_dec list; + p_nodes : node_dec list; +} + + +let mk_exp ?(loc = no_location) ?(ty = invalid_type) desc = + { e_desc = desc; e_loc = loc; e_ty = ty } + +let mk_const_dec ?(loc = no_location) n se = + { c_name = n; c_loc = loc; c_value = se } + +let mk_equation pat e = (pat, e) + +let mk_var_dec n ty = + { v_ident = n; v_ty = ty } + +let mk_param n = + { p_name = n } + +let mk_node n loc inlined inputs outputs params b probes = + { n_name = n; n_inputs = inputs; n_outputs = outputs; + n_body = b; n_params = params; n_constraints = []; + n_loc = loc; n_inlined = inlined; n_probes = probes } + +let mk_program cds nds = + { p_consts = cds; p_nodes = nds } diff --git a/minijazz/src/global/errors.ml b/minijazz/src/global/errors.ml new file mode 100644 index 0000000..9f64d36 --- /dev/null +++ b/minijazz/src/global/errors.ml @@ -0,0 +1,22 @@ +open Location + +exception Error + +type lexical_error = + | Illegal_character + | Unterminated_comment + | Bad_char_constant + | Unterminated_string + +let lexical_error err loc = + Format.eprintf (match err with + | Illegal_character -> Pervasives.format_of_string "%aIllegal character.@." + | Unterminated_comment -> "%aUnterminated comment.@." + | Bad_char_constant -> "%aBad char constant.@." + | Unterminated_string -> "%aUnterminated string.@." + ) print_location loc; + raise Error + +let syntax_error loc = + Format.eprintf "%aSyntax error.@." print_location loc; + raise Error diff --git a/minijazz/src/global/ident.ml b/minijazz/src/global/ident.ml new file mode 100644 index 0000000..9e36549 --- /dev/null +++ b/minijazz/src/global/ident.ml @@ -0,0 +1,39 @@ + +type t = { + i_id : int; + i_name : string; + i_from_source : bool +} + +let string_of_ident id = + if id.i_from_source then + id.i_name + else + id.i_name^"_"^(string_of_int id.i_id) + +let print_ident ff id = + Format.fprintf ff "%s" (string_of_ident id) + +module StringEnv = Map.Make (struct type t = string let compare = compare end) + +let ident_counter = ref 0 +let fresh_ident from_source s = + incr ident_counter; + { i_id = !ident_counter; i_name = s; i_from_source = from_source } + +let copy id = + fresh_ident false (string_of_ident id) + +let symbol_table = ref StringEnv.empty +let reset_symbol_table () = + symbol_table := StringEnv.empty +let ident_of_string s = + if StringEnv.mem s !symbol_table then + StringEnv.find s !symbol_table + else ( + let id = fresh_ident true s in + symbol_table := StringEnv.add s id !symbol_table; + id + ) + +let fresh_ident = fresh_ident false diff --git a/minijazz/src/global/location.ml b/minijazz/src/global/location.ml new file mode 100644 index 0000000..1837584 --- /dev/null +++ b/minijazz/src/global/location.ml @@ -0,0 +1,130 @@ +(* Printing a location in the source program *) +(* inspired from the source of the Caml Light 0.73 compiler *) + +open Lexing +open Parsing +open Format + +(* two important global variables: [input_name] and [input_chan] *) +type location = + Loc of position (* Position of the first character *) + * position (* Position of the next character following the last one *) + + +let input_name = ref "" (* Input file name. *) + +let input_chan = ref stdin (* The channel opened on the input. *) + +let initialize iname ic = + input_name := iname; + input_chan := ic + + +let no_location = Loc (dummy_pos, dummy_pos) + +let error_prompt = ">" + + +(** Prints [n] times char [c] on [oc]. *) +let prints_n_chars ff n c = for i = 1 to n do pp_print_char ff c done + +(** Prints out to [oc] a line designed to be printed under [line] from file [ic] + underlining from char [first] to char [last] with char [ch]. + [line] is the index of the first char of line. *) +let underline_line ic ff ch line first last = + let c = ref ' ' + and f = ref first + and l = ref (last-first) in + ( try + seek_in ic line; + pp_print_string ff error_prompt; + while c := input_char ic; !c != '\n' do + if !f > 0 then begin + f := !f - 1; + pp_print_char ff (if !c == '\t' then !c else ' ') + end + else if !l > 0 then begin + l := !l - 1; + pp_print_char ff (if !c == '\t' then !c else ch) + end + else () + done + with End_of_file -> + if !f = 0 && !l > 0 then prints_n_chars ff 5 ch ) + + +let copy_lines nl ic ff prompt = + for i = 1 to nl do + pp_print_string ff prompt; + (try pp_print_string ff (input_line ic) + with End_of_file -> pp_print_string ff "<EOF>"); + fprintf ff "@\n" + done + +let copy_chunk p1 p2 ic ff = + try for i = p1 to p2 - 1 do pp_print_char ff (input_char ic) done + with End_of_file -> pp_print_string ff "<EOF>" + + + +let skip_lines n ic = + try for i = 1 to n do + let _ = input_line ic in () + done + with End_of_file -> () + + + +let print_location ff (Loc(p1,p2)) = + let n1 = p1.pos_cnum - p1.pos_bol in (* character number *) + let n2 = p2.pos_cnum - p2.pos_bol in + let np1 = p1.pos_cnum in (* character position *) + let np2 = p2.pos_cnum in + let l1 = p1.pos_lnum in (* line number *) + let l2 = p2.pos_lnum in + let lp1 = p1.pos_bol in (* line position *) + let lp2 = p2.pos_bol in + let f1 = p1.pos_fname in (* file name *) + let f2 = p2.pos_fname in + + if f1 != f2 then (* Strange case *) + fprintf ff + "File \"%s\" line %d, character %d, to file \"%s\" line %d, character %d@." + f1 l1 n1 f2 l2 n2 + + else begin (* Same file *) + if l2 > l1 then + fprintf ff + "File \"%s\", line %d-%d, characters %d-%d:@\n" f1 l1 l2 n1 n2 + else + fprintf ff "File \"%s\", line %d, characters %d-%d:@\n" f1 l1 n1 n2; + (* Output source code *) + try + let ic = open_in f1 in + + if l1 == l2 then ( + (* Only one line : copy full line and underline *) + seek_in ic lp1; + copy_lines 1 ic ff ">"; + underline_line ic ff '^' lp1 n1 n2 ) + else ( + underline_line ic ff '.' lp1 0 n1; (* dots until n1 *) + seek_in ic np1; + (* copy the end of the line l1 after the dots *) + copy_lines 1 ic ff ""; + if l2 - l1 <= 8 then + (* copy the 6 or less middle lines *) + copy_lines (l2-l1-1) ic ff ">" + else ( + (* sum up the middle lines to 6 *) + copy_lines 3 ic ff ">"; + fprintf ff "..........@\n"; + skip_lines (l2-l1-7) ic; (* skip middle lines *) + copy_lines 3 ic ff ">" + ); + fprintf ff ">"; + copy_chunk lp2 np2 ic ff; (* copy interesting begining of l2 *) + ) + with Sys_error _ -> (); + end; + fprintf ff "@." diff --git a/minijazz/src/global/mapfold.ml b/minijazz/src/global/mapfold.ml new file mode 100644 index 0000000..50ffbaf --- /dev/null +++ b/minijazz/src/global/mapfold.ml @@ -0,0 +1,164 @@ +open Ast +open Static +open Misc + +exception Fallback + +type 'a it_funs = { + static_exp : 'a it_funs -> 'a -> static_exp -> static_exp * 'a; + static_exp_desc : 'a it_funs -> 'a -> static_exp_desc -> static_exp_desc * 'a; + ty : 'a it_funs -> 'a -> ty -> ty * 'a; + link : 'a it_funs -> 'a -> link -> link * 'a; + edesc : 'a it_funs -> 'a -> edesc -> edesc * 'a; + exp : 'a it_funs -> 'a -> exp -> exp * 'a; + pat : 'a it_funs -> 'a -> pat -> pat * 'a; + equation : 'a it_funs -> 'a -> equation -> equation * 'a; + var_dec : 'a it_funs -> 'a -> var_dec -> var_dec * 'a; + block : 'a it_funs -> 'a -> block -> block * 'a; + node_dec : 'a it_funs -> 'a -> node_dec -> node_dec * 'a; + const_dec : 'a it_funs -> 'a -> const_dec -> const_dec * 'a; + program : 'a it_funs -> 'a -> program -> program * 'a; +} + +let rec exp_it funs acc e = funs.exp funs acc e +and exp funs acc e = + let e_desc, acc = edesc_it funs acc e.e_desc in + let e_ty, acc = ty_it funs acc e.e_ty in + { e with e_desc = e_desc; e_ty = e_ty }, acc + +and edesc_it funs acc ed = + try funs.edesc funs acc ed + with Fallback -> edesc funs acc ed +and edesc funs acc ed = match ed with + | Econst v -> Econst v, acc + | Evar id -> Evar id, acc + | Ereg e -> + let e, acc = exp_it funs acc e in + Ereg e, acc + | Emem(k, addr_size, word_size, s, args) -> + let addr_size, acc = static_exp_it funs acc addr_size in + let word_size, acc = static_exp_it funs acc word_size in + let args, acc = mapfold (exp_it funs) acc args in + Emem(k, addr_size, word_size, s, args), acc + | Ecall(id, params, args) -> + let params, acc = mapfold (static_exp_it funs) acc params in + let args, acc = mapfold (exp_it funs) acc args in + Ecall(id, params, args), acc + +and static_exp_it funs acc sd = + try funs.static_exp funs acc sd + with Fallback -> static_exp funs acc sd +and static_exp funs acc se = + let se_desc, acc = static_exp_desc_it funs acc se.se_desc in + { se with se_desc = se_desc }, acc + +and static_exp_desc_it funs acc sed = + try funs.static_exp_desc funs acc sed + with Fallback -> static_exp_desc funs acc sed +and static_exp_desc funs acc sed = match sed with + | SInt _ | SBool _ | SVar _ -> sed, acc + | SBinOp (sop, se1, se2) -> + let se1, acc = static_exp_it funs acc se1 in + let se2, acc = static_exp_it funs acc se2 in + SBinOp(sop, se1, se2), acc + | SIf(c, se1, se2) -> + let c, acc = static_exp_it funs acc c in + let se1, acc = static_exp_it funs acc se1 in + let se2, acc = static_exp_it funs acc se2 in + SIf(c, se1, se2), acc + +and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t +and ty funs acc t = match t with + | TUnit | TBit -> t, acc + | TBitArray se -> + let se, acc = static_exp_it funs acc se in + TBitArray se, acc + | TProd t_l -> + let t_l, acc = mapfold (ty_it funs) acc t_l in + TProd t_l, acc + | TVar link -> + let link_v, acc = link_it funs acc !link in + link := link_v; + TVar link, acc + +and link_it funs acc c = + try funs.link funs acc c + with Fallback -> link funs acc c +and link funs acc l = match l with + | TIndex _ -> l, acc + | TLink ty -> + let ty, acc = ty_it funs acc ty in + TLink ty, acc + +and pat_it funs acc p = + try funs.pat funs acc p + with Fallback -> pat funs acc p +and pat funs acc p = p, acc + +and equation_it funs acc eq = funs.equation funs acc eq +and equation funs acc (pat, e) = + let pat, acc = pat_it funs acc pat in + let e, acc = exp_it funs acc e in + (pat, e), acc + +and block_it funs acc b = + try funs.block funs acc b + with Fallback -> block funs acc b +and block funs acc b = match b with + | BEqs(eqs, vds) -> + let vds, acc = mapfold (var_dec_it funs) acc vds in + let eqs, acc = mapfold (equation_it funs) acc eqs in + BEqs (eqs, vds), acc + | BIf(se, b1, b2) -> + let se, acc = static_exp_it funs acc se in + let b1, acc = block_it funs acc b1 in + let b2, acc = block_it funs acc b2 in + BIf(se, b1, b2), acc + +and var_dec_it funs acc vd = funs.var_dec funs acc vd +and var_dec funs acc vd = + let v_ty, acc = ty_it funs acc vd.v_ty in + { vd with v_ty = v_ty }, acc + + +and node_dec_it funs acc nd = funs.node_dec funs acc nd +and node_dec funs acc nd = + let n_inputs, acc = mapfold (var_dec_it funs) acc nd.n_inputs in + let n_outputs, acc = mapfold (var_dec_it funs) acc nd.n_outputs in + let n_constraints, acc = mapfold (static_exp_it funs) acc nd.n_constraints in + let n_body, acc = block_it funs acc nd.n_body in + { nd with + n_inputs = n_inputs; + n_outputs = n_outputs; + n_body = n_body; + n_constraints = n_constraints } + , acc + + +and const_dec_it funs acc c = funs.const_dec funs acc c +and const_dec funs acc c = + let c_value, acc = static_exp_it funs acc c.c_value in + { c with c_value = c_value }, acc + +and program_it funs acc p = funs.program funs acc p +and program funs acc p = + let p_consts, acc = mapfold (const_dec_it funs) acc p.p_consts in + let p_nodes, acc = mapfold (node_dec_it funs) acc p.p_nodes in + { p_nodes = p_nodes; p_consts = p_consts }, acc + + +let defaults = { + static_exp = static_exp; + static_exp_desc = static_exp_desc; + ty = ty; + link = link; + edesc = edesc; + exp = exp; + pat = pat; + equation = equation; + var_dec = var_dec; + block = block; + node_dec = node_dec; + const_dec = const_dec; + program = program; +} diff --git a/minijazz/src/global/misc.ml b/minijazz/src/global/misc.ml new file mode 100644 index 0000000..3a45456 --- /dev/null +++ b/minijazz/src/global/misc.ml @@ -0,0 +1,115 @@ + +(* Functions to decompose a list into a tuple *) +exception Arity_error of int * int (*expected, found*) +exception Arity_min_error of int * int (*expected, found*) + +let try_1 = function + | [v] -> v + | l -> raise (Arity_error(1, List.length l)) + +let try_2 = function + | [v1; v2] -> v1, v2 + | l -> raise (Arity_error(2, List.length l)) + +let try_3 = function + | [v1; v2; v3] -> v1, v2, v3 + | l -> raise (Arity_error(3, List.length l)) + +let try_4 = function + | [v1; v2; v3; v4] -> v1, v2, v3, v4 + | l -> raise (Arity_error(4, List.length l)) + +let try_1min = function + | v::l -> v, l + | l -> raise (Arity_min_error(1, List.length l)) + +let assert_fun f l = + try + f l + with + Arity_error(expected, found) -> + Format.eprintf "Internal compiler error: \ + wrong list size (found %d, expected %d).@." found expected; + assert false + +let assert_min_fun f l = + try + f l + with + Arity_min_error(expected, found) -> + Format.eprintf "Internal compiler error: \ + wrong list size (found %d, expected %d at least).@." found expected; + assert false + +let assert_1 l = assert_fun try_1 l +let assert_2 l = assert_fun try_2 l +let assert_3 l = assert_fun try_3 l +let assert_4 l = assert_fun try_4 l + +let assert_1min l = assert_min_fun try_1min l + +let mapfold f acc l = + let l,acc = List.fold_left + (fun (l,acc) e -> let e,acc = f acc e in e::l, acc) + ([],acc) l in + List.rev l, acc + +let mapi f l = + let rec aux i = function + | [] -> [] + | v::l -> (f i v)::(aux (i+1) l) + in + aux 1 l + +let unique l = + let tbl = Hashtbl.create (List.length l) in + List.iter (fun i -> Hashtbl.replace tbl i ()) l; + Hashtbl.fold (fun key _ accu -> key :: accu) tbl [] + +let is_empty = function | [] -> true | _ -> false + +let gen_symbol = + let counter = ref 0 in + let _gen_symbol () = + counter := !counter + 1; + "_"^(string_of_int !counter) + in + _gen_symbol + +let bool_of_string s = match s with + | "t" | "1" -> true + | "f" | "0" -> false + | _ -> raise (Invalid_argument ("bool_of_string")) + +let bool_array_of_string s = + let a = Array.make (String.length s) false in + for i = 0 to String.length s - 1 do + a.(i) <- bool_of_string (String.sub s i 1) + done; + a + +exception Int_too_big +let convert_size s n = + let m = String.length s in + if m > n then + raise Int_too_big + else + if m = n then s else (String.make (n - m) '0')^s + +let binary_not s = + for i=0 to String.length s - 1 do + s.[i] <- if s.[i] = '0' then '1' else '0' + done; + s + +let rec binary_string_of_int i n = + let rec s_of_i i = match i with + | 0 -> "0" + | 1 -> "1" + | i when i < 0 -> binary_not (binary_string_of_int (-i-1) n) + | _ -> + let q, r = i / 2, i mod 2 in + (s_of_i q) ^ (s_of_i r) + in + convert_size (s_of_i i) n + diff --git a/minijazz/src/global/printer.ml b/minijazz/src/global/printer.ml new file mode 100644 index 0000000..747541d --- /dev/null +++ b/minijazz/src/global/printer.ml @@ -0,0 +1,156 @@ +open Ident +open Ast +open Static +open Format +open Misc + +let print_name ff n = fprintf ff "%s" n + +let rec print_list_r print lp sep rp ff = function + | [] -> () + | x :: l -> + fprintf ff "%s%a" lp print x; + List.iter (fprintf ff "%s %a" sep print) l; + fprintf ff "%s" rp + +let rec print_list_nlr print lp sep rp ff = function + | [] -> () + | x :: l -> + fprintf ff "%s%a" lp print x; + List.iter (fprintf ff "%s@ %a" sep print) l; + fprintf ff "%s" rp + +let print_bool ff b = + if b then + fprintf ff "1" + else + fprintf ff "0" + +let rec print_const ff v = match v with + | VBit b -> print_bool ff b + | VBitArray a when Array.length a = 0 -> fprintf ff "[]" + | VBitArray l -> Array.iter (print_bool ff) l + +let rec print_static_exp ff se = match se.se_desc with + | SInt i -> fprintf ff "%d" i + | SBool b -> print_bool ff b + | SVar n -> print_name ff n + | SBinOp(op, se1, se2) -> + let op_str = match op with + | SAdd -> "+" | SMinus -> "-" + | SMult -> "*" | SDiv -> "/" + | SPower -> "^" | SEqual -> "=" + | SLess -> "<" | SLeq -> "<=" + | SGreater -> ">" | SGeq -> ">=" in + fprintf ff "(%a %s %a)" print_static_exp se1 op_str print_static_exp se2 + | SIf (c, se1, se2) -> + fprintf ff "(%a ? %a : %a)" + print_static_exp c print_static_exp se1 print_static_exp se2 + +let rec print_static_type ff sty = match sty with + | STInt -> fprintf ff "int" + | STBool -> fprintf ff "bool" + +let rec print_type ff ty = match ty with + | TUnit -> fprintf ff "()" + | TBit -> fprintf ff "bit" + | TBitArray se -> fprintf ff "bit[%a]" print_static_exp se + | TProd l -> print_list_r print_type "" "*" "" ff l + | TVar _ -> fprintf ff "<var>" + +let print_call_params ff params = match params with + | [] -> () + | _ -> print_list_r print_static_exp "<<"","">>" ff params + +let rec print_exp ff e = + if !Cli_options.print_types then + fprintf ff "(%a : %a)" print_edesc e.e_desc print_type e.e_ty + else + fprintf ff "%a" print_edesc e.e_desc + +and print_edesc ff ed = match ed with + | Econst v -> print_const ff v + | Evar n -> print_ident ff n + | Ereg e -> fprintf ff "reg %a" print_exp e + | Ecall("select", idx::_, args) -> + let e1 = assert_1 args in + fprintf ff "%a[%a]" print_exp e1 print_static_exp idx + | Ecall("slice", low::high::_, args) -> + let e1 = assert_1 args in + fprintf ff "%a[%a..%a]" + print_exp e1 print_static_exp low print_static_exp high + | Ecall("concat", _, args) -> + let e1, e2 = assert_2 args in + fprintf ff "%a . %a" print_exp e1 print_exp e2 + | Ecall(fn, params, args) -> + fprintf ff "%a%a%a" print_name fn print_call_params params print_args args + | Emem(MRom, addr_size, word_size, _, args) -> + fprintf ff "rom<%a,%a>%a" + print_static_exp addr_size print_static_exp word_size print_args args + | Emem(MRam, addr_size, word_size, _, args) -> + fprintf ff "ram<%a,%a>%a" + print_static_exp addr_size print_static_exp word_size print_args args + +and print_args ff args = + print_list_r print_exp "(" "," ")" ff args + +let rec print_pat ff pat = match pat with + | Evarpat id -> print_ident ff id + | Etuplepat l -> print_list_r print_ident "(" "," ")" ff l + +let print_eq ff (pat, e) = + fprintf ff "%a = %a" print_pat pat print_exp e + +let print_eqs ff eqs = + print_list_nlr print_eq """;""" ff eqs + +let print_var_dec ff vd = match vd.v_ty with + | TUnit -> fprintf ff "@[%a : .@]" print_ident vd.v_ident + | TBit -> fprintf ff "@[%a@]" print_ident vd.v_ident + | TBitArray se -> + fprintf ff "@[%a : [%a]@]" print_ident vd.v_ident print_static_exp se + | TProd _ -> assert false + | TVar _ -> fprintf ff "%a : <var>" print_ident vd.v_ident + +let print_var_decs ff vds = + print_list_r print_var_dec "("","")" ff vds + +let rec print_block ff b = match b with + | BEqs (eqs, []) -> print_eqs ff eqs + | BEqs (eqs, vds) -> + fprintf ff "@[<v 2>var %a@] in@,%a" print_var_decs vds print_eqs eqs + | BIf(se, thenb, elseb) -> + fprintf ff "@[<v 2>if %a then@,%a@]@,@[<v 2>else@,%a@]" + print_static_exp se + print_block thenb + print_block elseb + +let print_param ff p = + print_name ff p.p_name + +let print_params ff params = match params with + | [] -> () + | _ -> print_list_r print_param "<<"","">>" ff params + +let print_constraints ff cl = + if !Cli_options.print_types then + fprintf ff " with %a" (print_list_r print_static_exp "" " and " "") cl + +let print_node ff n = + fprintf ff "@[<v2>@[%a%a%a = %a@] where@ %a@.end where%a;@]@\n@." + print_name n.n_name + print_params n.n_params + print_var_decs n.n_inputs + print_var_decs n.n_outputs + print_block n.n_body + print_constraints n.n_constraints + +let print_const_dec ff cd = + fprintf ff "const %a = %a@\n@." + print_name cd.c_name print_static_exp cd.c_value + +let print_program oc p = + let ff = formatter_of_out_channel oc in + List.iter (print_const_dec ff) p.p_consts; + List.iter (print_node ff) p.p_nodes + diff --git a/minijazz/src/global/static.ml b/minijazz/src/global/static.ml new file mode 100644 index 0000000..352e62e --- /dev/null +++ b/minijazz/src/global/static.ml @@ -0,0 +1,31 @@ +open Errors +open Location + +type name = string +module NameEnv = Map.Make (struct type t = name let compare = compare end) + +type sop = + | SAdd | SMinus | SMult | SDiv | SPower (*int*) + | SEqual | SLess | SLeq | SGreater | SGeq (*bool*) + +type static_exp_desc = + | SInt of int + | SBool of bool + | SVar of name + | SBinOp of sop * static_exp * static_exp + | SIf of static_exp * static_exp * static_exp (* se1 ? se2 : se3 *) + +and static_exp = + { se_desc : static_exp_desc; + se_loc : location } + +type static_ty = STInt | STBool + +let mk_static_exp ?(loc = no_location) desc = + { se_desc = desc; se_loc = loc } +let mk_static_var s = + mk_static_exp (SVar s) +let mk_static_int i = + mk_static_exp (SInt i) +let mk_static_bool b = + mk_static_exp (SBool b) diff --git a/minijazz/src/global/static_utils.ml b/minijazz/src/global/static_utils.ml new file mode 100644 index 0000000..f95ce30 --- /dev/null +++ b/minijazz/src/global/static_utils.ml @@ -0,0 +1,76 @@ +open Static + +let pow a n = + let rec g p x = function + | 0 -> x + | i -> + g (p * p) (if i mod 2 = 1 then p * x else x) (i/2) + in + g a 1 n +;; + + +let fun_of_op op = match op with + | SAdd -> (+) | SMinus -> (-) + | SMult -> (fun i1 i2 -> i1 * i2) + | SDiv -> (/) + | SPower -> pow + | _ -> assert false + +let fun_of_comp_op op = match op with + | SEqual -> (=) | SLeq -> (<=) | SLess -> (<) + | _ -> assert false + +let rec simplify env se = match se.se_desc with + | SInt _ | SBool _ -> se + | SVar n -> + (try + let se = NameEnv.find n env in + simplify env se + with + | Not_found -> se) + | SBinOp(op, se1, se2) -> + let se1 = simplify env se1 in + let se2 = simplify env se2 in + let desc = + match op, se1.se_desc, se2.se_desc with + | (SAdd | SMinus | SDiv | SMult | SPower), SInt i1, SInt i2 -> + let f = fun_of_op op in + SInt (f i1 i2) + | (SEqual | SLess | SLeq | SGreater | SGeq), SInt i1, SInt i2 -> + let f = fun_of_comp_op op in + SBool (f i1 i2) + | _, _, _ -> SBinOp(op, se1, se2) + in + { se with se_desc = desc } + | SIf(c, se1, se2) -> + let c = simplify env c in + let se1 = simplify env se1 in + let se2 = simplify env se2 in + (match c.se_desc, se1.se_desc, se2.se_desc with + | SBool true, _, _ -> se1 + | SBool false, _, _ -> se2 + | _, sed1, sed2 when sed1 = sed2 -> { se with se_desc = sed1 } + | _, _, _ -> { se with se_desc = SIf(c, se1, se2) }) + +let rec subst env se = match se.se_desc with + | SInt _ | SBool _ -> se + | SVar n -> + (try + NameEnv.find n env + with + | Not_found -> se) + | SBinOp(op, se1, se2) -> + { se with se_desc = SBinOp(op, subst env se1, subst env se2) } + | SIf(c, se1, se2) -> + { se with se_desc = SIf(subst env c, subst env se1, subst env se2) } + +exception Unsatisfiable of static_exp +let check_true env cl = + let check_one c = + let res = simplify env c in + match res.se_desc with + | SBool true -> () + | _ -> raise (Unsatisfiable c) + in + List.iter check_one cl diff --git a/minijazz/src/main/cli_options.ml b/minijazz/src/main/cli_options.ml new file mode 100644 index 0000000..c5820a8 --- /dev/null +++ b/minijazz/src/main/cli_options.ml @@ -0,0 +1,18 @@ +(* version of the compiler *) +let version = "0.2.1" + +let verbose = ref false +let print_types = ref false +let no_inline_all = ref false +let main_node = ref "main" + +let base_path = ref "" + +let show_version () = + Format.printf "The MiniJazz compiler, version %s @." version +let errmsg = "Options are:" + +let doc_verbose = "\t\t\tSet verbose mode" +and doc_version = "\t\tThe version of the compiler" +and doc_full_type_info = "\t\tPrint full type information" +and doc_main_node = "\t\t\tSet the main node" diff --git a/minijazz/src/main/mj2net.ml b/minijazz/src/main/mj2net.ml new file mode 100644 index 0000000..9977a2d --- /dev/null +++ b/minijazz/src/main/mj2net.ml @@ -0,0 +1,94 @@ +open Ast +open Static +open Static_utils +open Ident + +let expect_int se = + let se = simplify NameEnv.empty se in + match se.se_desc with + | SInt v -> v + | _ -> + Format.eprintf "Unexpected static exp: %a@." Printer.print_static_exp se; + assert false + +let expect_ident e = match e.e_desc with + | Evar id -> string_of_ident id + | _ -> assert false + +let tr_value v = match v with + | VBit b -> Netlist_ast.VBit b + | VBitArray a -> Netlist_ast.VBitArray a + +let tr_ty ty = match ty with + | TBit -> Netlist_ast.TBit + | TBitArray se -> Netlist_ast.TBitArray (expect_int se) + | _ -> Format.eprintf "Unexpected type: %a@." Printer.print_type ty; assert false + +let tr_var_dec { v_ident = n; v_ty = ty } = + string_of_ident n, tr_ty ty + +let tr_pat pat = match pat with + | Evarpat id -> string_of_ident id + | Etuplepat ids -> + Format.eprintf "Unexpected pattern: %a@." Printer.print_pat pat; + assert false + +let expect_arg e = match e.e_desc with + | Evar id -> Netlist_ast.Avar (string_of_ident id) + | Econst v -> Netlist_ast.Aconst (tr_value v) + | _ -> Format.eprintf "Unexpected arg : %a@." Printer.print_exp e; assert false + +let rec tr_exp e = match e.e_desc with + | Evar id -> Netlist_ast.Earg (Netlist_ast.Avar (string_of_ident id)) + | Econst v -> Netlist_ast.Earg (Netlist_ast.Aconst (tr_value v)) + | Ereg e -> Netlist_ast.Ereg (expect_ident e) + | Ecall ("not", _, [e]) -> Netlist_ast.Enot (expect_arg e) + | Ecall (("or" | "xor" | "and" | "nand") as op, _, [e1; e2]) -> + let op = + match op with + | "or" -> Netlist_ast.Or + | "xor" -> Netlist_ast.Xor + | "and" -> Netlist_ast.And + | "nand" -> Netlist_ast.Nand + | _ -> assert false + in + Netlist_ast.Ebinop (op, expect_arg e1, expect_arg e2) + | Ecall ("mux", _, [e1; e2; e3]) -> + Netlist_ast.Emux (expect_arg e1, expect_arg e2, expect_arg e3) + | Ecall("select", idx::_, [e]) -> + Netlist_ast.Eselect (expect_int idx, expect_arg e) + | Ecall("slice", min::max::_, [e]) -> + Netlist_ast.Eslice (expect_int min, expect_int max, expect_arg e) + | Ecall("concat", _, [e1; e2]) -> + Netlist_ast.Econcat (expect_arg e1, expect_arg e2) + | Emem(MRom, addr_size, word_size, _, [e]) -> + Netlist_ast.Erom (expect_int addr_size, expect_int word_size, expect_arg e) + | Emem(MRam, addr_size, word_size, _, [ra; we; wa; data]) -> + Netlist_ast.Eram (expect_int addr_size, expect_int word_size, + expect_arg ra, expect_arg we, expect_arg wa, expect_arg data) + | _ -> assert false + +let tr_eq (pat, e) = + tr_pat pat, tr_exp e + +let tr_vds env vds = + List.fold_left + (fun env vd -> Netlist_ast.Env.add (string_of_ident vd.v_ident) (tr_ty vd.v_ty) env) + env vds + +let tr_block b = match b with + | BEqs (eqs, vds) -> + let env = tr_vds Netlist_ast.Env.empty vds in + let eqs = List.map tr_eq eqs in + env, eqs + | _ -> assert false + +let program p = + let n = match p.p_nodes with [n] -> n | _ -> assert false in + let vars, eqs = tr_block n.n_body in + let vars = tr_vds vars n.n_inputs in + let vars = tr_vds vars n.n_outputs in + let inputs = List.map (fun vd -> string_of_ident vd.v_ident) n.n_inputs in + let outputs = List.map (fun vd -> string_of_ident vd.v_ident) n.n_outputs in + { Netlist_ast.p_inputs = inputs; Netlist_ast.p_outputs = outputs; + Netlist_ast.p_vars = vars; Netlist_ast.p_eqs = eqs } diff --git a/minijazz/src/main/mj_compiler.ml b/minijazz/src/main/mj_compiler.ml new file mode 100644 index 0000000..c629e1c --- /dev/null +++ b/minijazz/src/main/mj_compiler.ml @@ -0,0 +1,80 @@ +open Errors +open Cli_options +open Location + +let separateur = "\n*********************************************\ + *********************************\n*** " + +let comment ?(sep=separateur) s = + if !verbose then Format.printf "%s%s@." sep s + +let do_pass d f p pp = + comment (d^" ...\n"); + let r = f p in + if !verbose then pp r; + comment ~sep:"*** " (d^" done."); + r + +let do_silent_pass d f p = do_pass d f p (fun _ -> ()) + +let pass d enabled f p pp = + if enabled + then do_pass d f p pp + else p + +let silent_pass d enabled f p = + if enabled + then do_silent_pass d f p + else p + +let parse lexbuf = + try + Parser.program Lexer.token lexbuf + with + | Lexer.Lexical_error(err, l) -> + lexical_error err l + | Parser.Error -> + let pos1 = Lexing.lexeme_start_p lexbuf + and pos2 = Lexing.lexeme_end_p lexbuf in + let l = Loc(pos1,pos2) in + syntax_error l + +let lexbuf_from_file file_name = + let ic = open_in file_name in + let lexbuf = Lexing.from_channel ic in + lexbuf.Lexing.lex_curr_p <- + { lexbuf.Lexing.lex_curr_p with Lexing.pos_fname = file_name }; + ic, lexbuf + +let compile_impl filename = + (* input and output files *) + let ic, lexbuf = lexbuf_from_file filename in + let net_name = (Filename.chop_suffix filename ".mj") ^ ".net" in + let net = open_out net_name in + let close_all_files () = + close_in ic; + close_out net + in + try + base_path := Filename.dirname filename; + + let pp = Printer.print_program stdout in + (* Parsing of the file *) + let p = do_pass "Parsing" parse lexbuf pp in + + let p = pass "Scoping" true Scoping.program p pp in + + let p = pass "Typing" true Typing.program p pp in + + let p = pass "Normalize" true Normalize.program p pp in + + let p = pass "Callgraph" true Callgraph.program p pp in + + let p = pass "Simplify" true Simplify.program p pp in + + let p = Mj2net.program p in + Netlist_printer.print_program net p; + + close_all_files () + with + | x -> close_all_files (); raise x diff --git a/minijazz/src/main/mjc.ml b/minijazz/src/main/mjc.ml new file mode 100644 index 0000000..ada6b34 --- /dev/null +++ b/minijazz/src/main/mjc.ml @@ -0,0 +1,20 @@ +open Cli_options +open Mj_compiler + +let main () = + try + Arg.parse + [ + "-v",Arg.Set verbose, doc_verbose; + "-version", Arg.Unit show_version, doc_version; + "-m", Arg.Set_string main_node, doc_main_node; + "-print-types", Arg.Set print_types, doc_full_type_info; + ] + compile_impl + errmsg; + with + | Errors.Error -> exit 2;; + +main () + + diff --git a/minijazz/src/myocamlbuild.ml b/minijazz/src/myocamlbuild.ml new file mode 100644 index 0000000..a0cf61a --- /dev/null +++ b/minijazz/src/myocamlbuild.ml @@ -0,0 +1,39 @@ +(***********************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Gwenael Delaval, LIG/INRIA, UJF *) +(* Leonard Gerard, Parkas, ENS *) +(* Adrien Guatto, Parkas, ENS *) +(* Cedric Pasteur, Parkas, ENS *) +(* Marc Pouzet, Parkas, ENS *) +(* *) +(* Copyright 2012 ENS, INRIA, UJF *) +(* *) +(* This file is part of the Heptagon compiler. *) +(* *) +(* Heptagon is free software: you can redistribute it and/or modify it *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 3 of the License, or *) +(* (at your option) any later version. *) +(* *) +(* Heptagon is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU General Public License for more details. *) +(* *) +(* You should have received a copy of the GNU General Public License *) +(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *) +(* *) +(***********************************************************************) +open Ocamlbuild_plugin +open Ocamlbuild_plugin.Options +open Myocamlbuild_config + +let df = function + | Before_options -> ocamlfind_before_options () + | After_rules -> ocamlfind_after_rules (); + + | _ -> () + +let _ = dispatch df diff --git a/minijazz/src/myocamlbuild_config.ml b/minijazz/src/myocamlbuild_config.ml new file mode 100644 index 0000000..e63553b --- /dev/null +++ b/minijazz/src/myocamlbuild_config.ml @@ -0,0 +1,112 @@ +(***********************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Gwenael Delaval, LIG/INRIA, UJF *) +(* Leonard Gerard, Parkas, ENS *) +(* Adrien Guatto, Parkas, ENS *) +(* Cedric Pasteur, Parkas, ENS *) +(* Marc Pouzet, Parkas, ENS *) +(* *) +(* Copyright 2012 ENS, INRIA, UJF *) +(* *) +(* This file is part of the Heptagon compiler. *) +(* *) +(* Heptagon is free software: you can redistribute it and/or modify it *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 3 of the License, or *) +(* (at your option) any later version. *) +(* *) +(* Heptagon is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU General Public License for more details. *) +(* *) +(* You should have received a copy of the GNU General Public License *) +(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *) +(* *) +(***********************************************************************) +open Ocamlbuild_plugin + +(* these functions are not really officially exported *) +let run_and_read = Ocamlbuild_pack.My_unix.run_and_read +let blank_sep_strings = Ocamlbuild_pack.Lexers.blank_sep_strings + +let split s ch = + let x = ref [] in + let rec go s = + let pos = String.index s ch in + x := (String.before s pos)::!x; + go (String.after s (pos + 1)) + in + try + go s + with Not_found -> !x + +let split_nl s = split s '\n' + +let before_space s = + try + String.before s (String.index s ' ') + with Not_found -> s + +(* this lists all supported packages *) +let find_packages () = + List.map before_space (split_nl & run_and_read "ocamlfind list") + +(* this is supposed to list available syntaxes, but I don't know how to do it. *) +let find_syntaxes () = ["camlp4o"; "camlp4r"] + +(* ocamlfind command *) +let ocamlfind x = S[A"ocamlfind"; x] + +let ocamlfind_query pkg = + let cmd = Printf.sprintf "ocamlfind query %s" (Filename.quote pkg) in + Ocamlbuild_pack.My_unix.run_and_open cmd (fun ic -> input_line ic) + +let ocamlfind_before_options () = + (* by using Before_options one let command line options have an higher priority *) + (* on the contrary using After_options will guarantee to have the higher priority *) + + (* override default commands by ocamlfind ones *) + Options.ocamlc := ocamlfind & A"ocamlc"; + Options.ocamlopt := ocamlfind & A"ocamlopt"; + Options.ocamldep := ocamlfind & A"ocamldep"; + Options.ocamldoc := ocamlfind & A"ocamldoc"; + Options.ocamlmktop := ocamlfind & A"ocamlmktop" + +let ocamlfind_after_rules () = + (* When one link an OCaml library/binary/package, one should use -linkpkg *) + flag ["ocaml"; "link"; "program"] & A"-linkpkg"; + + (* For each ocamlfind package one inject the -package option when + * compiling, computing dependencies, generating documentation and + * linking. *) + List.iter begin fun pkg -> + flag ["ocaml"; "compile"; "pkg_"^pkg] & S[A"-package"; A pkg]; + flag ["ocaml"; "ocamldep"; "pkg_"^pkg] & S[A"-package"; A pkg]; + flag ["ocaml"; "doc"; "pkg_"^pkg] & S[A"-package"; A pkg]; + flag ["ocaml"; "link"; "pkg_"^pkg] & S[A"-package"; A pkg]; + flag ["ocaml"; "infer_interface"; "pkg_"^pkg] & S[A"-package"; A pkg]; + end (find_packages ()); + + (* Like -package but for extensions syntax. Morover -syntax is useless + * when linking. *) + List.iter begin fun syntax -> + flag ["ocaml"; "compile"; "syntax_"^syntax] & S[A"-syntax"; A syntax]; + flag ["ocaml"; "ocamldep"; "syntax_"^syntax] & S[A"-syntax"; A syntax]; + flag ["ocaml"; "doc"; "syntax_"^syntax] & S[A"-syntax"; A syntax]; + flag ["ocaml"; "infer_interface"; "syntax_"^syntax] & S[A"-syntax"; A syntax]; + end (find_syntaxes ()); + + (* The default "thread" tag is not compatible with ocamlfind. + Indeed, the default rules add the "threads.cma" or "threads.cmxa" + options when using this tag. When using the "-linkpkg" option with + ocamlfind, this module will then be added twice on the command line. + + To solve this, one approach is to add the "-thread" option when using + the "threads" package using the previous plugin. + *) + flag ["ocaml"; "pkg_threads"; "compile"] (S[A "-thread"]); + flag ["ocaml"; "pkg_threads"; "link"] (S[A "-thread"]); + flag ["ocaml"; "pkg_threads"; "infer_interface"] (S[A "-thread"]) diff --git a/minijazz/src/netlist/netlist_ast.ml b/minijazz/src/netlist/netlist_ast.ml new file mode 100644 index 0000000..00100b6 --- /dev/null +++ b/minijazz/src/netlist/netlist_ast.ml @@ -0,0 +1,50 @@ +type ident = string + +(* Environment using ident as key *) +module Env = struct + include Map.Make(struct + type t = ident + let compare = compare + end) + + let of_list l = + List.fold_left (fun env (x, ty) -> add x ty env) empty l +end + +type ty = TBit | TBitArray of int +type value = VBit of bool | VBitArray of bool array + +type binop = Or | Xor | And | Nand + +(* argument of operators (variable or constant) *) +type arg = + | Avar of ident (* x *) + | Aconst of value (* constant *) + +(* Expressions (see MiniJazz documentation for more info on the operators) *) +type exp = + | Earg of arg (* a: argument *) + | Ereg of ident (* REG x : register *) + | Enot of arg (* NOT a *) + | Ebinop of binop * arg * arg (* OP a1 a2 : boolean operator *) + | Emux of arg * arg * arg (* MUX a1 a2 : multiplexer *) + | Erom of int (*addr size*) * int (*word size*) * arg (*read_addr*) + (* ROM addr_size word_size read_addr *) + | Eram of int (*addr size*) * int (*word size*) + * arg (*read_addr*) * arg (*write_enable*) + * arg (*write_addr*) * arg (*data*) + (* RAM addr_size word_size read_addr write_enable write_addr data *) + | Econcat of arg * arg (* CONCAT a1 a2 : concatenation of arrays *) + | Eslice of int * int * arg + (* SLICE i1 i2 a : extract the slice of a between indices i1 and i2 *) + | Eselect of int * arg + (* SELECT i a : ith element of a *) + +(* equations: x = exp *) +type equation = ident * exp + +type program = + { p_eqs : equation list; (* equations *) + p_inputs : ident list; (* inputs *) + p_outputs : ident list; (* outputs *) + p_vars : ty Env.t; } (* maps variables to their types*) diff --git a/minijazz/src/netlist/netlist_printer.ml b/minijazz/src/netlist/netlist_printer.ml new file mode 100644 index 0000000..d513137 --- /dev/null +++ b/minijazz/src/netlist/netlist_printer.ml @@ -0,0 +1,82 @@ +open Netlist_ast +open Format + +let rec print_env print lp sep rp ff env = + let first = ref true in + fprintf ff "%s" lp; + Env.iter + (fun x ty -> + if !first then + (first := false; fprintf ff "%a" print (x, ty)) + else + fprintf ff "%s%a" sep print (x, ty)) env; + fprintf ff "%s" rp + +let rec print_list print lp sep rp ff = function + | [] -> () + | x :: l -> + fprintf ff "%s%a" lp print x; + List.iter (fprintf ff "%s %a" sep print) l; + fprintf ff "%s" rp + +let print_ty ff ty = match ty with + | TBit -> () + | TBitArray n -> fprintf ff " : %d" n + +let print_bool ff b = + if b then + fprintf ff "1" + else + fprintf ff "0" + +let print_value ff v = match v with + | VBit b -> print_bool ff b + | VBitArray a -> Array.iter (print_bool ff) a + +let print_arg ff arg = match arg with + | Aconst v -> print_value ff v + | Avar id -> fprintf ff "%s" id + +let print_op ff op = match op with + | And -> fprintf ff "AND" + | Nand -> fprintf ff "NAND" + | Or -> fprintf ff "OR" + | Xor -> fprintf ff "XOR" + +let print_exp ff e = match e with + | Earg a -> print_arg ff a + | Ereg x -> fprintf ff "REG %s" x + | Enot x -> fprintf ff "NOT %a" print_arg x + | Ebinop(op, x, y) -> fprintf ff "%a %a %a" print_op op print_arg x print_arg y + | Emux (c, x, y) -> fprintf ff "MUX %a %a %a " print_arg c print_arg x print_arg y + | Erom (addr, word, ra) -> fprintf ff "ROM %d %d %a" addr word print_arg ra + | Eram (addr, word, ra, we, wa, data) -> + fprintf ff "RAM %d %d %a %a %a %a" addr word + print_arg ra print_arg we + print_arg wa print_arg data + | Eselect (idx, x) -> fprintf ff "SELECT %d %a" idx print_arg x + | Econcat (x, y) -> fprintf ff "CONCAT %a %a" print_arg x print_arg y + | Eslice (min, max, x) -> fprintf ff "SLICE %d %d %a" min max print_arg x + +let print_eq ff (x, e) = + fprintf ff "%s = %a@." x print_exp e + +let print_var ff (x, ty) = + fprintf ff "@[%s%a@]" x print_ty ty + +let print_vars ff env = + fprintf ff "@[<v 2>VAR@,%a@]@.IN@," + (print_env print_var "" ", " "") env + +let print_idents ff ids = + let print_ident ff s = fprintf ff "%s" s in + print_list print_ident """,""" ff ids + +let print_program oc p = + let ff = formatter_of_out_channel oc in + fprintf ff "INPUT %a@." print_idents p.p_inputs; + fprintf ff "OUTPUT %a@." print_idents p.p_outputs; + print_vars ff p.p_vars; + List.iter (print_eq ff) p.p_eqs; + (* flush *) + fprintf ff "@." diff --git a/minijazz/src/parser/_tags b/minijazz/src/parser/_tags new file mode 100644 index 0000000..d4a6ba1 --- /dev/null +++ b/minijazz/src/parser/_tags @@ -0,0 +1,2 @@ +<parser.ml>: use_menhirLib +true: use_menhir diff --git a/minijazz/src/parser/lexer.mll b/minijazz/src/parser/lexer.mll new file mode 100644 index 0000000..f7b0e82 --- /dev/null +++ b/minijazz/src/parser/lexer.mll @@ -0,0 +1,196 @@ +(* lexer.mll *) + + +{ +open Location +open Lexing +open Parser +open Errors + +exception Lexical_error of lexical_error * location;; + +let comment_depth = ref 0 + +let keyword_table = ((Hashtbl.create 149) : (string, token) Hashtbl.t);; + +List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ + "ram", RAM; + "rom", ROM; + "where", WHERE; + "end", END; + "true", BOOL(true); + "false", BOOL(false); + "reg", REG; + "not", NOT; + "const", CONST; + "and", AND; + "nand", NAND; + "or", OR; + "xor", XOR; + "if", IF; + "then", THEN; + "else", ELSE; + "inlined", INLINED; + "probing", PROBING +] + + +(* To buffer string literals *) + +let initial_string_buffer = String.create 256 +let string_buff = ref initial_string_buffer +let string_index = ref 0 + +let reset_string_buffer () = + string_buff := initial_string_buffer; + string_index := 0; + () + +(* +let incr_linenum lexbuf = + let pos = lexbuf.Lexing.lex_curr_p in + lexbuf.Lexing.lex_curr_p <- { pos with + Lexing.pos_lnum = pos.Lexing.pos_lnum + 1; + Lexing.pos_bol = pos.Lexing.pos_cnum; + } +*) + +let store_string_char c = + if !string_index >= String.length (!string_buff) then begin + let new_buff = String.create (String.length (!string_buff) * 2) in + String.blit (!string_buff) 0 new_buff 0 (String.length (!string_buff)); + string_buff := new_buff + end; + String.set (!string_buff) (!string_index) c; + incr string_index + + +let get_stored_string () = + let s = String.sub (!string_buff) 0 (!string_index) in + string_buff := initial_string_buffer; + s + +let char_for_backslash = function + 'n' -> '\010' + | 'r' -> '\013' + | 'b' -> '\008' + | 't' -> '\009' + | c -> c + +let char_for_decimal_code lexbuf i = + let c = + 100 * (int_of_char(Lexing.lexeme_char lexbuf i) - 48) + + 10 * (int_of_char(Lexing.lexeme_char lexbuf (i+1)) - 48) + + (int_of_char(Lexing.lexeme_char lexbuf (i+2)) - 48) in + char_of_int(c land 0xFF) + +} + +let newline = '\n' | '\r' '\n' + +rule token = parse + | newline { new_line lexbuf; token lexbuf } + | [' ' '\t'] + { token lexbuf } + | "(" { LPAREN } + | ")" { RPAREN } + | "*" { STAR } + | "+" { PLUS } + | "&" { AND } + | "/" { SLASH } + | "<" { LESS } + | ">" { GREATER } + | "[" { LBRACKET } + | "]" { RBRACKET } + | ":" { COLON } + | ";" { SEMICOL } + | "=" { EQUAL } + | "," { COMMA } + | "-" { MINUS } + | "^" { POWER } + | "<=" { LEQ } + | "." { DOT } + | ".." { DOTDOT } + | (['A'-'Z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) + {NAME id} + | (['A'-'Z' 'a'-'z']('_' ? ['A'-'Z' 'a'-'z' ''' '0'-'9']) * as id) + { let s = Lexing.lexeme lexbuf in + try Hashtbl.find keyword_table s + with Not_found -> NAME id } + | '0' ['b' 'B'] (['0'-'1']+ as lit) + { BOOL_INT lit } + | ['0'-'9']+ + | '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+ + | '0' ['o' 'O'] ['0'-'7']+ + { INT (int_of_string(Lexing.lexeme lexbuf)) } + | "\"" + { reset_string_buffer(); + let string_start = lexbuf.lex_start_p in + (* string_start_loc := Location.curr lexbuf; *) + string lexbuf; + lexbuf.lex_start_p <- string_start; + STRING (get_stored_string()) } + | "(*" + { let comment_start = lexbuf.lex_curr_p in + comment_depth := 1; + begin try + comment lexbuf + with Lexical_error(Unterminated_comment, (Loc (_, comment_end))) -> + raise(Lexical_error(Unterminated_comment, + Loc (comment_start, comment_end))) + end; + token lexbuf } + | eof {EOF} + | _ {raise (Lexical_error (Illegal_character, + Loc (Lexing.lexeme_start_p lexbuf, + Lexing.lexeme_end_p lexbuf)))} + +and comment = parse + "(*" + { comment_depth := succ !comment_depth; comment lexbuf } + | "*)" + { comment_depth := pred !comment_depth; + if !comment_depth > 0 then comment lexbuf } + | "\"" + { reset_string_buffer(); + let string_start = lexbuf.lex_curr_p in + begin try + string lexbuf + with Lexical_error(Unterminated_string, Loc (_, string_end)) -> + raise(Lexical_error + (Unterminated_string, Loc (string_start, string_end))) + end; + comment lexbuf } + | "''" + { comment lexbuf } + | "'" [^ '\\' '\''] "'" + { comment lexbuf } + | "'" '\\' ['\\' '\'' 'n' 't' 'b' 'r'] "'" + { comment lexbuf } + | "'" '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] "'" + { comment lexbuf } + | eof + { raise(Lexical_error(Unterminated_comment, Loc(dummy_pos, + Lexing.lexeme_start_p lexbuf))) } + | _ + { comment lexbuf } + +and string = parse + '"' + { () } + | '\\' ("\010" | "\013" | "\013\010") [' ' '\009'] * + { string lexbuf } + | '\\' ['\\' '"' 'n' 't' 'b' 'r'] + { store_string_char(char_for_backslash(Lexing.lexeme_char lexbuf 1)); + string lexbuf } + | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9'] + { store_string_char(char_for_decimal_code lexbuf 1); + string lexbuf } + | eof + { raise (Lexical_error(Unterminated_string, Loc (dummy_pos, + Lexing.lexeme_start_p lexbuf))) } + | _ + { store_string_char(Lexing.lexeme_char lexbuf 0); + string lexbuf } + +(* eof *) + diff --git a/minijazz/src/parser/parser.mly b/minijazz/src/parser/parser.mly new file mode 100644 index 0000000..126ab36 --- /dev/null +++ b/minijazz/src/parser/parser.mly @@ -0,0 +1,185 @@ +%{ + +open Ident +open Static +open Ast +open Location +open Misc + +let fresh_param () = + mk_static_exp (SVar ("_n"^(Misc.gen_symbol ()))) + +%} + +%token INLINED ROM RAM WHERE END CONST PROBING +%token LPAREN RPAREN COLON COMMA EQUAL REG OR XOR NAND AND POWER SLASH +%token EOF RBRACKET LBRACKET GREATER LESS NOT SEMICOL PLUS MINUS STAR +%token IF THEN ELSE LEQ DOT DOTDOT +%token <string> NAME +%token <string> STRING +%token <int> INT +%token <string> BOOL_INT +%token <bool> BOOL + +%left DOT +%left OR PLUS +%left LEQ EQUAL +%right MINUS +%left NAND XOR AND +%left STAR SLASH +%right NOT REG +%right POWER + +%start program +%type <Ast.program> program + +%% + +/** Tools **/ +%inline slist(S, x) : l=separated_list(S, x) {l} +%inline snlist(S, x) : l=separated_nonempty_list(S, x) {l} +%inline tuple(x) : LPAREN h=x COMMA t=snlist(COMMA,x) RPAREN { h::t } +%inline tag_option(P,x): + |/* empty */ { None } + | P v=x { Some(v) } + +localize(x): y=x { y, (Loc($startpos(y),$endpos(y))) } + +program: + | c=const_decs n=node_decs EOF + { mk_program c n } + +const_decs: c=list(const_dec) {c} +const_dec: + | CONST n=name EQUAL se=static_exp option(SEMICOL) + { mk_const_dec ~loc:(Loc($startpos,$endpos)) n se } + +name: n=NAME { n } + +ident: + | n=name { ident_of_string n } + +type_ident: LBRACKET se=static_exp RBRACKET { TBitArray se } + +node_name: + | n=name { reset_symbol_table (); n } + +node_decs: ns=list(node_dec) { ns } +node_dec: + inlined=inlined_status n=node_name p=params LPAREN args=args RPAREN + EQUAL out=node_out WHERE b=block probes=probe_decls END WHERE option(SEMICOL) + { mk_node n (Loc ($startpos,$endpos)) inlined args out p b probes } + +node_out: + | a=arg { [a] } + | LPAREN out=args RPAREN { out } + +inlined_status: + | INLINED { Inlined } + | /*empty*/ { NotInlined } + +params: + | /*empty*/ { [] } + | LESS pl=snlist(COMMA,param) GREATER { pl } + +param: + n=NAME { mk_param n } + +args: vl=slist(COMMA, arg) { vl } + +arg: + | n=ident COLON t=type_ident { mk_var_dec n t } + | n=ident { mk_var_dec n TBit } + +block: + | eqs=equs { BEqs (eqs, []) } + | IF se=static_exp THEN thenb=block ELSE elseb=block END IF { BIf(se, thenb, elseb) } + +equs: eq=equ tl=equ_tail { eq::tl } +equ_tail: + | /*empty*/ { [] } + | SEMICOL { [] } + | SEMICOL eq=equ tl=equ_tail { eq::tl } +equ: p=pat EQUAL e=exp { mk_equation p e } + +pat: + | n=ident { Evarpat n } + | LPAREN p=snlist(COMMA, ident) RPAREN { Etuplepat p } + +static_exp: se=_static_exp { mk_static_exp ~loc:(Loc ($startpos,$endpos)) se } +_static_exp : + | i=INT { SInt i } + | n=NAME { SVar n } + | LPAREN se=_static_exp RPAREN { se } + /*integer ops*/ + | se1=static_exp POWER se2=static_exp { SBinOp(SPower, se1, se2) } + | se1=static_exp PLUS se2=static_exp { SBinOp(SAdd, se1, se2) } + | se1=static_exp MINUS se2=static_exp { SBinOp(SMinus, se1, se2) } + | se1=static_exp STAR se2=static_exp { SBinOp(SMult, se1, se2) } + | se1=static_exp SLASH se2=static_exp { SBinOp(SDiv, se1, se2) } + /*bool ops*/ + | se1=static_exp EQUAL se2=static_exp { SBinOp(SEqual, se1, se2) } + | se1=static_exp LEQ se2=static_exp { SBinOp(SLeq, se1, se2) } + +exps: LPAREN e=slist(COMMA, exp) RPAREN {e} + +exp: e=_exp { mk_exp ~loc:(Loc ($startpos,$endpos)) e } +_exp: + | e=_simple_exp { e } + | c=const { Econst c } + | REG e=exp { Ereg e } + | n=NAME p=call_params a=exps { Ecall (n, p, a) } + | e1=exp PLUS e2=exp { Ecall ("or", [], [e1; e2]) } + | e1=exp OR e2=exp { Ecall ("or", [], [e1; e2]) } + | e1=exp AND e2=exp { Ecall ("and", [], [e1; e2]) } + | e1=exp POWER e2=exp { Ecall("xor", [], [e1; e2]) } + | e1=exp XOR e2=exp { Ecall ("xor", [], [e1; e2]) } + | e1=exp NAND e2=exp { Ecall ("nand", [], [e1; e2]) } + | NOT a=exp { Ecall ("not", [], [a])} + | e1=exp DOT e2=exp + { Ecall("concat", [fresh_param(); fresh_param(); fresh_param ()], [e1; e2]) } + | e1=simple_exp LBRACKET idx=static_exp RBRACKET + { Ecall ("select", [idx; fresh_param()], [e1]) } + | e1=simple_exp LBRACKET low=static_exp DOTDOT high=static_exp RBRACKET + { Ecall("slice", [low; high; fresh_param()], [e1]) } + | e1=simple_exp LBRACKET low=static_exp DOTDOT RBRACKET + { let n = fresh_param () in + let high = mk_static_exp (SBinOp(SMinus, n, mk_static_exp (SInt 1))) in + Ecall("slice", [low; high; n], [e1]) } + | e1=simple_exp LBRACKET DOTDOT high=static_exp RBRACKET + { + let params = [mk_static_exp (SInt 0); high; fresh_param ()] in + Ecall("slice", params, [e1]) + } + | ro=rom_or_ram LESS addr_size=static_exp + COMMA word_size=static_exp input_file=tag_option(COMMA, STRING) GREATER a=exps + { Emem(ro, addr_size, word_size, input_file, a) } + +simple_exp: e=_simple_exp { mk_exp ~loc:(Loc ($startpos,$endpos)) e } +_simple_exp: + | n=ident { Evar n } + | LPAREN e=_exp RPAREN { e } + +const: + | b=BOOL { VBit b } + | b=BOOL_INT { VBitArray (bool_array_of_string b) } + | i=INT + { match i with + | 0 -> VBit false + | 1 -> VBit true + | _ -> raise Parsing.Parse_error + } + | LBRACKET RBRACKET { VBitArray (Array.make 0 false) } + +rom_or_ram : + | ROM { MRom } + | RAM { MRam } + +call_params: + | /*empty*/ { [] } + | LESS pl=snlist(COMMA,static_exp) GREATER { pl } + +probe_decls: + | /*empty*/ { [] } + | PROBING l=separated_nonempty_list(COMMA, ident) { l } +%% diff --git a/minijazz/test/mem.bin b/minijazz/test/mem.bin new file mode 100644 index 0000000..124bd7c --- /dev/null +++ b/minijazz/test/mem.bin @@ -0,0 +1,4 @@ +11 +10 +01 +00
\ No newline at end of file diff --git a/minijazz/test/nadder.mj b/minijazz/test/nadder.mj new file mode 100644 index 0000000..a5a6a17 --- /dev/null +++ b/minijazz/test/nadder.mj @@ -0,0 +1,19 @@ +fulladder(a,b,c) = (s, r) where + s = (a ^ b) ^ c; + r = (a & b) + ((a ^ b) & c); +end where + +adder<n>(a:[n], b:[n], c_in) = (o:[n], c_out) where + if n = 0 then + o = []; + c_out = 0 + else + (s_n1, c_n1) = adder<n-1>(a[1..], b[1..], c_in); + (s_n, c_out) = fulladder(a[0], b[0], c_n1); + o = s_n . s_n1 + end if +end where + +main(a:[2], b:[2]) = (o:[2], c) where + (o, c) = adder<2>(a,b,0) +end where
\ No newline at end of file diff --git a/minijazz/test/shifters.mj b/minijazz/test/shifters.mj new file mode 100644 index 0000000..157abfe --- /dev/null +++ b/minijazz/test/shifters.mj @@ -0,0 +1,44 @@ +const word_size = 4 + +(* Transforme un fil en une nappe de n fils avec la meme valeur *) +power<n>(i) = (o:[n]) where + if n = 1 then + o = i + else + o = power<n-1>(i) . i + end if +end where + +mux_n<n>(c, a:[n], b:[n]) = (o:[n]) where + if n = 0 then + o = [] + else + o_n1 = mux_n<n-1>(c, a[1..n-1], b[1..n-1]); + o_n = mux(c, a[0], b[0]); + o = o_n . o_n1 + end if +end where + +lshifter_n<n, p>(sh:[n], a:[p]) = (o:[p]) where + if n = 0 then + o = [] + else + o = lshifter_n<n-1, p>(sh[1..n-1], u); + u = mux_n<p>(sh[0], a, a[2^(n-1)..p-1] . power<2^(n-1)>(false)) + end if +end where + +rshifter_n<n, p>(sh:[n], arith, a:[p]) = (o:[p]) where + if n = 1 then + added_bit = mux(arith, false, a[1]); + o = mux_n<p>(sh[0], a, added_bit . a[1..p-1]) + else + o = rshifter_n<n-1, p>(sh[1..n-1], arith, u); + added_bit = mux(arith, false, a[2^(n-1)]); + u = mux_n<p>(sh[0], a, power<2^(n-1)>(added_bit) . a[2^(n-1)..p-1]) + end if +end where + +main(sh:[2], arith, left, a:[word_size]) = (o:[word_size]) where + o = rshifter_n<2, word_size>(sh, arith, a) +end where
\ No newline at end of file diff --git a/minijazz/test/t1.in b/minijazz/test/t1.in new file mode 100644 index 0000000..6d94f07 --- /dev/null +++ b/minijazz/test/t1.in @@ -0,0 +1,5 @@ +1 1 +1 0 +0 1 +1 1 +0 1
\ No newline at end of file diff --git a/minijazz/test/tests.mj b/minijazz/test/tests.mj new file mode 100644 index 0000000..a8f8b63 --- /dev/null +++ b/minijazz/test/tests.mj @@ -0,0 +1,19 @@ +Fulladder(a,b,c) = (s, r) where + s = (a xor b) xor c; + r = (a and b) or ((a xor b) and c); +end where + +minus(x) = (y) where + y = x xor c; + c = reg (x or y) +end where + +cm2(x) = (s, r) where + s = reg (x xor s); + r = x and s +end where + +clk2() = (o) where + o = reg(c); + c = not (reg (o)) +end where
\ No newline at end of file |