This prototype resource-usage-analyzer inputs programs written in the language defined by the following syntax and reports whether each resource created in the programs is accessed properly according to each annotated specification.
Try our resource analyzer from the following form.
(Programs)
P ::= M;; (Program is a term followed by ;;)
(Terms)
M ::= v (values)
| new[spec]() (resource creation)
| acc[alabel](M) (resource access)
| if M1 then M2 else M3 (conditional branch)
| M1M2 (functional application)
| let x = M1 in M2 (local binding)
| M1;M2 (let _ = M1 in M2 (syntax sugar))
| try M1 with M2 (exception handling)
| raise (exception raising)
(Values)
v ::= true (true constant)
| false (false constant)
| x,y,f,g, ... (variables)
| fun(f,x,M) (functions)
| lambda x. M (non-recursive functions (syntax sugar))
(Access labels)
alabel ::= read (read access)
| close (close access)
| write (write access)
(Spec expressions) (specification in a regular expression)
spec ::= (read*);close
| (write*);close
The following program creates a resource which should be accessed according to (read*);close, and accesses the resource with read operation, raises an exception and, handling the exception, the program closes the resource finally.
/* Valid program */ let x=new[read*;close]() in try acc[read](x);raise with acc[close](x);;
The following program fails to close a resource.
/* Invalid program */ let x=new[read*;close]() in try acc[read](x);raise with true;;
The following is a prototypal program that uses recursive function. In the program, a resource is created and accessed repeatedly with read operation until an exception is raised. Then the exception is handled and the resource is closed finally.
/* Valid program */
let z=new[(read*);close]()
in try fun(f, x, if acc[read](x) then raise else f x) z
with acc[close](z);;
The following is a prototypical model of programs that copy data from a read only resource into a write only resource and then close these resources. For example, a fragment of OCaml program
let ic = open_in "filename1" in
let oc = open_out "filename2" in
try
while(true) do
let s = input_line ic (** read_line may raise End_of_File exception **)
in output_string oc (s^"\n")
done
with
End_of_file -> flush oc; close_in ic;close_out oc;;
is expressed as the following program in our language.
/* Valid program */
let x = new[read*;close]() in
let y = new[write*;close]()
in
try
fun(f,z, (if acc[read](x) then true else raise); acc[write](y); f true) true
with
acc[close](x); acc[close](y);;
The following program is equivalent to the above program except for failing to close the write only resource.
/* Invalid program */
let x = new[read*;close]() in
let y = new[write*;close]()
in
try
fun(f,z, (if acc[read](x) then true else raise); acc[write](y); f true) true
with
acc[close](x);;
In the following program, function input_line, which take a resource and access it with read operation and may raise exception, is defined. Then, after a read only resource is created, the resource is read repeatedly using the function until an exception is raised. Finally, when an exception is raised, the exception is handled and the resource is closed.
/*** Valid program ***/
let input_line
= lambda x. if acc[read](x) then true else raise in
let ic = new[read*;close]() in
let f = fun(g,x, input_line x;g x)
in try (f ic)
with acc[close](ic);;
The following program repeatedly creates a new resource and close it. Note that, in this program, arbitrarily many resources my be created, and also arbitrarily many exception handlers can be nested.
/*** Invalid program ***/
let create = fun(f,x, let y=new[read*;close]() in y) in
let repeat =
fun(g,x, let z = create true
in try (if acc[read](z)
then raise
else (g true;acc[read](z)))
with acc[close](z)) in
repeat true;;