CS代写 module F = Format

module F = Format

module Command = struct
type var = string

type exp = Var of var | Const of int | BinOp of (exp * exp)

type label = int * Cil.location

let string_of_location (_, loc) =
let file =
let idx = String.rindex loc.Cil.file ‘/’ in
let len = String.length loc.file in
String.sub loc.file (idx + 1) (len – idx – 1)
with _ -> loc.file
file ^ “:” ^ string_of_int loc.line

let pp_label fmt label = F.fprintf fmt “%d” (label |> fst)

let pp_exp fmt = function
| Var v -> F.fprintf fmt “%s” v
| Const i -> F.fprintf fmt “%d” i
(* Vars *)
let vars = get_vars vs in
F.fprintf fmt “%s” (String.concat “,” vars)

let pp fmt = function
| Assign (l, var, e) -> F.fprintf fmt “%a: %s = %a” pp_label l var pp_exp e
| Source (l, var) -> F.fprintf fmt “%a: %s = source()” pp_label l var
| Sanitizer (l, var, e) ->
F.fprintf fmt “%a: %s = sanitizer(%a)” pp_label l var pp_exp e
| Sink (l, e) -> F.fprintf fmt “%a: sink(%a)” pp_label l pp_exp e
| Skip l -> F.fprintf fmt “%a: skip” pp_label l
| Branch l -> F.fprintf fmt “%a: branch” pp_label l

module Node = struct
type t = Command.t

let compare = compare

let equal = ( = )

let hash = Hashtbl.hash

let count = ref 0

let rec of_exp exp =
let open Cil in
match exp with
| Lval (Var v, NoOffset) -> Command.Var v.vname
| Const (CInt64 (i, _, _)) -> Command.Const (Int64.to_int i)
| BinOp (_, e1, e2, _) -> Command.BinOp (of_exp e1, of_exp e2)
| _ -> failwith “Unsupported syntax”

let tostring s = Escape.escape_string (Pretty.sprint ~width:0 s)

let of_stmt stmt =
let open Cil in
match stmt.skind with
| Instr [ Set ((Var vi, NoOffset), e, loc) ] ->
Command.Assign ((stmt.sid, loc), vi.vname, of_exp e)
| Instr [ Call (Some (Var vi, _), Lval (Var f, _), _, loc) ]
when f.vname = “source” ->
Source ((stmt.sid, loc), vi.vname)
| Instr [ Call (Some (Var vi, _), Lval (Var f, _), [ e ], loc) ]
when f.vname = “sanitizer” ->
Sanitizer ((stmt.sid, loc), vi.vname, of_exp e)
| Instr [ Call (None, Lval (Var f, _), [ e ], loc) ] when f.vname = “sink”
Sink ((stmt.sid, loc), of_exp e)
| If (_, _, _, loc) -> Branch (stmt.sid, loc)
| Return (_, loc) | Loop (_, loc, _, _) | Goto (_, loc) | Break loc ->
Skip (stmt.sid, loc)
| Instr [] | Block _ -> Skip (stmt.sid, Cil.locUnknown)
d_stmt () stmt |> tostring |> prerr_endline;
failwith “Unsupported syntax”

let pp = Command.pp

module G = Graph.Persistent.Digraph.ConcreteBidirectional (Node)

type t = G.t

let add_edge = G.add_edge

let empty = G.empty

let iter_edges = G.iter_edges

let fold_edges = G.fold_edges

let fold_vertex = G.fold_vertex

let of_cfile file =
let cil = Frontend.parse file in
Cil.foldGlobals cil
(fun result glob ->
match glob with
| Cil.GFun (fd, _) when fd.svar.vname = “main” -> Some fd
| _ -> result)
| Some fd ->
Cil.computeCFGInfo fd true;
(match fd.Cil.smaxstmtid with Some i -> Node.count := i | None -> ());
List.fold_left
(fun g stmt ->
List.fold_left
(fun g succ -> add_edge g (Node.of_stmt stmt) (Node.of_stmt succ))
g stmt.Cil.succs)
empty fd.sallstmts
| None -> failwith “main not found”

let pp fmt g =
iter_edges
(fun src dst -> F.fprintf fmt “%a -> %a\n” Node.pp src Node.pp dst)

let print cfg =
let oc = open_out “cfg.txt” in
F.fprintf (F.formatter_of_out_channel oc) “%a” pp cfg;
close_out oc

let num_of_assignments cfg =
fold_vertex
(fun node cnt -> match node with Command.Assign _ -> cnt + 1 | _ -> cnt)

let num_of_obvious_bugs cfg =
fold_edges
(fun src dst cnt ->
match (src, dst) with
| Command.Source (_, var), Command.Sink (_, e)
when Command.get_vars e |> List.mem var ->
| _ -> cnt)
module F = Format
module Command = CFG.Command
module ConstraintSet = Constraint.Set

(* ************************************** *
Extracting Basic Facts
* ************************************** *)

let extract_cedge src dst set = failwith “Not implemented”

let extract_source node set = failwith “Not implemented”

let extract_sanitizer node set = failwith “Not implemented”

let extract_sink node set = failwith “Not implemented”

let extract_def node set = failwith “Not implemented”

let extract_use node set = failwith “Not implemented”

let extract_kill node1 node2 set = failwith “Not implemented”

let extract : CFG.t -> ConstraintSet.t = failwith “Not implemented”

(* ************************************** *
Rules for Reaching Definition Analysis
* ************************************** *)

(* Def(a, _) => Out(a, a) *)
let derive_out1 cs = failwith “Not implemented”

(* In(a, b) ^ !Kill(a, b) => Out(a, b) *)
let derive_out2 cs = failwith “Not implemented”

(* Out(a, b) ^ CEdge(a, c) => In(c, b) *)
let derive_in cs = failwith “Not implemented”

(* ************************************** *
Rules for Taint Analysis
* ************************************** *)

(* CEdge(a, b) => CPath(a, b) *)
let derive_cpath1 cs = failwith “Not implemented”

(* CPath(a, b) ^ CEdge(b, c) => CPath(a, c) *)
let derive_cpath2 cs = failwith “Not implemented”

(* In(a, b) ^ Use(a, v) ^ Def(b, v) => Edge(b, a) *)
let derive_edge cs = failwith “Not implemented”

(* Source(a) ^ Edge(a, b) => Path(a, b) *)
let derive_path1 cs = failwith “Not implemented”

(* Path(a, b) ^ Edge(b, c) ^ !Sanitizer(c) => Path(a, c) *)
let derive_path2 cs = failwith “Not implemented”

(* Path(a, b) ^ Sink(b) => Alarm(a, b) *)
let derive_alarm cs = failwith “Not implemented”

let rec solve const_set = failwith “Not implemented”

let compare = compare

let pp fmt = function
| CEdge (a, b) ->
F.fprintf fmt “CEdge (%a, %a)” Command.pp_label a Command.pp_label b
| CPath (a, b) ->
F.fprintf fmt “CPath (%a, %a)” Command.pp_label a Command.pp_label b
| Def (l, v) -> F.fprintf fmt “Def (%a, %s)” Command.pp_label l v
| Use (l, v) -> F.fprintf fmt “Use (%a, %s)” Command.pp_label l v
| Kill (a, b) ->
F.fprintf fmt “Kill (%a, %a)” Command.pp_label a Command.pp_label b
| In (a, b) ->
F.fprintf fmt “In (%a, %a)” Command.pp_label a Command.pp_label b
| Out (a, b) ->
F.fprintf fmt “Out (%a, %a)” Command.pp_label a Command.pp_label b
| Source l -> F.fprintf fmt “Source %a” Command.pp_label l
| Sink l -> F.fprintf fmt “Sink %a” Command.pp_label l
| Sanitizer l -> F.fprintf fmt “Santizer %a” Command.pp_label l
| Edge (a, b) ->
F.fprintf fmt “Edge (%a, %a)” Command.pp_label a Command.pp_label b
| Path (a, b) ->
F.fprintf fmt “Path (%a, %a)” Command.pp_label a Command.pp_label b
| Alarm (a, b) ->
F.fprintf fmt “Alarm (%a, %a)” Command.pp_label a Command.pp_label b

module Set = struct
include Set.Make (Constraint)

let pp fmt cs = iter (fun c -> F.fprintf fmt “%a\n” Constraint.pp c) cs

let print set =
let oc = open_out “result.txt” in
F.fprintf (F.formatter_of_out_channel oc) “%a” pp set;
close_out oc

include Constraint
let rec remove_temp instrs =
match instrs with
| Cil.Call (Some l, f, es, loc) :: Cil.Set (x, Cil.Lval r, _) :: t when l = r
Cil.Call (Some x, f, es, loc) :: remove_temp t
| h :: t -> h :: remove_temp t
| [] -> []

class removeTempVisitor =
inherit Cil.nopCilVisitor

method! vblock b =
let new_bstmts =
List.fold_left
(fun bstmts stmt ->
match stmt.Cil.skind with
| Cil.Instr [] when stmt.labels <> [] -> stmt :: bstmts
| Cil.Instr instrs ->
stmt.Cil.skind <- Cil.Instr (remove_temp instrs); stmt :: bstmts | _ -> stmt :: bstmts)
[] b.Cil.bstmts
b.Cil.bstmts <- List.rev new_bstmts; Cil.DoChildren class flattenVisitor = inherit Cil.nopCilVisitor method! vblock b = let new_bstmts = List.fold_left (fun bstmts stmt ->
match stmt.Cil.skind with
| Cil.Instr [] when stmt.labels <> [] -> stmt :: bstmts
| Cil.Instr instrs ->
(List.map Cil.mkStmtOneInstr instrs |> List.rev) @ bstmts
| _ -> stmt :: bstmts)
[] b.Cil.bstmts
b.Cil.bstmts <- List.rev new_bstmts; Cil.DoChildren let initialize () = Cil.initCIL (); Cabs2cil.doCollapseCallCast := true let prepare cfile = Cil.iterGlobals cfile (function | Cil.GFun (fd, _) -> Cil.prepareCFG fd
| _ -> ());
Cil.visitCilFile (new removeTempVisitor) cfile;
Cil.visitCilFile (new flattenVisitor) cfile

let parse cfile =
initialize ();
let cil = Frontc.parse cfile () in
prepare cil;
module F = Format
module ConstraintSet = Analyzer.ConstraintSet

let report const_set =
ConstraintSet.iter
match c with
| Constraint.Alarm (src, sink) ->
Format.printf “Potential Error @@ %s (%s)\n”
(CFG.Command.string_of_location src)
(CFG.Command.string_of_location sink)
| _ -> ())

let main argv =
if Array.length argv <> 2 then (
prerr_endline “analyzer: You must specify one C file”;
let cfg = CFG.of_cfile argv.(1) in
CFG.print cfg;
let result = cfg |> Analyzer.extract |> Analyzer.solve in
ConstraintSet.print result;
report result

let _ = main Sys.argv

程序代写 CS代考加微信: powcoder QQ: 1823890830 Email: powcoder@163.com

Related Posts