Skip to content

Commit

Permalink
Keep sub-modules in SymbolicUtility
Browse files Browse the repository at this point in the history
  • Loading branch information
@benozol
benozol committed Apr 20, 2020
1 parent 166a98f commit 814f712
Show file tree
Hide file tree
Showing 6 changed files with 117 additions and 106 deletions.
24 changes: 12 additions & 12 deletions src/colis.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,7 @@ module Constraints = Colis_constraints
let () =
(* Register the utilities to the mixed backend, which is used in interpreting the
interfaces for constraints and transducers equally *)
List.iter SymbolicUtility.Mixed.register [
List.iter SymbolicUtility.Mixed.Interpreter.register [
(module Basics.True) ;
(module Basics.Colon) ;
(module Basics.False) ;
Expand Down Expand Up @@ -173,13 +173,13 @@ type sym_config = {

module SymbolicConstraints = struct

type state = SymbolicUtility.Constraints.state
type sym_state = SymbolicUtility.Constraints.sym_state
type state = SymbolicUtility.Constraints.Interpreter.state
type sym_state = SymbolicUtility.Constraints.Interpreter.sym_state
type config = SymbolicUtility.Constraints.config = {
prune_init_state: bool;
}

let is_registered = SymbolicUtility.Mixed.is_registered
let is_registered = SymbolicUtility.Mixed.Interpreter.is_registered

let interp_program ~loop_limit ~stack_size ~argument0 stas' program =
let open Common in
Expand Down Expand Up @@ -210,10 +210,10 @@ module SymbolicConstraints = struct
fprintf fmt "id: %s@\n" id;
if !Colis_internals.Options.print_states_dir <> "" then
let filename = sprintf "%s/%s.dot" !Colis_internals.Options.print_states_dir id in
print_dot filename id sta.Constraints.filesystem.clause;
print_dot filename id sta.Constraints.Interpreter.filesystem.clause;
| None -> ()
end;
print_filesystem fmt sta.Constraints.filesystem;
print_filesystem fmt sta.Constraints.Interpreter.filesystem;
(* Print stdin *)
if sta.stdin <> [] then begin
fprintf fmt "stdin: |@\n";
Expand Down Expand Up @@ -266,8 +266,8 @@ module SymbolicConstraints = struct
let open SymbolicUtility in
let context = mk_context ~arguments ~vars in
let filesystems = Constraints.filesystems config sym_config.filesystem_spec in
let stas = List.map Constraints.mk_state filesystems in
let sym_stas = List.map (fun state -> Constraints.{ state; context }) stas in
let stas = List.map Constraints.Interpreter.mk_state filesystems in
let sym_stas = List.map (fun state -> Constraints.Interpreter.{ state; context }) stas in
let results =
interp_program ~loop_limit:sym_config.loop_limit ~stack_size:sym_config.stack_size ~argument0
sym_stas colis
Expand All @@ -286,10 +286,10 @@ module SymbolicConstraints = struct
let root0 = if prune_init_state then None else Some root in
let filesystem =
{root; clause; root0} in
mk_state filesystem
Interpreter.mk_state filesystem

let to_symbolic_state ~vars ~arguments state =
SymbolicUtility.Constraints.{state; context = mk_context ~arguments ~vars}
SymbolicUtility.Constraints.Interpreter.{state; context = mk_context ~arguments ~vars}
end

module SymbolicTransducers = struct
Expand All @@ -305,8 +305,8 @@ module SymbolicTransducers = struct
let context = mk_context ~arguments ~vars in
let stas =
let fs = Transducers.filesystems config sym_config.filesystem_spec in
List.map Transducers.mk_state fs in
List.map (fun state -> Transducers.{ state; context }) stas in
List.map Transducers.Interpreter.mk_state fs in
List.map (fun state -> Transducers.Interpreter.{ state; context }) stas in
let results = SymbolicUtility.Mixed.interp_program_transducers inp sym_stas colis in
exit (exit_code results)
end
4 changes: 2 additions & 2 deletions src/colis.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,8 +110,8 @@ type sym_config = {
module SymbolicConstraints : sig
open Constraints

type state = SymbolicUtility.Constraints.state
type sym_state = SymbolicUtility.Constraints.sym_state
type state = SymbolicUtility.Constraints.Interpreter.state
type sym_state = SymbolicUtility.Constraints.Interpreter.sym_state
type config = SymbolicUtility.Constraints.config = {
prune_init_state: bool; (** Prune the initial symbolic state during symbolic execution for a faster execution *)
}
Expand Down
64 changes: 32 additions & 32 deletions src/symbolic/symbolicUtility.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,12 @@ module type INTERPRETER = sig
val incomplete : utility:string -> string -> utility
val unknown : utility:string -> string -> utility

type utility_context = Semantics__UtilityContext.utility_context = {
cwd: Colis_constraints.Path.normal;
env: string Env.SMap.t;
args: string list;
}

module type SYMBOLIC_UTILITY = sig
val name : string
val interprete : utility_context -> utility
Expand Down Expand Up @@ -421,10 +427,8 @@ module Concrete = struct
let apply_spec fs spec = Option.to_list (spec fs)
end
module Interpreter = MakeInterpreter (Filesystem)
include MakeCombinators (Interpreter)
include MakeSpecifications (Interpreter) (CaseSpec)
include Filesystem
include Interpreter
module Combinators = MakeCombinators (Interpreter)
module Specifications = MakeSpecifications (Interpreter) (CaseSpec)
include CaseSpec

type config = unit
Expand Down Expand Up @@ -473,10 +477,8 @@ module Constraints = struct
end

module Interpreter = MakeInterpreter (Filesystem)
include MakeCombinators (Interpreter)
include MakeSpecifications (Interpreter) (CaseSpec)
include Filesystem
include Interpreter
module Combinators = MakeCombinators (Interpreter)
module Specifications = MakeSpecifications (Interpreter) (CaseSpec)
include CaseSpec

type config = { prune_init_state : bool }
Expand Down Expand Up @@ -506,10 +508,8 @@ module Transducers = struct
end

module Interpreter = MakeInterpreter (Filesystem)
include MakeCombinators (Interpreter)
include MakeSpecifications (Interpreter) (CaseSpec)
include Filesystem
include Interpreter
module Combinators = MakeCombinators (Interpreter)
module Specifications = MakeSpecifications (Interpreter) (CaseSpec)
include CaseSpec

type config = unit
Expand Down Expand Up @@ -567,27 +567,25 @@ module Mixed = struct
end

module Interpreter = MakeInterpreter (Filesystem)
include MakeCombinators (Interpreter)
include MakeSpecifications (Interpreter) (CaseSpec)
include Filesystem
include Interpreter
module Combinators = MakeCombinators (Interpreter)
module Specifications = MakeSpecifications (Interpreter) (CaseSpec)
include CaseSpec

(* Concrete interpretation *)

let state_from_concrete (s : Concrete.state) : state = {
let state_from_concrete (s : Concrete.Interpreter.state) : Interpreter.state = {
filesystem=Concrete s.filesystem;
stdin=s.stdin;
stdout=s.stdout;
log=s.log;
}

let sym_state_from_concrete (s: Concrete.sym_state) : sym_state = {
let sym_state_from_concrete (s: Concrete.Interpreter.sym_state) : Interpreter.sym_state = {
state = state_from_concrete s.state;
context = s.context;
}

let state_to_concrete (s: state) : Concrete.state =
let state_to_concrete (s: Interpreter.state) : Concrete.Interpreter.state =
let filesystem =
match s.filesystem with
| Concrete fs -> fs
Expand All @@ -596,26 +594,26 @@ module Mixed = struct

let interp_program_concrete inp stas pro =
let stas' = List.map sym_state_from_concrete stas in
let normals, errors, failures = interp_program inp stas' pro in
let normals, errors, failures = Interpreter.interp_program inp stas' pro in
List.map state_to_concrete normals,
List.map state_to_concrete errors,
List.map state_to_concrete failures

(* Constraints interpretation *)

let state_from_constraints (s : Constraints.state) : state = {
let state_from_constraints (s : Constraints.Interpreter.state) : Interpreter.state = {
filesystem=Constraints s.filesystem;
stdin=s.stdin;
stdout=s.stdout;
log=s.log;
}

let sym_state_from_constraints (s: Constraints.sym_state) : sym_state = {
let sym_state_from_constraints (s: Constraints.Interpreter.sym_state) : Interpreter.sym_state = {
state = state_from_constraints s.state;
context = s.context;
}

let state_to_constraints (s: state) : Constraints.state =
let state_to_constraints (s: Interpreter.state) : Constraints.Interpreter.state =
let filesystem =
match s.filesystem with
| Constraints fs -> fs
Expand All @@ -624,26 +622,26 @@ module Mixed = struct

let interp_program_constraints inp stas pro =
let stas' = List.map sym_state_from_constraints stas in
let normals, errors, failures = interp_program inp stas' pro in
let normals, errors, failures = Interpreter.interp_program inp stas' pro in
List.map state_to_constraints normals,
List.map state_to_constraints errors,
List.map state_to_constraints failures

(* Transducers interpretation *)

let state_from_transducers (s : Transducers.state) : state = {
let state_from_transducers (s : Transducers.Interpreter.state) : Interpreter.state = {
filesystem=Transducers s.filesystem;
stdin=s.stdin;
stdout=s.stdout;
log=s.log;
}

let sym_state_from_transducers (s: Transducers.sym_state) : sym_state = {
let sym_state_from_transducers (s: Transducers.Interpreter.sym_state) : Interpreter.sym_state = {
state = state_from_transducers s.state;
context = s.context;
}

let state_to_transducers (s: state) : Transducers.state =
let state_to_transducers (s: Interpreter.state) : Transducers.Interpreter.state =
let filesystem =
match s.filesystem with
| Transducers fs -> fs
Expand All @@ -652,24 +650,26 @@ module Mixed = struct

let interp_program_transducers inp stas pro =
let stas' = List.map sym_state_from_transducers stas in
let normals, errors, failures = interp_program inp stas' pro in
let normals, errors, failures = Interpreter.interp_program inp stas' pro in
List.map state_to_transducers normals,
List.map state_to_transducers errors,
List.map state_to_transducers failures
end

module ConstraintsCompatibility = struct

include Mixed
include Mixed.Interpreter
include Mixed.Specifications
include Mixed.Combinators

let success_case ~descr ?stdout constraints =
success_case ~descr ?stdout (case_spec ~constraints ())
success_case ~descr ?stdout (Mixed.case_spec ~constraints ())

let error_case ~descr ?stdout ?error_message constraints =
error_case ~descr ?stdout ?error_message (case_spec ~constraints ())
error_case ~descr ?stdout ?error_message (Mixed.case_spec ~constraints ())

let incomplete_case ~descr constraints =
incomplete_case ~descr (case_spec ~constraints ())
incomplete_case ~descr (Mixed.case_spec ~constraints ())

let noop = Constraints.noop
end
Loading

0 comments on commit 814f712

Please sign in to comment.