Permalink
Browse files

Translate subprogram calls to C.

  • Loading branch information...
xlq committed Sep 1, 2012
1 parent d7a7551 commit 9ef7843ef4d3b4937630b137a14a981d88b83ef7
Showing with 83 additions and 38 deletions.
  1. +11 −1 backend_c.ml
  2. +2 −0 icode.ml
  3. +4 −0 icode.mli
  4. +6 −0 misc.ml
  5. +3 −0 misc.mli
  6. +3 −1 translation.ml
  7. +54 −36 type_checking.ml
@@ -58,6 +58,10 @@ let rec translate_expr context = function
| Boolean_literal(false) -> 100, "false"
| Integer_literal(i) -> 100, string_of_big_int i
| Var(x) -> 100, c_name_of_symbol context x
| Var_v(x) ->
(* Note that this happens in the context of bound_arguments.
This isn't very neat. *)
100, c_name_of_symbol context x.ver_symbol
| Negation(e) ->
let e = translate_expr context e in
90, "!" ^ paren 90 e
@@ -91,7 +95,13 @@ let rec translate_icode context f = function
| Jump_term(jmp) ->
puts f ("goto block" ^ string_of_int jmp.jmp_target.bl_id ^ ";");
break f
(* | Call_term TODO *)
| Call_term(call, tail) ->
puts f (c_name_of_symbol context call.call_target ^ "("
^ String.concat ", "
(List.map (fun arg -> snd (translate_expr context arg)) call.call_bound_arguments)
^ ");");
break f;
translate_icode context f tail
| Inspect_type_term(_,_,tail) -> translate_icode context f tail
| Static_assert_term(_,_,tail) -> translate_icode context f tail
@@ -31,6 +31,8 @@ and call_info =
call_location : loc;
call_target : symbol;
call_arguments : expr list * (string * expr) list;
mutable call_bound_arguments
: expr list;
}
and block =
@@ -43,6 +43,10 @@ and call_info =
call_location : loc;
call_target : symbol;
call_arguments : expr list * (string * expr) list;
(* call_bound_arguments is set once the target subprogram has been
chosen. The list is in the same order as the target's parameters. *)
mutable call_bound_arguments
: expr list;
}
and block =
@@ -1,3 +1,9 @@
let unsome = function
| Some x -> x
| None -> raise (Failure "unsome")
let list_iteri f l =
let rec loop i = function
| [] -> ()
| x::l -> f i x; loop (i+1) l
in loop 0 l
@@ -1 +1,4 @@
val unsome : 'a option -> 'a
(* list_iteri f [a;b;c;...] = f 0 a; f 1 b; f 2 c; ... *)
val list_iteri : (int -> 'a -> unit) -> 'a list -> unit
@@ -223,7 +223,9 @@ let rec translate_statement
Call_term(
{call_location = loc;
call_target = subprogram_sym;
call_arguments = (positional_args, named_args)},
call_arguments = (positional_args, named_args);
call_bound_arguments = [];
},
translate_statement state context tail)
| _ ->
Errors.semantic_error loc
@@ -272,55 +272,73 @@ let rec type_check
begin match call.call_target.sym_info with
| Subprogram_sym(subprogram_info) ->
let preconditions = ref subprogram_info.sub_preconditions in
let parameters = ref subprogram_info.sub_parameters in
let (parameters: (symbol * expr option) array) = Array.of_list
(List.map (fun parameter_sym ->
(parameter_sym, None)) subprogram_info.sub_parameters)
in
let positional_args, named_args = call.call_arguments in
let got_argument param arg =
match param.sym_info with Parameter_sym(param_type) ->
let arg, arg_t = type_check_expr
{context with tc_expected = Some param_type} arg
in
ignore arg_t;
preconditions := List.map (subst param arg) !preconditions
let got_argument i arg =
match parameters.(i) with
| (parameter_sym, None) ->
begin
match parameter_sym.sym_info with Parameter_sym(param_type) ->
let arg, arg_t = type_check_expr
{context with tc_expected = Some param_type} arg
in
ignore arg_t;
preconditions := List.map (subst parameter_sym arg) !preconditions;
parameters.(i) <- (parameter_sym, Some arg)
end
| (parameter_sym, Some _) ->
Errors.semantic_error call.call_location
("Parameter `" ^ parameter_sym.sym_name
^ "' specified twice.")
in
(* Bind positional arguments. *)
List.iter (fun arg ->
match !parameters with
| [] ->
list_iteri (fun i arg ->
if i >= Array.length parameters then begin
Errors.semantic_error call.call_location
("Too many arguments to "
^ describe_symbol call.call_target ^ ".");
| param::remaining_params ->
parameters := remaining_params;
got_argument param arg
^ describe_symbol call.call_target ^ ".")
end else begin
got_argument i arg
end
) positional_args;
(* Bind named arguments. *)
List.iter (fun (name, arg) ->
let rec search = function
| [] ->
if List.exists
(fun param -> param.sym_name = name)
subprogram_info.sub_parameters
then begin
Errors.semantic_error call.call_location
("Parameter `" ^ name ^ "' specified twice.")
end else begin
let rec search i =
if i >= Array.length parameters then begin
Errors.semantic_error call.call_location
("Parameter `" ^ name ^ "' doesn't exist in call to "
^ describe_symbol call.call_target ^ ".")
end;
[]
| param::rest when param.sym_name = name ->
got_argument param arg;
rest
| param::rest -> param :: search rest
in parameters := search !parameters
end else if (fst parameters.(i)).sym_name = name then begin
got_argument i arg
end else begin
search (i + 1)
end
in search 0
) named_args;
List.iter (fun param ->
Errors.semantic_error call.call_location
("Missing argument for parameter `" ^ param.sym_name
^ "' of " ^ describe_symbol call.call_target ^ ".")
) !parameters;
(* Check that all parameters have arguments. *)
Array.iter (function
| (_, Some _) -> ()
| (parameter_sym, None) ->
Errors.semantic_error call.call_location
("Missing argument for parameter `" ^ parameter_sym.sym_name
^ "' of " ^ describe_symbol call.call_target ^ ".")
) parameters;
(* Prove that this subprogram's preconditions can be met, assuming
the facts we know. *)
List.iter (prove state context call.call_location) !preconditions;
(* Store the argument binding for later translation stages. *)
call.call_bound_arguments <-
begin
let rec loop bound_arguments = function
| 0 -> bound_arguments
| i ->
let _, Some arg = parameters.(i-1) in
loop (arg::bound_arguments) (i-1)
in loop [] (Array.length parameters)
end;
Unit_type
end
| Static_assert_term(loc, expr, tail) ->

0 comments on commit 9ef7843

Please sign in to comment.