Commit f9dbbab6 authored by Alexander Wilhelm's avatar Alexander Wilhelm
Browse files

[CHN]: 'user_tasks_image' type & round-robin-scheduling

parent c3d2c9a7
......@@ -54,6 +54,7 @@ let unoption = function
| _ -> raise @@ Invalid_argument "Analyze.unoption"
let find_opt f =
Printf.printf "find_opt\n";
try Some (f ())
with Not_found -> None
......@@ -246,6 +247,7 @@ let transfer_dhunk ctx dhunk state =
let instr_cache = Addr_tbl.create 5000
let decode_instr addr =
Printf.printf "decode_instr\n";
try Addr_tbl.find instr_cache addr
with Not_found ->
Logger.result "instruction cache miss";
......@@ -274,6 +276,7 @@ let transfer_instruction_nostub ctx address state =
transfer_dhunk ctx dhunk state |> Addr_map.of_list
let transfer_instruction ctx address trace state =
Printf.printf "transfer_instruction\n";
match Addr_tbl.find skip_table address with
| (SkipTo (_skip_type, dest), msg) ->
Logger.result "Skipping to %a. Reason: %s" Virtual_address.pp dest msg;
......@@ -368,6 +371,7 @@ and previous_func = ref "<start>"
(** Like {analyze_address} but does not call {next} on the first, and thus will
not stop if {address} was already visited. *)
and analyze_address_nocheck ctx state trace address =
Printf.printf "analyze_address_nocheck\n";
let successors =
match Addr_tbl.find skip_table address with
| (SkipTo (skip_type, dest), msg) ->
......@@ -547,6 +551,7 @@ let handle_successors ctx successors state_table state trace r' src =
table.
*)
let rec analyze_regex state_table ctx trace r =
Printf.printf "analyze_regex\n";
let open Regex in
let open Cfg_analysis.CfgRegex in
(* We propagate two things along the regex: a boolean that tells whether the
......@@ -554,14 +559,17 @@ let rec analyze_regex state_table ctx trace r =
* regexes, the state is memoized in a hash table. *)
if not (Regex_tbl.mem state_table r) then match r with
| Empty ->
Printf.printf "--Empty\n";
(* We cannot return a normal result, because if the input is, e.g.,
[Append (Empty, r)] we don't want [r] to be analysed. *)
raise @@ Invalid_argument "analyze_regex: empty regex"
| Epsilon ->
Printf.printf "--Epsilon\n";
(* Epsilon should always be in the state table before calling this
* function, so this is an error *)
raise @@ Invalid_argument "analyze_regex: epsilon not found in state table"
| Append (_,r',(src,_)) ->
Printf.printf "--Append\n";
analyze_regex state_table ctx trace r';
Codex_logger.current_instr_addr := fst src;
Logger.result "analyze_regex, case Append, src = %a" Cfg_analysis.V.pretty src;
......@@ -585,6 +593,7 @@ let rec analyze_regex state_table ctx trace r =
let exception Does_not_apply in
begin try match Addr_tbl.find skip_table (fst src) with
| (SkipTo (_,new_dst), msg) ->
Printf.printf "----SkipTo\n";
Logger.result "Skipping to %a. Reason: %s"
Virtual_address.pp new_dst msg;
(* Do not interpret the skipped instruction. Instead, set the entry
......@@ -592,6 +601,7 @@ let rec analyze_regex state_table ctx trace r =
* instruction. *)
Regex_tbl.add ctx state_table r state
| (Hook f, msg) ->
Printf.printf "----Hook\n";
(* Execute the hook function and record all the successors in the
* state table. We assume that the hook function is sound, and
* therefore that all edges going from {src} in the current CFG will
......@@ -604,17 +614,21 @@ let rec analyze_regex state_table ctx trace r =
Logger.result "Hook function executed.";
handle_successors ctx successors state_table state trace r' src
| (EndPath, _) ->
Printf.printf "----EndPath\n";
(* Don't interpret this instruction and don't add it to the regex ->
* state mapping. *)
()
| (Unroll _, _) ->
Printf.printf "----Unroll\n";
(* Do nothing special: unrolling is managed by the {AppendStar}
* case. *)
raise Does_not_apply
| (ChangeState _, _) ->
Printf.printf "----ChangeState\n";
(* This is handled elsewhere *)
raise Does_not_apply
| exception Not_found -> raise Does_not_apply
Printf.printf "----exception Not_found\n";
with Does_not_apply ->
let instr = decode_instr (fst src) in
let dhunk = instr.Instruction.dba_block in
......@@ -636,6 +650,7 @@ let rec analyze_regex state_table ctx trace r =
handle_successors ctx exits state_table state trace r' src
end
| AppendStar (_,r',x) ->
Printf.printf "--AppendStar\n";
analyze_regex state_table ctx trace r';
let init_state = Regex_tbl.find ctx state_table r' in
if init_state.State.is_bottom then Regex_tbl.add ctx state_table r init_state
......@@ -741,6 +756,7 @@ let rec analyze_regex state_table ctx trace r =
end
end
| Join (_,r1,r2) ->
Printf.printf "--Join\n";
Logger.result "JOIN";
analyze_regex state_table ctx trace r1;
let state1 = Regex_tbl.find ctx state_table r1 in
......@@ -927,6 +943,7 @@ let cpu_sp =
CPU's stack pointer and the MPIDR register set accordingly. {old} and {new}
must be between 0 and 3 included. *)
let switch_cpu ctx old new_ state =
Printf.printf "switch_cpu\n";
let open Framac_ival in
let size = 32 in
let exception Stack_pointer_not_singleton in
......
......@@ -257,6 +257,7 @@ module Create () : Sig = struct
(b3 lsl 24) lor (b2 lsl 16) lor (b1 lsl 8) lor b0
let load_image ptrsize img ctx memory =
Printf.printf "load_image\n";
let program_headers = Loader_elf.program_headers img in
let memory = Array.fold_left (fun mem phdr ->
let open Loader_elf in
......@@ -385,12 +386,15 @@ module Create () : Sig = struct
memory
let initial_memory img ctx =
Printf.printf "initial_memory\n";
let ptrsize = Codex_config.ptr_size () in
Printf.printf "ptrsize: 0x%x\n" ptrsize;
let img = match img with
| Loader.PE _ | Loader.Dump _ -> assert false
| Loader.ELF img -> img in
let load_img = load_image ptrsize img in
let root_type_sym, root_type = TSettingC.root in
Printf.printf "Looking for root_type_sym: %s\n" root_type_sym;
let root_type_addr = match Loader_utils.address_of_symbol ~name:root_type_sym
(Loader.ELF img) with None -> assert false | Some a -> Virtual_address.create a in
let add_bridge_section =
......
......@@ -273,6 +273,7 @@ let task_description =
})
(*
let user_tasks_image =
mk (Structure {
st_name = Some ("user_tasks_image");
......@@ -294,6 +295,16 @@ let user_tasks_image =
(24, "reserve", ptr_notnull (mk @@ Array (context, Some (Const (Z.of_int 10)))));
];
})
*)
let user_tasks_image =
mk (Structure {
st_name = Some ("user_tasks_image");
st_byte_size = Some (4);
st_members =
[ (0, "nb_tasks", const (with_ (Pred.eq (Sym "nb_tasks")) (mk @@ Base (4, "unsigned int"))));
];
})
(********** END OF AUTOGENERATED **********)
......
#!/bin/bash
config=mini_os/binsec.ini
compiler="gcc"
scheduler="rr"
opt_flags="s" # optimize for size
dyn_threads="-codex-no-dyn-threads" # leave empty for dynamic task creationg
shape= # TODO
printing="noprint"
ntasks=2
dlevel=1
exe=mini_os/main.exe
# Compiler settings
if [ $compiler = "gcc" ]; then
export CC=gcc
elif [ $compiler = "clang" ]; then
export CC=clang
fi
# Scheduler settings
if [ $scheduler = "edf" ]; then
export SCHEDULER=EDF_SCHEDULING
elif [ $scheduler = "fp" ]; then
export SCHEDULER=FP_SCHEDULING
elif [ $scheduler = "rr" ]; then
export SCHEDULER=ROUND_ROBIN_SCHEDULING
fi
# Optimization setttings
export OPT_FLAGS=-O${opt_flags}
# Dynamic thread creation settings
if [ $dyn_threads = "-codex-no-dyn-threads" ]; then
export DYNAMIC_TASK_CREATION=no
else
export DYNAMIC_TASK_CREATION=yes
fi
# Debug printing settings
if [ $printing = "noprint" ]; then
export DEBUG_PRINTING=no
elif [ $printing = "print" ]; then
export DEBUG_PRINTING=yes
fi
# Execution
echo "Compile miniOS without bugs"
cd mini_os/
make clean
make
cd ..
echo "Execute BINSEC/Codex"
echo "binsec -config $config $exe -codex-x86-types $scheduler -codex-nb-tasks $ntasks $dyn_threads -codex-debug-level $dlevel"
binsec -config $config $exe -codex-x86-types $scheduler -codex-nb-tasks $ntasks $dyn_threads -codex-debug-level $dlevel
echo "Convert .dot files into post-script files"
dot -Tps handlers_cpu0.dot -o handlers_cpu0.ps
dot -Tps init_concrete_cpu0.dot -o init_concrete_cpu0.ps
dot -Tps init_cpu0.dot -o init_cpu0.ps
......@@ -12,12 +12,12 @@ void init() {
int bla = 42;
}
void _start(void) {
init();
start_user_space();
}
/*
asm("\
.global asm_syscall_handler\n\t\
.type asm_syscall_handler, @function\n\
......@@ -25,6 +25,14 @@ asm_syscall_handler:\n\t"
" jmp error_infinite_loop\n\
.size asm_syscall_handler, . - asm_syscall_handler\n\
");
*/
void asm_syscall_handler(void) {
/* Round-robing-scheduler */
static int count = 0;
tasks[count]();
count = (count + 1) % user_tasks_image.nb_tasks;
}
asm("\
.global error_infinite_loop\n\
......
......@@ -9,4 +9,18 @@ int two();
extern int (*tasks[NTASKS])();
void start_user_space(void);
/* High-level description of the application. */
extern const struct user_tasks_image {
unsigned int const nb_tasks;
/*
unsigned int const nb_contexts;
struct task_description const *const tasks;
struct low_level_description const low_level;
char *idle_start;
char *idle_end;
struct context * const idle_ctx_array;
struct context * reserve;
*/
} user_tasks_image;
#endif /* TASKS_H */
#include "kernel.h"
#include "tasks.h"
const struct user_tasks_image user_tasks_image = {
.nb_tasks = 2
};
int (*tasks[NTASKS])() = {one, two};
void start_user_space() {
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment