Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add a concrete backend to the symbolic engine #134

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Add a concrete backend to the symbolic engine #134

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
166a98f
Start concrete backend for symbolic engine
benozol Apr 20, 2020
814f712
Keep sub-modules in SymbolicUtility
benozol Apr 20, 2020
a6deefc
Comment
benozol Apr 20, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions src/colis.ml
View file
Open in desktop
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
Open in desktop
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
127 changes: 97 additions & 30 deletions src/symbolic/symbolicUtility.ml
View file
Open in desktop
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 @@ -408,6 +414,28 @@ struct
List.flatten (List.map (apply_case state) cases)
end

(** Concrete *)

module Concrete = struct
module Filesystem = struct
type filesystem = FilesystemSpec.t
end
module CaseSpec = struct
include Filesystem
type case_spec = filesystem -> filesystem option
let noop fs = Some fs
let apply_spec fs spec = Option.to_list (spec fs)
end
module Interpreter = MakeInterpreter (Filesystem)
module Combinators = MakeCombinators (Interpreter)
module Specifications = MakeSpecifications (Interpreter) (CaseSpec)
include CaseSpec

type config = unit

let filesystems () fs = [fs]
end

(* Constraints *)

module Constraints = struct
Expand Down Expand Up @@ -449,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 @@ -482,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 All @@ -500,6 +524,7 @@ module Mixed = struct

module Filesystem = struct
type filesystem =
| Concrete of Concrete.filesystem
| Constraints of Constraints.filesystem
| Transducers of Transducers.filesystem
end
Expand All @@ -509,24 +534,30 @@ module Mixed = struct

(* The case_specs are wrapped in a closure because they may raise Incomplete_case_spec *)
type case_spec = {
concrete: unit -> Concrete.CaseSpec.case_spec;
constraints: unit -> Constraints.CaseSpec.case_spec;
transducers: unit -> Transducers.CaseSpec.case_spec;
}

let case_spec ?transducers ?constraints () : case_spec =
let case_spec ?concrete ?transducers ?constraints () : case_spec =
let case_spec_or_incomplete opt () =
match opt with Some x -> x | None -> raise Incomplete_case_spec in
{constraints = case_spec_or_incomplete constraints;
{concrete = case_spec_or_incomplete concrete;
constraints = case_spec_or_incomplete constraints;
transducers = case_spec_or_incomplete transducers}

let noop : case_spec =
case_spec
~concrete:Concrete.noop
~transducers:Transducers.noop
~constraints:Constraints.noop
()

let apply_spec fs spec =
match fs with
| Concrete fs ->
Concrete.apply_spec fs (spec.concrete ()) |>
List.map (fun fs -> Concrete fs)
| Constraints fs ->
Constraints.apply_spec fs (spec.constraints ()) |>
List.map (fun fs -> Constraints fs)
Expand All @@ -536,73 +567,109 @@ 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

let state_from_constraints (s : Constraints.state) : state = {
(* Concrete interpretation *)

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.Interpreter.sym_state) : Interpreter.sym_state = {
state = state_from_concrete s.state;
context = s.context;
}

let state_to_concrete (s: Interpreter.state) : Concrete.Interpreter.state =
let filesystem =
match s.filesystem with
| Concrete fs -> fs
| _ -> invalid_arg "state_to_concrete" in
{filesystem; stdin=s.stdin; stdout=s.stdout; log=s.log}

let interp_program_concrete inp stas pro =
let stas' = List.map sym_state_from_concrete stas 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.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
| Transducers _ -> invalid_arg "state_to_constraints" in
| _ -> invalid_arg "state_to_constraints" in
{filesystem; stdin=s.stdin; stdout=s.stdout; log=s.log}

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
List.map state_to_constraints normals, List.map state_to_constraints errors, List.map state_to_constraints failures
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
| Constraints _ -> invalid_arg "state_to_transducers" in
| _ -> invalid_arg "state_to_transducers" in
{filesystem; stdin=s.stdin; stdout=s.stdout; log=s.log}

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
List.map state_to_transducers normals, List.map state_to_transducers errors, List.map state_to_transducers failures
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