From a217edbc63bab4559419f4902978c06f338d1acf Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Tue, 1 Jul 2008 12:35:03 +0000 Subject: [PATCH] CIL examples. --- cil-tools/Makefile.in | 25 ++++++++++++++++++++++--- cil-tools/ext3.c | 8 ++++---- cil-tools/ext3.ml | 29 +++++++++++++++++++++++++++++ cil-tools/task_struct.c | 1 + cil-tools/task_struct.ml | 17 +++++++++++++++++ 5 files changed, 73 insertions(+), 7 deletions(-) create mode 100644 cil-tools/ext3.ml create mode 100644 cil-tools/task_struct.ml diff --git a/cil-tools/Makefile.in b/cil-tools/Makefile.in index c50e05c..7a0d9db 100644 --- a/cil-tools/Makefile.in +++ b/cil-tools/Makefile.in @@ -32,6 +32,8 @@ OCAMLOPTFLAGS = OCAMLOPTPACKAGES = $(OCAMLCPACKAGES) OCAMLOPTLIBS = $(OCAMLOPTPACKAGES) camlp4lib.cmxa -linkpkg ../bitmatch.cmxa ../bitmatch_persistent.cmxa +PP = -pp "camlp4o -I .. bitmatch.cma bitmatch_persistent.cma pa_bitmatch.cmo" + OCAMLDOCFLAGS = -html -sort all: bitmatch-import-c bitmatch-import-c.opt @@ -45,20 +47,37 @@ bitmatch-import-c.opt: bitmatch_import_c.cmx test: # Examples. +# +# To compile task_struct you'll need to grab a copy of the Linux +# kernel original header files and set the directory below. #DEBUG = DEBUG = --debug -LINUX_HEADERS = linux-2.6.25.4-headers +LINUX_HEADERS = linux-2.6.25.7-headers LINUX_INCLUDES = -I $(LINUX_HEADERS) -examples: ext3.ml task_struct.ml +#EXAMPLES = ext3 task_struct +EXAMPLES = ext3 + +examples: $(EXAMPLES) + +ext3: ext3.cmo ext3.bmpp + $(OCAMLFIND) ocamlc $(OCAMLCFLAGS) $(OCAMLCLIBS) $< -o $@ + +ext3.cmo: ext3.ml + $(OCAMLFIND) ocamlc $(OCAMLCFLAGS) $(OCAMLCPACKAGES) $(PP) -c $< -o $@ ext3.bmpp: ext3.c bitmatch-import-c - cd $(LINUX_HEADERS) && ln -sf asm-x86 asm rm -f $@.new ./bitmatch-import-c $(DEBUG) $(LINUX_INCLUDES) $< > $@.new mv $@.new $@ +task_struct: task_struct.cmo task_struct.bmpp + $(OCAMLFIND) ocamlc $(OCAMLCFLAGS) $(OCAMLCLIBS) $< -o $@ + +task_struct.cmo: task_struct.ml + $(OCAMLFIND) ocamlc $(OCAMLCFLAGS) $(OCAMLCPACKAGES) $(PP) -c $< -o $@ + task_struct.bmpp: task_struct.c bitmatch-import-c cd $(LINUX_HEADERS) && ln -sf asm-x86 asm rm -f $@.new diff --git a/cil-tools/ext3.c b/cil-tools/ext3.c index 1e1a82d..cf4f695 100644 --- a/cil-tools/ext3.c +++ b/cil-tools/ext3.c @@ -1,9 +1,10 @@ /* This is an example import file, showing how to import the ext3 * superblock automatically from Linux header files. * - * Use: bitmatch-import-c ext3.c > ext3_stubs.ml + * Use: bitmatch-import-c ext3.c > ext3.bmpp * * Tip: Add the --debug flag to that command line to see what's going on. + * Also use bitmatch-objinfo to examine the bmpp file. */ /* These are required by Linux in order to get the little/big-endian @@ -17,10 +18,9 @@ * interested in. */ #include -//#include -#include +#include /* This tells the importer program what structures and constants to import. */ //typedef struct ext3_super_block BITMATCH_IMPORT(ext3_super_block); -typedef struct ext2_super_block BITMATCH_IMPORT(ext2_super_block); +typedef struct ext3_super_block BITMATCH_IMPORT(ext3_super_block); BITMATCH_CONSTANT_INT32 (ext3_super_magic, EXT3_SUPER_MAGIC); diff --git a/cil-tools/ext3.ml b/cil-tools/ext3.ml new file mode 100644 index 0000000..dbbe210 --- /dev/null +++ b/cil-tools/ext3.ml @@ -0,0 +1,29 @@ +(* This is an example program using an imported C structure. + * + * The C structure is imported from via "ext3.c" + * by the bitmatch-import-c program, and saved as "ext3.bmpp". + * + * Then we can load "ext3.bmpp" here. + *) + +open Printf + +open bitmatch "ext3.bmpp" + +let () = + (* Load a real ext3 superblock from the examples directory. *) + let bits = Bitmatch.bitstring_of_file "examples/ext3_sb" in + + bitmatch bits with + | { :ext3_super_block } -> + printf "ext3 superblock:\n"; + printf " s_inodes_count = %ld\n" s_inodes_count; + printf " s_blocks_count = %ld\n" s_blocks_count; + printf " s_free_inodes_count = %ld\n" s_free_inodes_count; + printf " s_free_blocks_count = %ld\n" s_free_blocks_count; + printf " s_uuid = %S\n" s_uuid; + printf " s_volume_name = %S\n" s_volume_name; + printf " s_last_mounted = %S\n" s_last_mounted + + | { _ } -> + failwith "input is not an ext2/3 superblock" diff --git a/cil-tools/task_struct.c b/cil-tools/task_struct.c index b17f925..51a4c29 100644 --- a/cil-tools/task_struct.c +++ b/cil-tools/task_struct.c @@ -4,6 +4,7 @@ * Use: bitmatch-import-c task_struct.c > task_struct.ml * * Tip: Add the --debug flag to that command line to see what's going on. + * Also use bitmatch-objinfo to examine the bmpp file. */ /* Any defines, etc. necessary to get the include to work. */ diff --git a/cil-tools/task_struct.ml b/cil-tools/task_struct.ml new file mode 100644 index 0000000..763c718 --- /dev/null +++ b/cil-tools/task_struct.ml @@ -0,0 +1,17 @@ +(* This is an example program using an imported C structure. + * + * The Linux process table entry structure is imported from + * via "task_struct.c" by the bitmatch-import-c + * program, and saved as "task_struct.bmpp". + * + * Then we can load "task_struct.bmpp" here. + *) + +open Printf + +open bitmatch "task_struct.bmpp" + +(* +let () = + let bits = Bitmatch.bitstring_of_file "examples/ext3_sb" in +*) -- 1.8.3.1