Skip to content

Commit f31bf75

Browse files
Add Ada bindings for the runtime
Closes eng/fuzz/symcc#4.
1 parent 97de5f1 commit f31bf75

File tree

4 files changed

+112
-0
lines changed

4 files changed

+112
-0
lines changed

runtime/bindings/README

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
2+
3+
Runtime bindings
4+
5+
6+
This directory contains bindings to the user-facing functionality of the runtime
7+
(see runtime/RuntimeCommon.h). The bindings give target programs written in
8+
different languages access to runtime features like in-memory input or custom
9+
test-case handlers.

runtime/bindings/ada/README

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
2+
3+
Ada bindings
4+
5+
6+
This directory contains Ada bindings for the SymCC runtime. To use them in your
7+
Ada code, you can either point gprbuild here directly (e.g., by setting
8+
GPR_PROJECT_PATH appropriately), or you can install them in the system:
9+
10+
$ gprbuild -Psymcc
11+
$ gprinstall -Psymcc
12+
13+
Either way, you'll then be able to include SymCC in your project definition
14+
(i.e., the .gpr file for your project):
15+
16+
with "symcc";
17+
18+
This will let you use the bindings in your Ada code, for example:
19+
20+
with SymCC; use SymCC;
21+
22+
-- ...
23+
24+
-- Register a procedure that receives new program inputs.
25+
SymCC_Set_Test_Case_Handler (My_Handler);
26+
27+
-- Tell SymCC where to find the input in memory. Note that the variable needs
28+
-- to be declared with the "aliased" keyword.
29+
SymCC_Make_Symbolic (Input'Address, Input'Size / System.Storage_Unit);
30+
31+
-- Run your code on the input; SymCC will follow the computations
32+
-- symbolically and call My_Handler whenever it produces a new test input.
33+
My_Code_Under_Test (Input);
34+
35+
See the doc comments in symcc.ads for details, or generate HTML documentation
36+
with "gnatdoc -Psymcc".

runtime/bindings/ada/symcc.ads

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
-- This file is part of the SymCC runtime.
2+
3+
-- The SymCC runtime is free software: you can redistribute it and/or modify
4+
-- it under the terms of the GNU Lesser General Public License as published by
5+
-- the Free Software Foundation, either version 3 of the License, or (at your
6+
-- option) any later version.
7+
8+
-- The SymCC runtime is distributed in the hope that it will be useful, but
9+
-- WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
10+
-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public
11+
-- License for more details.
12+
13+
with Interfaces.C;
14+
with System;
15+
16+
-- @summary
17+
-- Ada bindings to the SymCC runtime API.
18+
--
19+
-- @description
20+
-- This package provides thin bindings to the user-facing functionality of the
21+
-- SymCC runtime (see RuntimeCommon.h).
22+
package SymCC is
23+
24+
procedure SymCC_Make_Symbolic
25+
(Address : System.Address; Size : Interfaces.C.size_t) with
26+
Import => True, Convention => C, External_Name => "symcc_make_symbolic";
27+
-- Mark a memory region as symbolic program input.
28+
-- @param Address The start of the region containing the input data.
29+
-- @param Size The length in bytes of the region.
30+
31+
type Test_Case_Handler_Callback_Type is
32+
access procedure
33+
(Data_Block : System.Address; Size : Interfaces.C.size_t) with
34+
Convention => C;
35+
-- Type of functions that the runtime can call when it generates new
36+
-- program inputs (see SymCC_Set_Test_Case_Handler).
37+
38+
procedure SymCC_Set_Test_Case_Handler
39+
(Callback : Test_Case_Handler_Callback_Type) with
40+
Import => True,
41+
Convention => C,
42+
External_Name => "symcc_set_test_case_handler";
43+
-- Define a custom handler for new program inputs.
44+
-- @param Callback The procedure to be called for each new input.
45+
46+
end SymCC;

runtime/bindings/ada/symcc.gpr

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
-- This file is part of the SymCC runtime.
2+
3+
-- The SymCC runtime is free software: you can redistribute it and/or modify
4+
-- it under the terms of the GNU Lesser General Public License as published by
5+
-- the Free Software Foundation, either version 3 of the License, or (at your
6+
-- option) any later version.
7+
8+
-- The SymCC runtime is distributed in the hope that it will be useful, but
9+
-- WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
10+
-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public
11+
-- License for more details.
12+
13+
library project SymCC is
14+
15+
for Library_Name use "symcc";
16+
for Library_Dir use "lib";
17+
18+
for Languages use ("Ada");
19+
for Object_Dir use "obj";
20+
21+
end SymCC;

0 commit comments

Comments
 (0)