nits

backend/cn/lib/definition.ml

@@ -117,15 +117,15 @@ module Clause = struct
     aux clause_packing_ft
 
 
-    let rec explicit_negative_guards_aux (cs : t list) (prev_negated : IT.t) : t list =
+  let rec explicit_negative_guards_aux (cs : t list) (prev_negated : IT.t) : t list =
     let cerb_loc = Cerb_location.unknown in
     match cs with
     | [] -> []
-    | {loc; guard=cur_guard; packing_ft} :: cs' ->
+    | { loc; guard=cur_guard; packing_ft } :: cs' ->
       let cur =
-        {loc; guard=IT.and_ [prev_negated; cur_guard] cerb_loc; packing_ft}
+        { loc; guard=IT.and_ [ prev_negated; cur_guard ] cerb_loc; packing_ft }
       in
-      let so_far_ng = IT.and_ [IT.not_ cur_guard cerb_loc; prev_negated] cerb_loc in
+      let so_far_ng = IT.and_ [ IT.not_ cur_guard cerb_loc; prev_negated ] cerb_loc in
       cur :: explicit_negative_guards_aux cs' so_far_ng
 
 

backend/cn/lib/explain.ml

@@ -31,7 +31,7 @@ open ResultWithData
 
 (* ask the solver if the given set of constraints is satisfiable *)
 let ask_solver g lcs =
-  match (Solver.ask_solver g lcs) with
+  match Solver.ask_solver g lcs with
   | Unsat -> No !^"Solver returned No."
   | Unknown -> Unknown !^"Solver returned Unknown."
   | Sat -> Yes lcs
@@ -41,7 +41,7 @@ let ask_solver g lcs =
 let convert_symmap_to_lc (m : IT.t Sym.Map.t) : LogicalConstraints.t list =
   let loc = Cerb_location.unknown in
   let kvs = Sym.Map.bindings m in
-  let to_lc (k, v) = LC.T (IT.eq_ (IT.IT (IT.Sym k, IT.get_bt v, loc) , v) loc) in
+  let to_lc (k, v) = LC.T (IT.eq_ (IT.IT (IT.Sym k, IT.get_bt v, loc), v) loc) in
   List.map to_lc kvs
 
 
@@ -50,25 +50,25 @@ let rec check_pred (name : Sym.t) (def : Def.Predicate.t) (candidate : IT.t) (ct
   : LAT.check_result
   =
   (* ensure candidate type matches output type of predicate *)
-  if (not (BT.equal (IT.get_bt candidate) (def.oarg_bt))) then
+  if not (BT.equal (IT.get_bt candidate) (def.oarg_bt)) then
     No
-      (!^"Candidate"
-      ^^^ IT.pp candidate
-      ^^^ !^"has different type from predicate output:"
-      ^^^ BT.pp (IT.get_bt candidate)
-      ^^^ !^" versus"
-      ^^^ BT.pp def.oarg_bt
-      ^^^ !^".")
-  else
+       (!^"Candidate"
+       ^^^ IT.pp candidate
+       ^^^ !^"has different type from predicate output:"
+       ^^^ BT.pp (IT.get_bt candidate)
+       ^^^ !^" versus"
+       ^^^ BT.pp def.oarg_bt
+       ^^^ !^".")
+  else (
     match def.clauses with
     | None -> Unknown (!^"Predicate" ^^^ Sym.pp name ^^^ !^"is uninterpreted. ")
     | Some clauses ->
       let clauses_with_guards = Def.Clause.explicit_negative_guards clauses in
       (* for each clause, check if candidate could have been its output *)
       let checked =
-        List.map (fun c -> check_clause c candidate  ctxt def.iargs) clauses_with_guards
+        List.map (fun c -> check_clause c candidate ctxt def.iargs) clauses_with_guards
       in
-      LAT.combine_results checked
+      LAT.combine_results checked)
 
 
 (* check if a candidate term could have been the output of a predicate clause *)
@@ -121,48 +121,48 @@ and get_var_constraints
   match Sym.Map.find_opt v var_def_locs with
   | None ->
     (match (Sym.Map.find_opt v ctxt.logical, Sym.Map.find_opt v ctxt.computational) with
-    | Some (Value it, _), _ -> get_body_constraints it var_def_locs v_cand ctxt iargs
-    | _, Some (Value it, _) -> get_body_constraints it var_def_locs v_cand ctxt iargs
-    (* TODO: logical vs computational *)
-    (* TODO: BaseType case? *)
-    | _ ->
-      let f = fun (s, _) -> Sym.equal s v in
-      if (Base.List.exists iargs ~f) then
-        Yes ([], var_cands)
-      else
-        Unknown (!^"Could not find variable definition line for" ^^^ (Sym.pp v)))
+     | Some (Value it, _), _ -> get_body_constraints it var_def_locs v_cand ctxt iargs
+     | _, Some (Value it, _) -> get_body_constraints it var_def_locs v_cand ctxt iargs
+     (* TODO: logical vs computational *)
+     (* TODO: BaseType case? *)
+     | _ ->
+       let f (s, _) = Sym.equal s v in
+       if (Base.List.exists iargs ~f) then
+         Yes ([], var_cands)
+       else
+         Unknown (!^"Could not find variable definition line for" ^^^ (Sym.pp v)))
   | Some line ->
-    match line with
-      (* recurse with x's definition *)
-    | DefineL ((_, t), _) ->
-      get_body_constraints t var_def_locs v_cand ctxt iargs (*TODO: variable conflicts?*)
-    | ResourceL ((_, (p, _)), _) ->
-      match p with
-      | P psig ->
-        (match psig.name with
-        | Owned (_, _) ->
-          (* if the predicate is Owned, its pointer argument should not be null *)
-          let neq = IT.ne__ psig.pointer (IT.null_ loc) loc in
-          Yes ([LC.T neq], var_cands)
+    (match line with
+     (* recurse with x's definition *)
+     | DefineL ((_, t), _) ->
+       get_body_constraints t var_def_locs v_cand ctxt iargs (*TODO: variable conflicts?*)
+     | ResourceL ((_, (p, _)), _) ->
+       (match p with
+        | P psig ->
+          (match psig.name with
+           | Owned (_, _) ->
+             (* if the predicate is Owned, its pointer argument should not be null *)
+             let neq = IT.ne__ psig.pointer (IT.null_ loc) loc in
+           Yes ([LC.T neq], var_cands)
         | PName name ->
           (* search for predicate definition *)
-          match Sym.Map.find_opt name ctxt.global.resource_predicates with
-          | Some pdef ->
-            (* TODO: this doesn't account for looking up args of the predicate further up in the graph.
-              Adding that will require dealing with scoping issues, e.g. if
-              a candidate or line definition for one of the arguments includes a variable with a
-              different usage within the predicate *)
-            (match check_pred name pdef v_cand ctxt with
-            | Yes cs -> Yes (cs, var_cands)
-            | No e -> No e
-            | Unknown e -> Unknown e
-            | Error e -> Error e)
-          | None ->
-            Unknown (!^"Could not find definition of predicate" ^^^ Sym.pp name)
-        )
+          (match Sym.Map.find_opt name ctxt.global.resource_predicates with
+           | Some pdef ->
+             (* TODO: this doesn't account for looking up args of the predicate further up in the graph.
+                Adding that will require dealing with scoping issues, e.g. if
+                a candidate or line definition for one of the arguments includes a variable with a
+                different usage within the predicate *)
+             (match check_pred name pdef v_cand ctxt with
+              | Yes cs -> Yes (cs, var_cands)
+              | No e -> No e
+              | Unknown e -> Unknown e
+              | Error e -> Error e)
+           | None ->
+             Unknown (!^"Could not find definition of predicate" ^^^ Sym.pp name))
+          )
       | Q qsig ->
         let _ = qsig in
-        Unknown (!^"Quantified predicates are out of scope for now.")
+        Unknown (!^"Quantified predicates are out of scope for now.")))
 
 (** End section: Infrastructure for checking if a countermodel satisfies a predicate **)
 
@@ -322,31 +322,31 @@ let state (ctxt : C.t) log model_with_q extras =
       match (Request.get_name rt, o) with
       | Owned _, _ -> None
       | PName s, Resource.O it ->
-        (match (Sym.Map.find_opt s defs), evaluate it with
-        | Some def, Some cand -> Some (check_pred s def cand ctxt, rt, it)
-        | Some _, None ->
-          Some (Error (!^"Could not locate definition of variable" ^^^ IT.pp it), rt, it)
-        | None, _ ->
-          Some (Error (!^"Could not locate definition of predicate" ^^^ Sym.pp s), rt, it))
-        in
+        (match (Sym.Map.find_opt s defs, evaluate it) with
+         | Some def, Some cand -> Some (check_pred s def cand ctxt, rt, it)
+         | Some _, None ->
+           Some (Error (!^"Could not locate definition of variable" ^^^ IT.pp it), rt, it)
+         | None, _ ->
+           Some (Error (!^"Could not locate definition of predicate" ^^^ Sym.pp s), rt, it))
+    in
     let checked = LAT.filter_map_some check (C.get_rs ctxt) in
     let nos, rest = List.partition (fun (r, _, _) -> is_no r) checked in
     let yeses, unknown = List.partition (fun (r, _, _) -> is_yes r) rest in
     let pp_checked_res (_, req, cand) =
       let rslt = Req.pp req ^^^ !^", output: " ^^^ IT.pp cand in
       Rp.
-        { original = rslt ;
+        { original = rslt;
           (*TODO: original =  LAT.pp_check_result (snd p) ;*)
-          simplified = [rslt]
+          simplified = [ rslt ]
         }
       in
     Rp.add_labeled
       Rp.lab_invalid
       (List.map pp_checked_res nos)
       (Rp.add_labeled
-        Rp.lab_unknown
-        (List.map pp_checked_res unknown)
-        (Rp.add_labeled Rp.lab_valid (List.map pp_checked_res yeses) Rp.labeled_empty))
+         Rp.lab_unknown
+         (List.map pp_checked_res unknown)
+         (Rp.add_labeled Rp.lab_valid (List.map pp_checked_res yeses) Rp.labeled_empty))
   in
   let not_given_to_solver =
     (* get predicates from past steps of trace not given to solver *)

backend/cn/lib/logicalArgumentTypes.ml

@@ -242,6 +242,7 @@ let filter_map_some (f : 'a -> 'b option) (l : 'a list) : 'b list =
     []
     l
 
+
 (* Gives a single canonical result *)
 let combine_results (results : check_result list) : check_result =
   match results with
@@ -272,24 +273,25 @@ let def_line_pp dl =
   | ResourceL ((s, (re, _)), _) ->
     group (!^"take" ^^^ Sym.pp s ^^^ equals ^^^ Req.pp re ^^ semi)
 
+
 (* Optionally zip two lists, returning None if the lists have different lengths *)
 let rec zip (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list option =
-  match l1, l2 with
+  match (l1, l2) with
   | [], [] -> Some []
   | h1 :: tl1, h2 :: tl2 ->
     (match zip tl1 tl2 with Some zs -> Some ((h1, h2) :: zs) | None -> None)
   | _, _ -> None
 
+
 (* Take the union of two symbol maps,
    removing any key that is in both maps but has a different value in each *)
 let merge_eq (eq : 'a -> 'a -> bool) (m1 : 'a Sym.Map.t) (m2 : 'a Sym.Map.t)
   : 'a Sym.Map.t
   =
-  let merge _ v1 v2 =
-    if eq v1 v2 then Some v1 else None
-  in
+  let merge _ v1 v2 = if eq v1 v2 then Some v1 else None in
   Sym.Map.union merge m1 m2
 
+
 (* Build a map by using f to develop a map for each
    pair of elements in the two lists, failing
    if they produce different results for any symbol or if
@@ -313,15 +315,15 @@ let rec get_var_cands (exp : IT.t) (candidate : IT.t)
   =
   let map_from_IT_lists = map_from_lists get_var_cands IT.equal in
   let sort_by_discard_fst compare l =
-    List.map snd ( List.sort (fun p1 p2 -> compare (fst p1) (fst p2)) l)
+    List.map snd (List.sort (fun p1 p2 -> compare (fst p1) (fst p2)) l)
   in
   let sort_by_id = sort_by_discard_fst Id.compare in
   let sort_by_pattern = sort_by_discard_fst (Terms.compare_pattern BT.compare) in
   let map_with_guard_unknown g l1 l1' =
-    if g then map_from_IT_lists l1 l1' else (Unknown (Pp.bool g ^^^ !^" not satisfied"))
+    if g then map_from_IT_lists l1 l1' else Unknown (Pp.bool g ^^^ !^" not satisfied")
   in
   let map_with_guard_no g l1 l1' =
-    if g then map_from_IT_lists l1 l1' else (No (Pp.bool g ^^^ !^" not satisfied") )
+    if g then map_from_IT_lists l1 l1' else No (Pp.bool g ^^^ !^" not satisfied")
   in
   let default =
     Unknown
@@ -337,7 +339,10 @@ let rec get_var_cands (exp : IT.t) (candidate : IT.t)
   | ITE (exp1, exp2, exp3), ITE (exp1', exp2', exp3') ->
     map_from_IT_lists [ exp1; exp2; exp3 ] [ exp1'; exp2'; exp3' ]
   | EachI ((z1, (v, bty), z2), exp1), EachI ((z1', (v', bty'), z2'), exp1') ->
-    map_with_guard_unknown (z1 = z1' && Sym.equal v v' && BT.equal bty bty' && z2 = z2') [ exp1 ] [ exp1' ]
+    map_with_guard_unknown
+      (z1 = z1' && Sym.equal v v' && BT.equal bty bty' && z2 = z2')
+      [ exp1 ]
+      [ exp1' ]
   | Tuple exps, Tuple exps' -> map_from_IT_lists exps exps'
   | NthTuple (n, exp1), NthTuple (n', exp1') ->
     map_with_guard_unknown (n = n') [ exp1 ] [ exp1' ]
@@ -357,36 +362,34 @@ let rec get_var_cands (exp : IT.t) (candidate : IT.t)
     map_with_guard_no (Sym.equal name name') (sort_by_id args) (sort_by_id args')
   | MemberShift (exp1, v, id), MemberShift (exp1', v', id') ->
     map_with_guard_unknown (Sym.equal v v' && Id.equal id id') [ exp1 ] [ exp1' ]
-  | ArrayShift {base; ct; index}, ArrayShift {base=base'; ct=ct'; index=index'} ->
+  | ArrayShift { base; ct; index }, ArrayShift { base=base'; ct=ct'; index=index' }
+    ->
     map_with_guard_unknown (Sctypes.equal ct ct') [base; index ] [base'; index' ]
-  | CopyAllocId {addr=exp1; loc=exp2}, CopyAllocId {addr=exp1'; loc=exp2'} ->
+  | CopyAllocId { addr=exp1; loc=exp2 }, CopyAllocId { addr=exp1'; loc=exp2' } ->
     map_from_IT_lists [ exp1; exp2 ] [ exp1'; exp2' ]
-  | HasAllocId exp1, HasAllocId exp1' ->
-    get_var_cands exp1 exp1'
-  | SizeOf cty, SizeOf cty' ->
-    map_with_guard_unknown (Sctypes.equal cty cty') [] []
+  | HasAllocId exp1, HasAllocId exp1' -> get_var_cands exp1 exp1'
+  | SizeOf cty, SizeOf cty' -> map_with_guard_unknown (Sctypes.equal cty cty') [] []
   | OffsetOf (v, id), OffsetOf (v', id') ->
     map_with_guard_unknown (Sym.equal v v' && Id.equal id id') [] []
-  | Nil bty, Nil bty' ->
-    map_with_guard_no (BT.equal bty bty') [] []
-  | Cons (h, tl), Cons (h', tl') ->
-    map_from_IT_lists [ h; tl ] [ h'; tl' ]
-  | Head l, Head l' ->
-    get_var_cands l l'
-  | Tail l, Tail l' ->
-    get_var_cands l l'
-  | NthList (exp1, exp2, exp3),  NthList (exp1', exp2', exp3') ->
+  | Nil bty, Nil bty' -> map_with_guard_no (BT.equal bty bty') [] []
+  | Cons (h, tl), Cons (h', tl') -> map_from_IT_lists [ h; tl ] [ h'; tl' ]
+  | Head l, Head l' -> get_var_cands l l'
+  | Tail l, Tail l' -> get_var_cands l l'
+  | NthList (exp1, exp2, exp3), NthList (exp1', exp2', exp3') ->
     map_from_IT_lists [ exp1; exp2; exp3 ] [ exp1'; exp2'; exp3' ]
   | ArrayToList (exp1, exp2, exp3), ArrayToList (exp1', exp2', exp3') ->
     map_from_IT_lists [ exp1; exp2; exp3 ] [ exp1'; exp2'; exp3' ]
   | Representable (cty, exp1), Representable (cty', exp1') ->
     map_with_guard_unknown (Sctypes.equal cty cty') [ exp1 ] [ exp1' ]
   | Good (cty, exp1), Good (cty', exp1') ->
     map_with_guard_unknown (Sctypes.equal cty cty') [ exp1 ] [ exp1' ]
-  | Aligned { t=exp1; align=exp2}, Aligned { t=exp1'; align=exp2'} ->
+  | Aligned { t=exp1; align=exp2 }, Aligned { t=exp1'; align=exp2' } ->
     map_from_IT_lists [ exp1; exp2 ] [ exp1'; exp2' ]
   | WrapI (ity, exp1), WrapI (ity', exp1') ->
-    map_with_guard_unknown (Cerb_frontend.IntegerType.integerTypeEqual ity ity') [ exp1 ] [ exp1' ]
+    map_with_guard_unknown
+      (Cerb_frontend.IntegerType.integerTypeEqual ity ity')
+      [ exp1 ]
+      [ exp1' ]
   | MapConst (bty, exp1), MapConst (bty', exp1') ->
     map_with_guard_unknown (BT.equal bty bty') [ exp1 ] [ exp1' ]
   | MapSet (exp1, exp2, exp3), MapSet (exp1', exp2', exp3') ->
@@ -406,7 +409,7 @@ let rec get_var_cands (exp : IT.t) (candidate : IT.t)
   (* included so the compiler will catch any missing new constructors *)
   | Const _, _ -> default
   | Unop _, _ -> default
-  | Binop _, _-> default
+  | Binop _, _ -> default
   | ITE _, _ -> default
   | EachI _, _ -> default
   | Tuple _, _ -> default
@@ -443,11 +446,17 @@ let rec get_var_cands (exp : IT.t) (candidate : IT.t)
   | Match _, _ -> default
   | Cast _, _ -> default
 
+
 (* Get the free variables from an expression *)
 let get_fvs (exp : IT.t) : Sym.t list = Sym.Set.elements (IT.free_vars exp)
 
 (*TODO: what if lcs mention vars not examined in the algorithm*)
-let rec organize_lines_aux (lines : packing_ft) (defs : def_line Sym.Map.t) (lcs : LC.t list): IT.t * def_line Sym.Map.t * (LC.t list) =
+let rec organize_lines_aux
+  (lines : packing_ft)
+  (defs : def_line Sym.Map.t)
+  (lcs : LC.t list)
+  : IT.t * def_line Sym.Map.t * (LC.t list)
+  =
   match lines with
   | Define ((v, it), i, next) ->
     let ln = DefineL ((v, it), i) in
@@ -460,7 +469,8 @@ let rec organize_lines_aux (lines : packing_ft) (defs : def_line Sym.Map.t) (lcs
   | Constraint (lc, _, next) -> organize_lines_aux next defs (lc :: lcs)
   | I it -> (it, defs, lcs)
 
+
 (* Sort lines into the returned expression, a map of variables to their defining lines, and a list of constraints *)
-let organize_lines (lines : packing_ft) : IT.t * def_line Sym.Map.t * (LC.t list) = organize_lines_aux lines Sym.Map.empty []
+let organize_lines (lines : packing_ft) : IT.t * def_line Sym.Map.t * LC.t list = organize_lines_aux lines Sym.Map.empty []
 
-(** End infrastructure for checking if a countermodel satisfies a predicate **)
+(** End infrastructure for checking if a countermodel satisfies a predicate **)

backend/cn/lib/report.ml

@@ -241,24 +241,25 @@ let simp_view s =
 
 let table_by_label mk_table render data main_lab labs =
   let get_table lab =
-    match (StrMap.find_opt lab data) with
+    match StrMap.find_opt lab data with
     | None -> (lab, "(none)")
     | Some t -> (lab, mk_table (List.map render t))
   in
   let tables = List.map get_table labs in
   let combine_tables acc (new_lab, new_table) = acc ^ details new_lab new_table in
   List.fold_left combine_tables (snd (get_table main_lab)) tables
 
+
 let make_invalid_resources rs =
   h
     1
     lab_invalid
     (table_by_label
-      table_without_head
-      simp_view
-      rs
-      lab_invalid
-      [lab_unknown; lab_valid])
+       table_without_head
+       simp_view
+       rs
+       lab_invalid
+       [ lab_unknown; lab_valid ])
 
 
 let make_not_given_to_solver ds =