Logic

design/README.md

@@ -0,0 +1,7 @@
+# Soteria Design Documents
+
+This folder contains documents used for discussing or exposing the design of complex features in Soteria or Soteria-based interpreters.
+
+PRs that may add a lot of complexity to Soteria may be preceded or come with a design document for discussion.
+
+- [Logic and Syntax in Soteria](./syntax.md)

design/syntax.md

@@ -0,0 +1,36 @@
+# Logic and Syntax
+
+## Introduction
+
+Soteria is originally designed as a *semantic* framework. The syntactic representation of symbolic values, that is, interpreters are constructed independently of the existence of variables or the AST of symbolic values. In essence, this is what makes Soteria "natural" to use for writing interpreters, it hides away the "symbols" in "symbolic execution".
+
+Unfortunately, this beautiful abstraction makes it impossible to reason about function summaries (used e.g. in bi-abduction), or type summaries (used in RUXt). Our goal is to extend Soteria with a way to reason about syntax, without adding too much complexity, and without exposing too much grungy details to the user.
+
+Note that Soteria already has some embryonic support for syntax, used for bi-abduction in Soteria-C. However, this support is limited, does not generalise well, and is currently incompatible with over-approximation (which is necessary for some optimisations in RUXt).
+
+## Syntactic reasoning
+
+We re-use concepts from Compositional Symbolic Execution (CSE) to reason about syntax. All CSE tools use a notion of *producer* and *consumer* of assertion, where a producer is morally a "separation logic assume", and a consumer is a "separation logic assert". Producer "adds" an assertion to the current symbolic state, while a consumer removes an assertion from the current state.
+
+Function specifications can then be *executed* by first consuming the precondition, and then producing the postcondition. Similarly, implications of the form `A ⊢ B` can be checked by producing `A` and then consuming `B` (in OX mode).
+
+# TO EXPLAIN
+
+- Identity producer
+- Syntax needs of substitution, define it in a single place
+- Why ability to consume needs to be checked pre-emptively
+
+
+## Bikeshedding list
+
+- All `subst` functions require a `Typed.cast`, can we get around this?
+- fixes are now `syn list list`, this makes sense but can we add some type beauty to it?
+- The horrible interface Value.Syn.Subst
+- The specifications of the various functions in Value.Syn have too many invariants. How much could we simplify it?
+- `State_monad`:
+  - Exactly duplicates the code of Symex for Producer and Consumer. Needs to become a functor to avoid this
+  - Has to expose `nondet_UNSAFE`, though possibly we could make `subst` produce something *within a monad*. Modular explicit would be extremely helpful, but in the meantime we can make a mini functor that we instantiate inline.
+
+
+## TODOS
+  - Go through Symex interface and remove all things that are useless. Specifically, old consume_pure!

soteria-linear/semantic/aux.ml

@@ -1,5 +1,6 @@
 open Soteria_linear_ast.Lang
 module Typed = Soteria.Tiny_values.Typed
+module Syn = Soteria.Tiny_values.Typed.Syn
 
 module Symex =
   Soteria.Symex.Make
@@ -10,18 +11,32 @@ module S_int = struct
   include Typed
 
   type t = Typed.T.sint Typed.t
+  type syn = Syn.t [@@deriving show { with_path = false }]
 
   let simplify = Symex.simplify
   let fresh () = Symex.nondet Typed.t_int
   let pp = Typed.ppa
+
+  let subst (f : syn -> 'a Typed.t) (e : syn) : t =
+    (* FIXME: I don't know how to do without `Typed.cast`... *)
+    Typed.cast (f e)
+
+  let to_syn = Syn.of_value
+  let exprs_syn (s : syn) : Symex.Value.Syn.t list = [ s ]
 end
 
 module S_val = struct
   include Typed
 
   type t = T.any Typed.t [@@deriving show { with_path = false }]
+  type syn = Syn.t [@@deriving show { with_path = false }]
 
-  let sem_eq = sem_eq_untyped
+  let subst (f : syn -> 'a Typed.t) (e : syn) : t = Typed.cast (f e)
+  let to_syn = Syn.of_value
+  let exprs_syn (s : syn) : Symex.Value.Syn.t list = [ s ]
+
+  let learn_eq (syn : syn) (v : t) : (unit, 'a) Symex.Consumer.t =
+    Symex.Consumer.learn_eq syn v
 
   let fresh () : t Symex.t =
     Symex.branches
@@ -39,14 +54,8 @@ module S_val = struct
     else Symex.Result.ok (Typed.cast v)
 end
 
-type _ Effect.t += Resolve_function : string -> Fun_def.t Effect.t
 type subst = S_val.t String_map.t [@@deriving show { with_path = false }]
 
-let get_function fname = Effect.perform (Resolve_function fname)
-
-let with_program (program : Program.t) f =
-  try f ()
-  with effect Resolve_function name, k -> (
-    match String_map.find_opt name program with
-    | Some func_def -> Effect.Deep.continue k func_def
-    | None -> failwith ("Function not found: " ^ name))
+module PMap = Soteria.Sym_states.Pmap.Make (Symex) (S_int)
+module Excl_val = Soteria.Sym_states.Excl.Make (Symex) (S_val)
+module Freeable = Soteria.Sym_states.Freeable.Make (Symex)

soteria-linear/semantic/bi_state.ml

@@ -1,25 +1,32 @@
 open Aux
 module Bi = Soteria.Sym_states.Bi_abd.Make (Symex)
 
-type t = (State.t, State.fixes) Bi.t [@@deriving show { with_path = false }]
-type fixes = State.fixes [@@deriving show { with_path = false }]
+type t = (State.t option, State.syn) Bi.t
+[@@deriving show { with_path = false }]
+
+type syn = State.syn [@@deriving show { with_path = false }]
+type fixes = State.syn list [@@deriving show { with_path = false }]
 type err = State.err * t [@@deriving show { with_path = false }]
 
 let pp_spec ft ((st, pre), pc, res) =
-  let post = State.serialize st in
+  let post = State.to_syn st in
   Fmt.pf ft
     "@[<v>@[<2>Requires:@ %a@]@ @[<2>Ensures:@ %a@]@ @[<2>PC: %a@]@ %a@]"
-    State.pp_fixes (List.concat pre) State.pp_fixes post
+    pp_fixes pre pp_fixes post
     (Fmt.list ~sep:(Fmt.any "@ && ") Symex.Value.ppa)
     pc
     (Fmt.Dump.result ~ok:S_val.pp ~error:State.pp_err)
     res
 
 let empty = (State.empty, [])
 let bi_wrap f = (Bi.wrap ~produce:State.produce) f
-let load addr = bi_wrap (State.load addr)
+
+let load addr : t -> (S_val.t * t, err, syn list) Symex.Result.t =
+  bi_wrap (State.load addr)
+
 let store addr value = bi_wrap (State.store addr value)
 let alloc st = bi_wrap State.alloc st
 let free addr = bi_wrap (State.free addr)
 let produce fix t = Bi.produce State.produce fix t
+let consume fix t = Bi.consume ~produce:State.produce State.consume fix t
 let error msg state = (`Interp msg, state)

soteria-linear/semantic/context.ml

@@ -0,0 +1,78 @@
+(** This module revolves around analysis contexts, which are a program, as well
+    as anything that is relevant to run the analysis. *)
+
+open Soteria_linear_ast.Lang
+open Aux
+module Logic = Soteria.Logic.Make (Symex)
+
+module Spatial_atom : Logic.Asrt.S with type t = State.syn = struct
+  type t = State.syn [@@deriving show]
+
+  let ins_outs = State.ins_outs
+end
+
+module With_pure = Logic.Asrt.With_pure (Spatial_atom)
+module Atom = With_pure.Atom
+
+type spec = (Atom.t list, State.err) Logic.Spec.t
+
+type t = {
+  program : Program.t;
+  specs : spec list Hashtbl.Hstring.t;
+  use_specs : bool;
+  being_analysed : string Dynarray.t;
+}
+
+let make ~use_specs ~program () =
+  {
+    program;
+    specs = Hashtbl.Hstring.create 0;
+    use_specs;
+    being_analysed = Dynarray.create ();
+  }
+
+type _ Effect.t +=
+  | Get_function : string -> Fun_def.t Effect.t
+  | Get_specs : string -> spec list option Effect.t
+  | Add_spec : string * spec list -> unit Effect.t
+  | Use_specs : bool Effect.t
+
+let get_function name = Effect.perform (Get_function name)
+let get_specs name = Effect.perform (Get_specs name)
+let add_spec name spec = Effect.perform (Add_spec (name, spec))
+let use_specs () = Effect.perform Use_specs
+
+let with_context ctx f =
+  try f () with
+  | effect Get_function name, k ->
+      let func = String_map.find name ctx.program in
+      Effect.Deep.continue k func
+  | effect Get_specs name, k ->
+      let res = Hashtbl.Hstring.find_opt ctx.specs name in
+      Effect.Deep.continue k res
+  | effect Add_spec (name, specs), k ->
+      let current_specs =
+        Hashtbl.Hstring.find_opt ctx.specs name |> Option.value ~default:[]
+      in
+      Hashtbl.Hstring.replace ctx.specs name (current_specs @ specs);
+      Effect.Deep.continue k ()
+  | effect Use_specs, k -> Effect.Deep.continue k ctx.use_specs
+
+module Asrt_model (State : State_intf.S) = struct
+  module Spatial_atom_model :
+    Logic.Asrt.Model(Spatial_atom).S
+      with type state = State.t
+       and type fix = State.syn = struct
+    type state = State.t
+    type fix = State.syn
+
+    let produce = State.produce
+    let consume = State.consume
+  end
+
+  module Model_with_pure = With_pure.Model (Spatial_atom_model)
+  include Logic.Asrt.Model_with_star (With_pure.Atom) (Model_with_pure)
+
+  let execute (spec : spec) (args : 'a Typed.t list) (state : State.t option) =
+    Logic.Spec.execute ~consume ~produce spec args state
+end

soteria-linear/semantic/dune

@@ -1,5 +1,6 @@
 (library
  (name soteria_linear_semantic)
  (libraries soteria_linear_ast soteria)
+ (flags :standard -open Soteria.Soteria_std)
  (preprocess
   (pps ppx_deriving.std soteria.ppx)))

soteria-linear/semantic/interp.ml

@@ -5,6 +5,11 @@ open Symex.Syntax
 open S_val.Infix
 open Soteria.Logs
 
+let collapse_spec_execution_error (error : (State.err, cons_fail) Either.t) =
+  function
+  | Either.Left err -> err
+  | Either.Right err -> err
+
 let cast_both (ty : [< S_val.T.any ] S_val.ty) v1 v2 =
   let v1 = S_val.cast_checked v1 ty in
   let v2 = S_val.cast_checked v2 ty in
@@ -22,8 +27,8 @@ let cast_to_int v =
   | Some v -> Result.ok v
   | None -> Result.error "Type error"
 
-let rec interp_pure_expr (subst : subst) expr :
-    (S_val.t, 'err, 'a) Symex.Result.t =
+let rec eval_pure_expr (subst : subst) expr : (S_val.t, 'err, 'a) Symex.Result.t
+    =
   match expr with
   | Pure_expr.Int n -> Result.ok (S_val.int n)
   | Bool b -> Result.ok (S_val.bool b)
@@ -32,8 +37,8 @@ let rec interp_pure_expr (subst : subst) expr :
       let* v = Symex.nondet S_val.t_int in
       Result.ok v
   | BinOp (e1, op, e2) -> (
-      let** v1 = interp_pure_expr subst e1 in
-      let** v2 = interp_pure_expr subst e2 in
+      let** v1 = eval_pure_expr subst e1 in
+      let** v2 = eval_pure_expr subst e2 in
       match op with
       | BinOp.Eq -> Symex.Result.ok (v1 ==?@ v2)
       | BinOp.And ->
@@ -65,67 +70,82 @@ module Make (State : State_intf.S) = struct
     let+- msg = f in
     State.error msg state
 
-  let interp_pure_expr subst expr = lift_to_state (interp_pure_expr subst expr)
+  let eval_pure_expr subst expr = lift_to_state (eval_pure_expr subst expr)
   let cast_to_bool v = lift_to_state (cast_to_bool v)
   let cast_to_int v = lift_to_state (cast_to_int v)
 
-  let rec interp_expr (subst : subst) (state : State.t) expr =
+  let rec eval_expr (subst : subst) (state : State.t option) expr =
     let* () = Symex.consume_fuel_steps 1 in
     L.debug (fun m ->
         m "@[<v 0>@[<v 2>Interp expr:@ %a@]@.@[<v 2>In subst:@ %a@]@]" Expr.pp
           expr pp_subst subst);
     match expr with
     | Expr.Pure_expr e ->
-        let++ v = interp_pure_expr subst e state in
+        let++ v = eval_pure_expr subst e state in
         (v, state)
     | Let (x, e1, e2) ->
-        let** v1, state = interp_expr subst state e1 in
+        let** v1, state = eval_expr subst state e1 in
         let subst =
           Option.fold ~none:subst ~some:(fun x -> String_map.add x v1 subst) x
         in
-        interp_expr subst state e2
+        eval_expr subst state e2
     | If (guard, then_, else_) ->
-        let** v_guard, state = interp_expr subst state guard in
+        let** v_guard, state = eval_expr subst state guard in
         let** v_guard = cast_to_bool v_guard state in
-        if%sat v_guard then interp_expr subst state then_
-        else interp_expr subst state else_
+        if%sat v_guard then eval_expr subst state then_
+        else eval_expr subst state else_
     | Call (fname, arg_exprs) ->
         let** arg_values =
           Symex.Result.fold_list arg_exprs ~init:[] ~f:(fun acc e ->
-              let++ res = interp_pure_expr subst e state in
+              let++ res = eval_pure_expr subst e state in
               res :: acc)
         in
         let arg_values = List.rev arg_values in
-        let func = get_function fname in
-        run_function func state arg_values
+        let func = Context.get_function fname in
+        eval_call func state arg_values
     | Load addr ->
-        let** addr = interp_pure_expr subst addr state in
+        let** addr = eval_pure_expr subst addr state in
         let** addr = cast_to_int addr state in
         State.load addr state
     | Store (addr, value) ->
-        let** addr = interp_pure_expr subst addr state in
+        let** addr = eval_pure_expr subst addr state in
         let** addr = cast_to_int addr state in
-        let** value = interp_pure_expr subst value state in
+        let** value = eval_pure_expr subst value state in
         let++ (), state = State.store addr value state in
         ((S_val.v_false :> S_val.t), state)
     | Alloc ->
         let++ addr, state = State.alloc state in
         ((addr :> S_val.t), state)
     | Free addr ->
-        let** addr = interp_pure_expr subst addr state in
+        let** addr = eval_pure_expr subst addr state in
         let** addr = cast_to_int addr state in
         let++ (), state = State.free addr state in
         ((S_val.v_false :> S_val.t), state)
 
-  and run_function func state args =
+  and eval_function func state args =
     let subst = List.combine func.Fun_def.args args |> String_map.of_list in
     L.debug (fun m ->
         m "@[<v 2>Running function %s with args:@ %a@]" func.Fun_def.name
           pp_subst subst);
-    let++ r = interp_expr subst state func.Fun_def.body in
+    let++ r = eval_expr subst state func.Fun_def.body in
     L.debug (fun m ->
         m "@[<v 2>Function %s returned:@ %a@]" func.Fun_def.name
-          (Fmt.Dump.pair S_val.pp State.pp)
+          (Fmt.Dump.pair S_val.pp (Fmt.Dump.option State.pp))
           r);
     r
+
+  and eval_call func state args =
+    let use_specs = Context.use_specs () in
+    if use_specs then
+      let* specs = get_specs func.Fun_def.name in
+      let executions =
+        List.map (fun spec -> fun () -> Context.Spec.execute spec args state)
+      in
+      ()
+    else eval_function func state args
+
+  and get_specs name =
+    match Context.get_specs name with
+    | Some specs -> Symex.return specs
+    | None -> failwith "TODO: compute missing specifications"
 end

soteria-linear/semantic/spec.ml

@@ -0,0 +1,3 @@
+(** Specifications generated by bi-abduction! *)
+
+type t = { requires : State.syn list; ensures : State.syn list }