Worklog: Run SATO

Build

⋊> opam var z3:version
4.8.14
⋊> opam var batteries:version
3.5.0
⋊> opam var ocaml:version
4.09.0

The commands are

make sato

Example

./sato test/test-sources/natodefa-types/alias.natodefa
./sato --mode=input -t target assert.odefa

Test

You can comment out test/test.ml line 8 Test_ddpa.tests; to just test SATO.

make test

(* or *)
./_build/default/test/test.exe -list-test
./_build/default/test/test.exe 

Code (for workflow)

Sato-main

Sato.() calls Sato.run_generation with mode Type_checking | Test_generation.

Sato.run_generation calls Generator.generate_answers with hook generation_callback : Ans.t -> unit.

Answer-generation

Generator.generate_answers calls Generator.take_steps to perform the step function. It's a step wrapper for Symbolic-interpreter.Interpreter.step

Symbolic-interpreter

Noting Symbolic-interpreter doesn't depend on Answer-generation. Instead, SATO adds Error collections in Symbolic-interpreter.Interpreter.step.

In my patch, the Error is moved from Odefa.Ast to Nat_odefa.Ast (I forgot why I did this). However, both work.

In interpreter.ml, the rule handlers are extracted out into (Interpreter.)rule_computations from (Interpreter.)lookup.

In rule_computations, each rule handlers call record_visited_clause. For Abort rules, record_abort_point is called.

Code (for multi-targets)

Sato.() calls Sato.run_generation with mode Type_checking | Test_generation.

Each mode uses one first-class module of Generator.Generator as Sato.run_generation's first argument (in sato.ml)

• (module Generator.Make(Generator_answer.Natodefa_type_errors): Generator.Generator)
• (module Generator.Make(Generator_answer.Input_sequence): Generator.Generator)

Natodefa_type_errors and Input_sequence are of module type Generator_answer.Answer. Themselves are less interesting, just converting the result to get the prompting answer to users (answer_from_result)

In Sato.run_generation, the target_vars is computed by get_target_vars:

1. If args.args_target_var is set, use that var
2. If None, use Interpreter_environment.list_instrument_conditionals expr, that are abort_val.abort_conditional_ident in enum_all_aborts_in_expr.

Generator.create uses the first target var to start the interpreter and store all the target vars in gen_target_vars.

gen_target_vars are passed into Generator.take_steps (inner step function) as x_list.

take_steps drives the step based on the current state (gen_ref : generator_reference), that is

1. If #results reach the max_res, exit
2. If #steps reach the max_step_pre_task, exit or Interpreter.start the next target
3. Else, step the current target, and eliminate visited vars in the target vars.

The visited information is passed in as:

1. Symbolic_monad.record_visited_clause appends log_visited_clauses = Ident_set.singleton ident;
2. Any logs are merged in the monadic merging with other log details.
3. Log details are passed to the evaluation step result evaluation_result by er_visited_clauses = log.log_visited_clauses
4. The evaluation step result is passed to the interpreter step result by er_visited = eval_result.M.er_visited_clauses

Therefore, the visited nodes are passed along symbolic_monad, evaluation interpreter, and are used to filter target vars in Generator.take_steps.

On Belief

Here are a few examples running in SATO's input mode

belif/assume.odefa

x = input;
t = true;
z = assume t;
target = x;

⨯ ./sato --mode=input -t target belief/assume.odefa
* Input sequence: [0]
* Found in 21 steps
--------------------
1 input found.
No further control flows exist.

assume_fail.odefa

x = input;
f = false;
z = assume f;
target = x;

⨯ ./sato --mode=input -t target belief/assume_fail.odefa
No inputs found.
No further control flows exist.

abort.odefa

x = input;
t = true;
z = t ? (zt = 2) : (zf = abort);
target = z;

⨯ ./sato --mode=input -t target belief/abort.odefa
* Input sequence: [0]
* Found in 58 steps
--------------------
1 input found.
No further control flows exist.

abort_ill.odefa

x = input;
t = true;
z = abort;
target = x;

⨯ ./sato --mode=input -t target belief/abort_ill.odefa
Program is ill-formed.
* (Ast_wellformedness.Invalid_abort z)

assume.natodefa

let z = assume true in
let target = 1 in target

⨯ ./sato --mode=input -t target belief/assert.natodefa
* Input sequence: []
* Found in 72 steps
--------------------
1 input found.
No further control flows exist.

⨯ ./translator  < belief/assume.natodefa

  bool~0 = true;
  assume~1 = assume bool~0;
  z = assume~1;
  int~2 = 1;
  target = int~2;
  var~3 = target;
  ~result = var~3

assert.natodefa

let z = assert true in
let target = 1 in target

./sato --mode=input -t target belief/assert.natodefa
* Input sequence: []
* Found in 72 steps
--------------------
1 input found.
No further control flows exist.

⨯ ./translator  < belief/assert.natodefa

  bool~0 = true;
  assert_pred~1 = bool~0;
  m~7 = assert_pred~1 ~ bool;
  assert_res~2 = m~7 ? (
                          c_cond~8 = assert_pred~1 ? (assert_res_true~3 = {}) : 
                                                       (ab~4 = abort)
                         ) : (ab~9 = abort);
  z = assert_res~2;
  int~5 = 1;
  target = int~5;
  var~6 = target;
  ~result = var~6

Summary

1. Natodefa has assume e and assert e.
2. Odefa has assume x and abort.
3. Natodefa.assume is translated to Odefa.assume as a clause to bring extra constraint.
4. Natodefa.assert is translated to a condition whose else-block contains just one about clause.
5. In Odefa, abort are not free to use in other places.